Theory IDE_CP_Core
chapter ‹Integrated Deduction Environment for Programming (IDE-P)›
theory IDE_CP_Core
imports Phi_BI.Phi_BI Phi_Element_Path
keywords
"proc" :: thy_goal_stmt
and "as" "→" "⟼" "←" "^" "^*" "⟸" "⟸'" "$" "subj"
"var" "val" "invar" "⟹" "@tag" "∃" "throws" "holds_fact"
"input" "certified" "apply_rule" "]." ")." ".$" "!."
:: quasi_command
and "❴" :: prf_goal % "proof"
and ";;" "；" :: prf_goal % "proof"
and "❵" :: prf_goal % "proof"
and "φlang_parser" :: thy_decl % "ML"
and "φoverloads" "declare_φlang_operator" :: thy_decl
abbrevs
"!!" = "!!"
and "<label>" = "𝗅𝖺𝖻𝖾𝗅"
and "<by>" = "❙b❙y"
and "<try>" = "❙t❙r❙y"
and "<obligation>" = "𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇"
and ">->" = "↣"
and "<;>" = "⨾"
and "<val>" = "𝗏𝖺𝗅"
and "<ret>" = "❙r❙e❙t"
and "<is>" = "𝗂𝗌"
and "|>" = "‣"
and "<-" = "←"
and "←->" = "⟷"
and ";;" = "；"
begin
section ‹Preliminary Configuration›
named_theorems φlemmata ‹Contextual facts during the programming. They are automatically
aggregated from every attached \<^prop>‹P› in \<^prop>‹𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk in [R] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 Sth 𝗌𝗎𝖻𝗃 P›
during the programming. Do not modify it manually because it is managed automatically and
cleared frequently›
subsubsection ‹Syntax \& Prelude ML›
ML_file ‹library/syntax/Phi_Syntax.ML›
ML_file ‹library/syntax/procedure2.ML›
section ‹Antecedent Jobs \& Annotations in Sequents›
subsection ‹Text Label›
text ‹This part presents a mechanism to encode text symbol inside sequent.
It may be used anywhere needing some text annotation for any purpose.›
paragraph ‹Label tag› text ‹embeds any text string in the name of a lambda abstraction from
\<^typ>‹unit› to \<^typ>‹unit›, i.e. term ▩‹Abs ("embeded text", unit, Bound 0)› if readers are familiar with
the internal representation of terms in Isabelle.
This way encodes text strings using machine string which reaches the optimal performance.
A deficiency is it is unstable for α-conversion. Fortunately, α-conversion doesn't happen during
the unification with a schematic variable, although the unification with another label makes
the result undecidable.
›
datatype label = LABEL_TAG "unit ⇒ unit"
lemma [cong]: "LABEL_TAG x ≡ LABEL_TAG x" using reflexive .
lemma label_eq: "x = y" for x :: label by (cases x, cases y) auto
syntax "_LABEL_" :: "idt ⇒ label" ("LABEL _" [0] 1000)
translations "LABEL name" == "CONST LABEL_TAG (λname. ())"
paragraph ‹Label Input›
definition LabelTag :: " label ⇒ bool" ("𝗅𝖺𝖻𝖾𝗅 _" [1000] 26) where "𝗅𝖺𝖻𝖾𝗅 x ≡ True"
text ‹The \<^term>‹𝗅𝖺𝖻𝖾𝗅 x› indicate \<^term>‹x› is a \<^typ>‹label› that should be set by user, e.g.,
\<^prop>‹𝗅𝖺𝖻𝖾𝗅 name ⟹ do_something_relating name›.
The φ-processor `set_label` processes the \<^term>‹𝗅𝖺𝖻𝖾𝗅 x› antecedent.›
lemma LabelTag: "𝗅𝖺𝖻𝖾𝗅 x" unfolding LabelTag_def ..
paragraph ‹Label Binding of Objects›
definition Labelled :: "label ⇒ 'a::{} ⇒ 'a" where [iff]: "Labelled name x ≡ x"
lemma Labelled_def_sym: ‹x::'a::{} ≡ Labelled name x› unfolding Labelled_def .
lemma Labelled_I': ‹PROP P ⟹ PROP (Labelled name (PROP P))› unfolding Labelled_def .
lemma Labelled_I : ‹P ⟹ PROP Trueprop (Labelled name P)› unfolding Labelled_def .
syntax "_LABELED_" :: "idt ⇒ logic ⇒ logic" ("_❙:/ (_)" [1000,11] 10)
translations "name❙: X" == "CONST Labelled (LABEL name) X"
syntax "_LABELED_PROP_" :: "idt ⇒ prop ⇒ prop" ("_❙:/ (_)" [1000,11] 10)
translations "_LABELED_PROP_ name X" => "CONST Labelled (LABEL name) X"
ML_file ‹library/syntax/label.ML›
ML_file ‹library/tools/named_premises.ML›
definition Labelled_embed :: "label ⇒ bool ⇒ bool" where "Labelled_embed name x ≡ x"
lemma [iso_atomize_rules, symmetric, iso_rulify_rules]:
‹Labelled L (Trueprop P) ≡ Trueprop (Labelled_embed L P)›
unfolding Labelled_embed_def Labelled_def .
subsection ‹General Syntax›
subsubsection ‹Technical Tag›
text ‹A general syntactic tag used for hiding internal things.›
definition Technical :: ‹'a::{} ⇒ 'a› ("TECHNICAL _" [18] 17) where ‹Technical x ≡ x›
lemma Technical_I : ‹P ⟹ Technical P› unfolding Technical_def .
lemma Technical_I': ‹PROP P ⟹ PROP Technical P› unfolding Technical_def .
lemma Technical_D : ‹Technical P ⟹ P› unfolding Technical_def .
lemma Technical_D': ‹PROP Technical P ⟹ PROP P› unfolding Technical_def .
optional_translation_group φhide_techinicals
‹Hides internal techinical constructions›
optional_translations (φhide_techinicals)
("aprop") "Y" <= ("aprop") "(CONST Pure.imp) (CONST Trueprop (CONST Technical X)) Y"
("aprop") "Y" <= ("aprop") "(CONST Pure.imp) (CONST Trueprop (name❙: CONST Technical X)) Y"
("aprop") "Y" <= ("aprop") "(CONST Pure.imp) (CONST Technical X) Y"
("aprop") "Y" <= ("aprop") "(CONST Pure.imp) (name❙: CONST Technical X) Y"
"L" <= "CONST Technical X❟ L"
"R" <= "R ❟ CONST Technical X"
"R❟ L" <= "R ❟ CONST Technical X❟ L"
"𝖼𝗎𝗋𝗋𝖾𝗇𝗍 𝗌𝗍𝖺𝗍𝖾: XCONST Void" <= "𝖼𝗎𝗋𝗋𝖾𝗇𝗍 𝗌𝗍𝖺𝗍𝖾: TECHNICAL X"
"𝖼𝗎𝗋𝗋𝖾𝗇𝗍 𝗏𝗂𝖾𝗐: XCONST Void" <= "𝖼𝗎𝗋𝗋𝖾𝗇𝗍 𝗏𝗂𝖾𝗐: TECHNICAL X"
declare [[φhide_techinicals,
φpremise_attribute [THEN Technical_D ] for ‹Technical ?P› (%φattr_normalize),
φpremise_attribute [THEN Technical_D'] for ‹PROP Technical ?P› (%φattr_normalize) ]]
definition Technical_embed :: ‹bool ⇒ bool› where ‹Technical_embed X ≡ X›
lemma [iso_atomize_rules, symmetric, iso_rulify_rules]:
‹Technical (Trueprop P) ≡ Trueprop (Technical_embed P)›
unfolding Technical_def Technical_embed_def .
lemma [φreason 1000]:
‹ X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 C
⟹ TECHNICAL X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 C ›
unfolding Technical_def .
lemma [φreason 1000]:
‹ C 𝗌𝗎𝖿𝖿𝗂𝖼𝖾𝗌 X
⟹ C 𝗌𝗎𝖿𝖿𝗂𝖼𝖾𝗌 TECHNICAL X ›
unfolding Technical_def .
paragraph ‹Reasoning Rules›
lemma [φreason 1200]:
‹ Identity_Element⇩I X P
⟹ Identity_Element⇩I (TECHNICAL X) P›
unfolding Technical_def .
lemma [φreason 1200]:
‹ Identity_Element⇩E X
⟹ Identity_Element⇩E (TECHNICAL X) ›
unfolding Technical_def .
ML_file ‹library/system/reasoners.ML›
subsection ‹Annotations on φ-Types›
typedecl struct_tag
definition Struct_Tag :: ‹'a BI ⇒ struct_tag ⇒ 'a BI› ("_【_】" [17,17] 16)
where ‹Struct_Tag S tg ≡ S›
text ‹In a ToA like \<^term>‹x ⦂ T【A】𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ U【A】› , \<^term>‹x ⦂ T【A】› represents the
\<^term>‹x ⦂ T› may come from a larger structure ‹A› containing it, and after the transformation,
it hints the system to put \<^term>‹y ⦂ U› back to the original position of \<^term>‹x ⦂ T› in ‹A›.
It is useful when we access or modify a field in a complex structure, and the original structure
of ‹A› will not be broken after the access.
›
subsubsection ‹Implementation›
definition Changes_To :: ‹'a BI ⇒ ('b,'c) φ ⇒ 'a BI› (infix "<changes-to>" 16)
where ‹(S <changes-to> _) = S›
definition Auto_Transform_Hint :: ‹'b BI ⇒ 'a BI ⇒ bool›
where ‹Auto_Transform_Hint residue result = True›
subsection ‹Programming Modes›
typedecl working_mode
consts working_mode_procedure :: working_mode
working_mode_implication :: working_mode
working_mode_view_shift :: working_mode
definition φProgramming_Method :: ‹prop ⇒ working_mode ⇒ prop ⇒ prop ⇒ prop ⇒ prop›
where ‹φProgramming_Method Target mode Programming_Deduction Post_Reasoning Future_Works
≡ ( PROP Programming_Deduction
⟹ PROP Post_Reasoning
⟹ PROP Future_Works
⟹ PROP Target)›
declare [[φreason_default_pattern
‹PROP φProgramming_Method ?T _ _ _ _› ⇒ ‹PROP φProgramming_Method ?T _ _ _ _› (100)
]]
φreasoner_group φprogramming_method = (1000, [1000,1999])
for ‹PROP φProgramming_Method Target mode Programming_Deduction Post_Reasoning Future_Works›
‹Rules indicating how to derive the given property ‹Target›, under what ‹mode›, with what reasoning
goals ‹Post_Reasoning› to be processed using φ-LPR after the programming, and with what remaining
goals ‹Future_Works› presenting to the user to be processed later.
The Programming_Deduction have to be in Harrop form:
‹⋀xs. premses ⟹ conclsion›
where ‹xs› are local variables to be fixed, ‹premises› are local assumptions which can be prefixed
by ‹name❙:› (see \<^const>‹Labelled›) giving the name binding the premise. Among the premises, there
must be one of name ‹φ𝗂𝗇𝗂𝗍𝗂𝖺𝗅› which is the initial sequent of user deduction. From the inital sequent,
users are expected to deduce the conclusion proposition.
Any rule specifying programming methods should be cutting.
›
lemma reason_programming:
‹ PROP φProgramming_Method Target working_mode Programming_Deduction Post_Reasoning Future_Works
⟹ TERM working_mode
⟹ PROP Programming_Deduction
⟹ PROP Post_Reasoning
⟹ PROP Future_Works
⟹ PROP Target›
unfolding φProgramming_Method_def
subgoal premises prems using prems(1)[OF prems(3) prems(4) prems(5)] . .
ML_file ‹library/system/Phi_Working_Mode.ML›
ML_file ‹library/system/Phi_Envir.ML›
hide_fact introduce_Ex_ToA_subj_P introduce_Ex_ToA_subj introduce_Ex_ToA
introduce_Ex_pending_E introduce_Ex_pending introduce_Ex_subj introduce_Ex
subsubsection ‹General Rules Normalizing Programming Methods›
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method G⇩1 M D R F
⟹ PROP φProgramming_Method (PROP G⇩1 &&& PROP G⇩2) M D R (PROP F &&& PROP G⇩2) ›
unfolding φProgramming_Method_def conjunction_imp
by (rule conjunctionI)
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method (Trueprop Q) M D R F
⟹ PROP φProgramming_Method (Trueprop (P ⟶ Q)) M (P ⟹ PROP D) (P ⟹ PROP R) (P ⟹ PROP F)›
unfolding φProgramming_Method_def
proof (intro impI)
assume A: ‹PROP D ⟹ PROP R ⟹ PROP F ⟹ Q›
and D: ‹P ⟹ PROP D›
and R: ‹P ⟹ PROP R›
and F: ‹P ⟹ PROP F›
and P: ‹P›
show ‹Q› using A[OF D[OF P] R[OF P] F[OF P]] .
qed
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method Q M D R F
⟹ PROP φProgramming_Method (PROP P ⟹ PROP Q) M (PROP P ⟹ PROP D) (PROP P ⟹ PROP R)
(PROP P ⟹ PROP F)›
unfolding φProgramming_Method_def
proof -
assume A: ‹PROP D ⟹ PROP R ⟹ PROP F ⟹ PROP Q›
and D: ‹PROP P ⟹ PROP D›
and R: ‹PROP P ⟹ PROP R›
and F: ‹PROP P ⟹ PROP F›
and P: ‹PROP P›
show ‹PROP Q› using A[OF D[OF P] R[OF P] F[OF P]] .
qed
lemma φProgramming_Method_All:
‹ (⋀x. PROP φProgramming_Method (Trueprop (P x)) M (D x) (R x) (F x))
⟹ PROP φProgramming_Method (Trueprop (All P)) M (⋀x. PROP D x) (⋀x. PROP R x) (⋀x. PROP F x)›
unfolding φProgramming_Method_def
proof (intro allI)
fix x :: 'a
assume A: ‹⋀x. PROP D x ⟹ PROP R x ⟹ PROP F x ⟹ P x›
and D: ‹⋀x. PROP D x›
and R: ‹⋀x. PROP R x›
and F: ‹⋀x. PROP F x›
show ‹P x› using A[OF D R F] .
qed
lemma φProgramming_Method_ALL:
‹ (⋀x. PROP φProgramming_Method (P x) M (D x) (R x) (F x))
⟹ PROP φProgramming_Method (⋀x. PROP P x) M (⋀x. PROP D x) (⋀x. PROP R x) (⋀x. PROP F x)›
unfolding φProgramming_Method_def
proof -
fix x :: 'a
assume A: ‹⋀x. PROP D x ⟹ PROP R x ⟹ PROP F x ⟹ PROP P x›
and D: ‹⋀x. PROP D x›
and R: ‹⋀x. PROP R x›
and F: ‹⋀x. PROP F x›
show ‹PROP P x› using A[OF D R F] .
qed
φreasoner_ML ‹φProgramming_Method (Trueprop (All P))› 1000
(‹PROP φProgramming_Method (Trueprop (All ?P)) _ _ _ _›)
= ‹fn (_, (ctxt,sequent)) =>
let val _ $ (_ $ (_ $ P)) $ _ $ _ $ _ $ _ = Thm.major_prem_of sequent
fun rename N' (Abs ("x",T,X)) = Abs (N',T,X)
| rename N' (X $ Y) = rename N' X $ rename N' Y
| rename _ X = X
val rule = @{thm φProgramming_Method_All}
val rule' = case P of Abs (N,_,_) => Thm.renamed_prop (rename N (Thm.prop_of rule)) rule
| _ => rule
in Phi_Reasoners.wrap (Phi_Reasoner.single_RS rule') (ctxt,sequent)
end
›
φreasoner_ML ‹φProgramming_Method (Pure.all P)› 1000
(‹PROP φProgramming_Method (Pure.all ?P) _ _ _ _›)
= ‹fn (_, (ctxt,sequent)) =>
let val _ $ (_ $ P) $ _ $ _ $ _ $ _ = Thm.major_prem_of sequent
fun rename N' (Abs ("x",T,X)) = Abs (N',T,X)
| rename N' (X $ Y) = rename N' X $ rename N' Y
| rename _ X = X
val rule = @{thm φProgramming_Method_ALL}
val rule' = case P of Abs (N,_,_) => Thm.renamed_prop (rename N (Thm.prop_of rule)) rule
| _ => rule
in Phi_Reasoners.wrap (Phi_Reasoner.single_RS rule') (ctxt,sequent)
end
›
hide_fact φProgramming_Method_All φProgramming_Method_ALL
subsubsection ‹Built-in Programming Methods›
paragraph ‹Transformation›
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method
(Trueprop (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P))
working_mode_implication
(⋀ℭc. φ𝗂𝗇𝗂𝗍𝗂𝖺𝗅❙: (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭc) 𝗂𝗌 X) ⟹ 𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭc) 𝗂𝗌 Y 𝗌𝗎𝖻𝗃 P)
(Trueprop True)
(Trueprop True)›
unfolding φProgramming_Method_def conjunction_imp all_conjunction Action_Tag_def
Labelled_def
using φmake_implication .
paragraph ‹View Shift›
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method
(Trueprop (X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P))
working_mode_view_shift
(⋀ℭc ℜr. φ𝗂𝗇𝗂𝗍𝗂𝖺𝗅❙: (𝗏𝗂𝖾𝗐 ℭc [ℜr] 𝗂𝗌 X) ⟹ 𝗏𝗂𝖾𝗐 ℭc [ℜr] 𝗂𝗌 Y 𝗌𝗎𝖻𝗃 P)
(Trueprop True)
(Trueprop True)›
unfolding φProgramming_Method_def conjunction_imp all_conjunction Action_Tag_def Labelled_def
using φmake_view_shift .
paragraph ‹Procedure›
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method
(Trueprop (𝗉𝗋𝗈𝖼 G ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
working_mode_procedure
(⋀𝔖s ℜr. φ𝗂𝗇𝗂𝗍𝗂𝖺𝗅❙: (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 𝔖s [ℜr] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 X) ⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 G 𝗈𝗇 𝔖s [ℜr] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 Y 𝗍𝗁𝗋𝗈𝗐𝗌 E)
(Trueprop True)
(Trueprop True)›
unfolding φProgramming_Method_def conjunction_imp all_conjunction Action_Tag_def Labelled_def
using φreassemble_proc_final .
hide_fact φmake_implication φmake_view_shift φreassemble_proc_final
paragraph ‹Object_Equiv›
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method (⋀x y. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 eq x y ⟹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ T) M D R F
⟹ PROP φProgramming_Method (Trueprop (Object_Equiv T eq)) M D R ((∀x. eq x x) &&& PROP F)›
unfolding φProgramming_Method_def Object_Equiv_def Premise_def conjunction_imp
by clarsimp
paragraph ‹Identity Element›
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method (Trueprop (A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 1 𝗐𝗂𝗍𝗁 P)) M D R F
⟹ PROP φProgramming_Method (Trueprop (Identity_Element⇩I A P)) M D R F ›
unfolding φProgramming_Method_def Identity_Element⇩I_def
by simp
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method (Trueprop (1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 A)) M D R F
⟹ PROP φProgramming_Method (Trueprop (Identity_Element⇩E A)) M D R F ›
unfolding φProgramming_Method_def Identity_Element⇩E_def
by simp
paragraph ‹Is_Functional›
context begin
private lemma Is_Functional_imp'':
‹ S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S' 𝗐𝗂𝗍𝗁 Is_Functional S'
⟹ Is_Functional S›
unfolding Transformation_def Is_Functional_def
by blast
lemma [φreason %φprogramming_method]:
‹ PROP φProgramming_Method (Trueprop (S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S' 𝗌𝗎𝖻𝗃-𝗋𝖾𝖺𝗌𝗈𝗇𝗂𝗇𝗀 Is_Functional S')) M D R F
⟹ Friendly_Help TEXT(‹Hi! You are trying to show› S ‹is functional›
‹Now you entered the programming mode and you need to transform the specification to›
‹someone which is functional, so that we can verify your claim.›)
⟹ PROP φProgramming_Method (Trueprop (Is_Functional S)) M D R F›
unfolding φProgramming_Method_def ToA_Construction_def conjunction_imp
Subj_Reasoning_def
by (rule Is_Functional_imp''[where S'=S']; simp)
end
subsection ‹Automation›
named_theorems φsledgehammer_simps ‹Simplification rules used before applying slegehammer automation›
ML_file ‹library/tools/sledgehammer_solver.ML›
subsection ‹Ad-hoc Overload›
ML_file ‹library/system/app_rules.ML›
φoverloads cast
text ‹
Convention of Overloading Distance:
▪ 0. Transparent, the matching is perfect.
▪ 1. Almost Transparent, but still incomparable to the really transparent, meaning tiny cost still
exists, maybe in time or reasoning only
▪ 3. Expected Conversion: some conversion and therefore information lost is inevitable but it is
expected so can be accepted.
▪ 5. Less Expected Conversion: in some (rare) case the information lost can be severe
but generally still can be accepted for most of usages.
▪ 9. Slightly Aggressive.
▪ 12. Aggressive in most of the situations.
▪ 15. Bad.
Threshold Cost Always!
›
subsection ‹Synthesis›
text ‹The synthesis involves not only making a program but also finding a view shift or a ToA.
Given a target assertion ‹X› intended to be synthesized,
on a ready state of a construction like ‹𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 S› or ‹(𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S)›,
the mechanism synthesizes programs or deduces ToA to deduce the state sequent into
‹𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 X❟ S'› or ‹(𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 X❟ S')›.
On a state sequent having antecedents, e.g. ‹P ⟹ Q›, the synthesis mechanism solve the antecedent
‹P› according to the given specification from user.
For example, the ‹P› can be the specification of a procedure to be programmed, like the guard
‹P ≡ 𝗉𝗋𝗈𝖼 ?f ⦃ X ⟼ ?cond ⦂ 𝗏𝖺𝗅 𝔹 ⦄› of the branch statement. In this case
the mechanism is to synthesis that guard according to the user-given specification, like ‹$x > 2›
to synthesis ‹𝗉𝗋𝗈𝖼 ?f ⦃ X ⟼ $x > 2 ⦂ 𝗏𝖺𝗅 𝔹 ⦄›.
›
consts synthesis :: action
definition DoSynthesis :: ‹'a ⇒ prop ⇒ prop ⇒ prop›
where ‹DoSynthesis term sequent result ≡ (PROP sequent ⟹ PROP result)›
definition Synthesis_Parse :: ‹'a ⇒ 'b ⇒ bool›
where ‹Synthesis_Parse input parsed ⟷ True›
declare [[φreason_default_pattern ‹Synthesis_Parse ?in _› ⇒ ‹Synthesis_Parse ?in _› (100)]]
lemma φsynthesis:
‹ PROP sequent
⟹ PROP DoSynthesis X sequent result
⟹ PROP result›
unfolding DoSynthesis_def .
text ‹
Overall, the synthesis procedure consists of 2 phases.
The first phase is a pre-process parsing the user input. Performed by antecedent
\<^schematic_prop>‹Synthesis_Parse input ?parsed›,
it rewrites the user \<^term>‹input› to \<^schematic_term>‹?parsed›.
The rewrite process enables user to input partially instead of always giving the complete
assertion every time, for example, just the abstract object \<^term>‹x› to
denote \<^pattern_term>‹x ⦂ _› and leave the type unspecified to accept anything.
For example, user may input just an abstract object \<^term>‹x› to mean to
synthesis \<^term>‹x ⦂ T› for some unspecified \<^term>‹T›;
user may also input \<^term>‹0::nat› to mean to synthesis \<^term>‹0 ⦂ Natural_Number›.
One can disable φ_synthesis_parsing to disable this feature.
The second phase does the real work, synthesising the ‹?parsed›.
As the given specifications are on abstraction, ways to synthesis an abstract specification
are many and not uniquely determined syntactically of course.
Therefore we apply an A* algorithm according to explicitly annotated cost. The algorithm finds the
solution having the minimum cost.
Besides, in order to reduce the search space, we assume a large amount of operators having
specific programs to refine them (such as plus and subtract),
so that synthesising a composite expression can be split structurally (and syntactically) to
several small problems for synthesising its operands and for finding a proper program refining the operator.
To find such a proper instantiation requires to know the abstraction relations of the operands,
but it is not an easy problem because transformation of abstraction can happen at every application.
The choice of the abstraction relation of a sub-expression affects the synthesis of the inner
operations of the sub-expression and also the outer operation using it.
Choices of the intermediate abstraction relations have to be counted globally.
Therefore the synthesis reasoning also contains two phases. The first phase split the synthesis
problem for the original big composite expression down to several small problems of
choosing the intermediate abstraction relations and instantiating proper refinement for each
operators. And the second phase is an heuristic search finding the optimum choices
and the instantiations.
The first phase is a greedy algorithm as what we assumed.
The first-reached solution (according to the PLPR priority of the configured rules) is adopted
and the remains are dropped.
The second phase is exhaustive for every possible search branches (with pruning).
Candidates of the second phase are measured by the distance of the transformation used inside.
An ideal solution is to involve no transformation at all.
A transformation is an edge and each one is labelled with a distance manually.
The distance of a path ‹e⇩1;e⇩2;…;e⇩n› is the maximum distance of its edges (transformations),
‹max{e⇩i}›.
›
definition DoSynthesis_embed :: ‹'a ⇒ bool ⇒ bool ⇒ bool›
where ‹DoSynthesis_embed term sequent result ≡ (sequent ⟶ result)›
lemma [iso_atomize_rules, symmetric, iso_rulify_rules]:
‹DoSynthesis term (Trueprop sequent) (Trueprop result) ≡ Trueprop (DoSynthesis_embed term sequent result)›
unfolding DoSynthesis_def DoSynthesis_embed_def atomize_imp .
subsubsection ‹Conventions›
declare [[φreason_default_pattern
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag synthesis› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag synthesis› (100)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag synthesis› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag synthesis› (110)
and ‹(?X::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis› ⇒
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis› (100)
and ‹(?X::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis› ⇒
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis› (110)
and ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag synthesis› ⇒
‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag synthesis› (100)
and ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag synthesis› ⇒
‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag synthesis› (100)
and ‹?X @tag synthesis› ⇒
‹ERROR TEXT(‹Malformed Synthesis rule› ⏎ ?X)› (0)
]]
φreasoner_group φsynthesis_all = (100, [1, 3000]) for ‹_ @tag synthesis›
‹Rules implementing Synthesis mechanism of IDE-CP›
and φsynthesis_red = (2500, [2500, 2799]) in φsynthesis_all
‹Reductions and Evaluations›
and φsynthesis = (100, [10, 500]) in φsynthesis_all
‹usual rules›
and φsynthesis_literal = (470, [450, 500]) in φsynthesis
‹literal›
and φsynthesis_fallback = (9, [9,9]) in φsynthesis_all and < φsynthesis
‹fallbacks›
and φsynthesis_cut = (1000, [1000, 1500]) in φsynthesis_all and > φsynthesis and < φsynthesis_red
‹cutting rules›
and φsynthesis_split = (1530, [1530, 1550]) in φsynthesis_all and > φsynthesis_cut
‹Splitting the targets into each sub-reasoning goal›
and φsynthesis_normalize = (2000, [2000,2400]) in φsynthesis_all and > φsynthesis_split
‹normalization›
and φsynthesis_weak_normalize = (800, [800,900]) in φsynthesis_all and < φsynthesis_cut
‹normalization with backtracking›
and interp_φsynthesis = (%cutting, [%cutting, %cutting+30]) for ‹PROP DoSynthesis _ _ _›
‹describing how to carry out the synthesis in detail on specific IDE-CP sequent›
and φsynthesis_parse_all = (1000, [10, 3000]) for ‹Synthesis_Parse input parsed›
‹Synthesis Parsing›
and φsynthesis_parse = (1000, [1000, 1030]) in φsynthesis_parse_all
‹usual rules›
and φsynthesis_parse_success = (3000, [3000, 3000]) in φsynthesis_parse_all and > φsynthesis_parse
‹direct success›
and φsynthesis_parse_default = (10, [10,29]) in φsynthesis_parse_all and < φsynthesis_parse
‹default parsing›
and φsynthesis_parse_number = (40, [30, 70]) in φsynthesis_parse_all
and < φsynthesis_parse and > φsynthesis_parse_default
‹parsing numbers›
and φsynthesis_parse_guess_literal_type = (60, [60, 60]) in φsynthesis_parse_number
‹see Guess_Literal_Type_Synthesis_Parse›
subsubsection ‹Parse the Term to be Synthesised›
lemma [φreason %φsynthesis_parse_success for
‹Synthesis_Parse (?X'::?'ret ⇒ assn) (?X::?'ret ⇒ assn)›
‹Synthesis_Parse (?X'::?'c BI) (?X::?'c BI)›
]:
‹Synthesis_Parse X X›
unfolding Synthesis_Parse_def ..
lemma [
φreason %φsynthesis_parse_success for
‹Synthesis_Parse (?X'::assn) (?X::?'ret ⇒ assn)›,
φreason default %φsynthesis_parse_default for
‹Synthesis_Parse (?X'::?'a BI) (?X::?'ret ⇒ assn)›
]:
‹Synthesis_Parse X (λ_. X)› for X :: ‹assn›
unfolding Synthesis_Parse_def ..
lemma [φreason default %φsynthesis_parse_default
for ‹Synthesis_Parse ?x (?Y::?'ret ⇒ assn)›
except ‹Synthesis_Parse (?x ⦂ ?T) ?Y›
‹Synthesis_Parse (?x::assn) ?Y›
‹Synthesis_Parse (?x::?'ret ⇒ assn) ?Y›
]:
‹Synthesis_Parse x (λret. (x ⦂ 𝗏𝖺𝗅[ret] X :: assn))›
unfolding Synthesis_Parse_def ..
lemma [φreason default %φsynthesis_parse_default]:
‹Synthesis_Parse T (x ⦂ T)›
unfolding Synthesis_Parse_def ..
lemma [φreason default %φsynthesis_parse_default+10
for ‹Synthesis_Parse (numeral ?n::?'bb::numeral) ?X›
‹Synthesis_Parse (0::?'cc::zero) ?X›
‹Synthesis_Parse (1::?'dd::one) ?X›
except ‹Synthesis_Parse (?n::nat) ?X›
]:
‹ Synthesis_Parse (n :: nat) X
⟹ Synthesis_Parse n X›
unfolding Synthesis_Parse_def
..
lemma [φreason default %φsynthesis_parse_default+10 for ‹Synthesis_Parse (?T :: ?'ret2 ⇒ (fiction,?'x) φ) (?Y::?'ret ⇒ assn)›]:
‹ Synthesis_Parse T (λret. x ⦂ T ret :: assn) ›
unfolding Synthesis_Parse_def ..
lemma [φreason default %φsynthesis_parse_default+10 for ‹Synthesis_Parse (?T :: (fiction,?'x) φ) (?Y::?'ret ⇒ assn)›]:
‹ Synthesis_Parse T (λret. x ⦂ T :: assn) ›
unfolding Synthesis_Parse_def ..
subsubsection ‹Guess the ‹φ›-Type of Literals›
ML_file ‹library/tools/guess_literal_number_type.ML›
φreasoner_ML Guess_Literal_Type_Synthesis_Parse %φsynthesis_parse_guess_literal_type
(‹Synthesis_Parse _ (?X :: ?'ret ⇒ assn)›)
= ‹fn (_, (ctxt,sequent)) => Seq.make (fn () =>
let val (bvtys, _ $ (Const(\<^const_name>‹Synthesis_Parse›, _) $ literal $ X))
= Phi_Help.strip_meta_hhf_bvtys (Phi_Help.leading_antecedent' sequent)
val time = Phi_Envir.the_time ctxt
in if Phi_Type_of_Literal.is_literal literal
then Phi_Type_of_Literal.guess ctxt bvtys time literal
|> Option.map (fn phi_type =>
((ctxt,
\<^instantiate>‹ T=phi_type
and n=‹Thm.var (("n", Thm.maxidx_of_cterm phi_type + 1),
Thm.dest_ctyp0 (Thm.ctyp_of_cterm phi_type))›
and X=‹Thm.cterm_of ctxt X›
and 'c=‹Thm.dest_ctyp0 (Thm.dest_ctyp1 (Thm.ctyp_of_cterm phi_type))›
and 'x=‹Thm.dest_ctyp0 (Thm.ctyp_of_cterm phi_type)›
and 'any=‹Thm.ctyp_of ctxt (Term.fastype_of1 (bvtys, X))›
in lemma ‹ Synthesis_Parse (n ⦂ T) X
⟹ Synthesis_Parse n X ›
for T :: ‹('c,'x) φ› and X :: ‹'any›
by (simp add: Synthesis_Parse_def) › RS sequent), Seq.empty))
else NONE
end )›
subsubsection ‹Tagging the target of a synthesis rule›
text ‹
Only procedure rules need to be tagged by \<^const>‹synthesis›. The view shift and the ToA do not.
Occurring in the post-condition of a rule (either a procedure specification or a view shift
or an implication), SYNTHESIS tags the target of the rule, i.e., the construct that this
procedure or this transformation synthesises.
For example, \<^prop>‹𝗉𝗋𝗈𝖼 f ⦃ X ⟼ λret. Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Y ⦄ @tag synthesis›
represents the procedure f generates
something that meets Z, and it is a synthesis rule for synthesising the target ‹Z›.
Occurring during reasoning, antecedent like
\<^schematic_prop>‹𝗉𝗋𝗈𝖼 ?f ⦃ X ⟼ λret. Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Y ⦄ @tag synthesis ⟹ C›,
represents a reasoning task to find some procedure or some transformation to synthesis
something meeting Z.
TODO: update the comment.
›
subsubsection ‹Synthesis Operations›
paragraph ‹Fallback›
text ‹On programming mode, the synthesis operation always tries to find a procedure.
View shifts have to be wrapped in a procedure. The following is an automatic wrapper. ›
lemma Synthesis_Proc_fallback_VS
[φreason default %φsynthesis_fallback for ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λv. ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag synthesis›]:
‹ S1 𝗌𝗁𝗂𝖿𝗍𝗌 X' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 S2 𝗐𝗂𝗍𝗁 Any
⟹ 𝗉𝗋𝗈𝖼 Return φV_none ⦃ S1 ⟼ λv. X' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 S2 ⦄ @tag synthesis›
unfolding φProcedure_def Return_def det_lift_def View_Shift_def Action_Tag_def less_eq_BI_iff
by simp
lemma [φreason default %φsynthesis_fallback]:
‹ A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 B 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag synthesis
⟹ A 𝗌𝗁𝗂𝖿𝗍𝗌 B 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag synthesis ›
unfolding Action_Tag_def
using view_shift_by_implication .
paragraph ‹Construction on Programming›
lemma [φreason %interp_φsynthesis
for ‹PROP DoSynthesis ?X (Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?S1)) ?RET›
]:
" 𝗋CALL Synthesis_Parse X X'
⟹ Begin_Optimum_Solution
⟹ 𝗉𝗋𝗈𝖼 f ⦃ S1 ⟼ λv. X' v 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 S2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis
⟹ End_Optimum_Solution
⟹ (⋀v. 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] (X'' v, E'') : (X' v, E))
⟹ 𝗋Success
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP DoSynthesis X
(Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 S1))
(Trueprop (𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f 𝗈𝗇 blk [H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 (λv. X'' v * S2) 𝗍𝗁𝗋𝗈𝗐𝗌 E''))"
unfolding REMAINS_def Action_Tag_def DoSynthesis_def Simplify_def
using φapply_proc by fastforce
paragraph ‹Construction on View Shifting›
text ‹On view shifting mode, the synthesis operation tries to find a view shifting.›
lemma [φreason %interp_φsynthesis
for ‹PROP DoSynthesis ?X (Trueprop (𝗏𝗂𝖾𝗐 ?blk [?H] 𝗂𝗌 ?S1)) ?RET›
]:
" 𝗋CALL Synthesis_Parse X X'
⟹ S1 𝗌𝗁𝗂𝖿𝗍𝗌 X' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 S2 𝗐𝗂𝗍𝗁 P
⟹ 𝗋Success
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X'' : X'
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP DoSynthesis X
(Trueprop (𝗏𝗂𝖾𝗐 blk [H] 𝗂𝗌 S1))
(Trueprop ((𝗏𝗂𝖾𝗐 blk [H] 𝗂𝗌 X'' * S2) ∧ P))"
unfolding REMAINS_def Action_Tag_def DoSynthesis_def Simplify_def
using φapply_view_shift
by metis
paragraph ‹Construction on ToA›
lemma [φreason %interp_φsynthesis+10
for ‹PROP DoSynthesis ?X (Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(?x) 𝗂𝗌 (?S1::?'c::sep_magma_1 BI))) ?RET›
]:
" 𝗋CALL Synthesis_Parse X X'
⟹ S1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 S2 𝗐𝗂𝗍𝗁 P
⟹ 𝗋Success
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X'' : X'
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP DoSynthesis X
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S1))
(Trueprop ((𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 X'' * S2) ∧ P))"
unfolding REMAINS_def Action_Tag_def DoSynthesis_def Simplify_def
by (meson φapply_implication_impl)
lemma [φreason %interp_φsynthesis
for ‹PROP DoSynthesis ?X (Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(?x) 𝗂𝗌 ?S1)) ?RET›
]:
" 𝗋CALL Synthesis_Parse X X'
⟹ Ψ[Some] S1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Ψ[Some] X' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 S2 𝗐𝗂𝗍𝗁 P
⟹ Ψ[Some] X' * S2 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Ψ[Some] RET @clean
⟹ 𝗋Success
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] RET' : RET
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP DoSynthesis X
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S1))
(Trueprop ((𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 RET') ∧ P))"
unfolding REMAINS_def Action_Tag_def DoSynthesis_def Simplify_def
by (smt (verit) ToA_Construction_def Transformation_def World_Shift_expn option.inject)
paragraph ‹Solving an antecedent by Synthesis›
definition Synthesis_by :: ‹'a ⇒ prop ⇒ prop›
where ‹Synthesis_by X Q ≡ Q›
text ‹If the synthesis procedure is invoked on an inference rule like \<^prop>‹P ⟹ Q›,
it invokes the Synthesis_by procedure which tries to solve the antecedent \<^prop>‹P›
under the instruction of the given \<^term>‹X› to be synthesised,
by reasoning antecedent \<^prop>‹PROP Synthesis_by X P›.
Note the procedure of Synthesis_by will not trigger Synthesis_Parse because this
generic procedure does not the type to be synthesised. Lacking of this type information
affects the preciseness of Synthesis_Parse rule. The procedure of Synthesis_Parse
should be triggered at the entry point of each specific operation, where the expected type
is clear.›
definition Synthesis_by_embed :: ‹'a ⇒ bool ⇒ bool› where ‹Synthesis_by_embed X Q ≡ Q›
lemma [iso_atomize_rules, symmetric, iso_rulify_rules]:
‹Synthesis_by X (Trueprop P) ≡ Trueprop (Synthesis_by_embed X P)›
unfolding Synthesis_by_embed_def Synthesis_by_def .
declare [[φreason_default_pattern ‹PROP Synthesis_by ?X ?Q› ⇒ ‹PROP Synthesis_by ?X ?Q› (100)]]
φreasoner_group φant_by_synthesis_all = (1000, [1,3000]) for ‹PROP Synthesis_by X Ant›
‹how to solve an antecedent ‹Ant› with the annotated synthesis target ‹X››
and φant_by_synthesis = (1000, [1000,1030]) in φant_by_synthesis_all
‹cutting rules›
and φant_by_synthesis_red = (2500, [2500, 2800]) in φant_by_synthesis_all and > φant_by_synthesis
‹Reduction or Evaluation›
lemma [φreason %interp_φsynthesis
for ‹PROP DoSynthesis ?X (PROP ?P ⟹ PROP ?Q) ?RET›
]:
" PROP Synthesis_by X (PROP P)
⟹ 𝗋Success
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP DoSynthesis X (PROP P ⟹ PROP Q) (PROP Q)"
unfolding DoSynthesis_def Synthesis_by_def Action_Tag_def .
lemma [φreason %φant_by_synthesis]:
‹(⋀x. PROP Synthesis_by X (PROP P x))
⟹ PROP Synthesis_by X (⋀x. PROP P x)›
unfolding Synthesis_by_def .
lemma [φreason %φant_by_synthesis]:
‹(PROP P ⟹ PROP Synthesis_by X (PROP Q))
⟹ PROP Synthesis_by X (PROP P ⟹ PROP Q)›
unfolding Synthesis_by_def .
lemma [φreason %φant_by_synthesis]:
‹ 𝗋CALL Synthesis_Parse A A'
⟹ Begin_Optimum_Solution
⟹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ λret. A' ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E' @tag synthesis
⟹ End_Optimum_Solution
⟹ (⋀ret. 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] (A'' ret, E'') : (A' ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R, E'))
⟹ (⋀ret. A'' ret 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y ret)
⟹ (⋀e. E'' e 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 E e)
⟹ PROP Synthesis_by A (Trueprop (𝗉𝗋𝗈𝖼 f ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ))›
unfolding Synthesis_by_def Action_Tag_def Simplify_def
by (simp, meson "_φcast_proc_exception_internal_rule_" "_φcast_proc_return_internal_rule_" Action_Tag_def Premise_True 𝗋Success_I)
lemma [φreason %φant_by_synthesis]:
‹ (⋀x. PROP Synthesis_by X (Trueprop (P x)))
⟹ PROP Synthesis_by X (Trueprop (All P))›
unfolding Synthesis_by_def Action_Tag_def ..
lemma [φreason %φant_by_synthesis]:
‹ (P ⟹ PROP Synthesis_by X (Trueprop Q))
⟹ PROP Synthesis_by X (Trueprop (P ⟶ Q))›
unfolding Synthesis_by_def Action_Tag_def ..
subsubsection ‹General Synthesis Rules›
lemma [φreason %φant_by_synthesis_red]:
‹ 𝗉𝗋𝗈𝖼 F ⦃ R1 ⟼ λret. f x ⦂ T ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 F ⦃ R1 ⟼ λret. case_named f (tag x) ⦂ T ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ @tag synthesis›
by simp
lemma [φreason %φant_by_synthesis_red]:
‹ PROP Synthesis_by X (Trueprop P)
⟹ PROP Synthesis_by X (Trueprop (𝗎𝗌𝖾𝗋 P))›
unfolding Argument_def .
lemma [φreason %φant_by_synthesis_red]:
‹ PROP Synthesis_by X (PROP P)
⟹ PROP Synthesis_by X (PROP (Argument P))›
unfolding Argument_def .
lemma [φreason %φant_by_synthesis for ‹PROP Synthesis_by ?X (Trueprop (_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?X' 𝗐𝗂𝗍𝗁 _))›]:
‹ A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X 𝗐𝗂𝗍𝗁 P
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X' : X
⟹ PROP Synthesis_by X (Trueprop (A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X' 𝗐𝗂𝗍𝗁 P))›
unfolding Synthesis_by_def Simplify_def by meson
lemma [φreason %φant_by_synthesis for ‹PROP Synthesis_by ?X (Trueprop (_ 𝗌𝗁𝗂𝖿𝗍𝗌 ?X' 𝗐𝗂𝗍𝗁 _))›]:
‹ A 𝗌𝗁𝗂𝖿𝗍𝗌 X 𝗐𝗂𝗍𝗁 P
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X' : X
⟹ PROP Synthesis_by X (Trueprop (A 𝗌𝗁𝗂𝖿𝗍𝗌 X' 𝗐𝗂𝗍𝗁 P))›
unfolding Synthesis_by_def Simplify_def by meson
lemma [φreason %φant_by_synthesis for ‹PROP Synthesis_by ?X (⋀a. _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 ?P)›]:
‹ (⋀a. A a 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X a 𝗐𝗂𝗍𝗁 P)
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X' : X
⟹ PROP Synthesis_by X (⋀a. A a 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X' a 𝗐𝗂𝗍𝗁 P)›
unfolding Synthesis_by_def Simplify_def by meson
lemma [φreason %φant_by_synthesis for ‹PROP Synthesis_by ?X (⋀a. ?A a 𝗌𝗁𝗂𝖿𝗍𝗌 ?B a 𝗐𝗂𝗍𝗁 ?P)›]:
‹ (⋀a. A a 𝗌𝗁𝗂𝖿𝗍𝗌 X a 𝗐𝗂𝗍𝗁 P)
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X' : X
⟹ PROP Synthesis_by X (⋀a. A a 𝗌𝗁𝗂𝖿𝗍𝗌 X' a 𝗐𝗂𝗍𝗁 P)›
unfolding Synthesis_by_def Simplify_def by meson
lemma [φreason %φant_by_synthesis for ‹PROP Synthesis_by ?X (⋀a. 𝗎𝗌𝖾𝗋 _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 ?P)›]:
‹ (⋀a. A a 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X a 𝗐𝗂𝗍𝗁 P)
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X' : X
⟹ PROP Synthesis_by X (⋀a. 𝗎𝗌𝖾𝗋 A a 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X' a 𝗐𝗂𝗍𝗁 P)›
unfolding Synthesis_by_def Argument_def Simplify_def by meson
lemma [φreason %φant_by_synthesis for ‹PROP Synthesis_by ?X (⋀a. 𝗎𝗌𝖾𝗋 ?A a 𝗌𝗁𝗂𝖿𝗍𝗌 ?B a 𝗐𝗂𝗍𝗁 ?P)›]:
‹ (⋀a. A a 𝗌𝗁𝗂𝖿𝗍𝗌 X a 𝗐𝗂𝗍𝗁 P)
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[programming_mode] X' : X
⟹ PROP Synthesis_by X (⋀a. 𝗎𝗌𝖾𝗋 A a 𝗌𝗁𝗂𝖿𝗍𝗌 X' a 𝗐𝗂𝗍𝗁 P)›
unfolding Synthesis_by_def Argument_def Simplify_def by meson
subsection ‹Application›
text ‹It is a generic framework allowing to apply general things on the state sequent.
These general things named ∗‹application› includes
▪ procedures --- therefore appending a procedure on the current construction
▪ transformations of abstraction and view shifts --- transforming the abstract state
▪ actions --- meta operations combining several applications or transformations, cf. section Action.
›
definition φApplication :: ‹prop ⇒ prop ⇒ prop ⇒ prop›
where ‹φApplication App_Rules State Result
≡ (PROP State ⟹ PROP App_Rules ⟹ PROP Result)›
lemma φapplication:
‹ PROP Apps
⟹ PROP State
⟹ PROP φApplication Apps State Result
⟹ 𝗋Success
⟹ PROP Result›
unfolding φApplication_def Pure.prop_def Optimum_Solution_def Optimum_Among_def .
definition φApplication_Conv :: ‹prop ⇒ prop ⇒ prop›
where ‹φApplication_Conv ≡ (⟹)›
definition φApp_Conv :: ‹bool ⇒ bool ⇒ bool›
where ‹φApp_Conv ≡ (⟶)›
lemma φApplication_Conv:
‹ PROP P
⟹ PROP φApplication_Conv P Q
⟹ 𝗋Success
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP Q›
unfolding φApplication_Conv_def .
ML_file ‹library/system/application.ML›
φreasoner_group φapplication_all = (1000, [10,3000]) for (‹PROP φApplication Apps State Result›)
‹describs how to apply ‹Apps› over ‹State››
and φapplication_traverse_apps = (70, [70,70]) in φapplication_all
‹attemps each application candidate in order›
and φapplication = (1000, [1000, 1100]) in φapplication_all > φapplication_traverse_apps
‹usual cutting rules›
and φapp_conv_all = (1000, [0,3000]) for (‹(PROP φApplication_Conv Antcedent Consequent)›,
‹φApp_Conv Antcedent Consequent›)
‹application as converting ‹Antecedent› to ‹Consequent››
and φapp_conv_success = (3000, [3000,3000]) in φapp_conv_all
‹direct success›
and φapp_conv_normalize = (2000, [2000,2300]) in φapp_conv_all and < φapp_conv_success
‹normalization rules›
and φapp_conv = (1000, [1000,1200]) in φapp_conv_all and < φapp_conv_normalize
‹usual cutting rules›
and φapp_conv_derived = (50, [50, 60]) in φapp_conv_all and < φapp_conv
‹derived rules›
and φapp_conv_failure = (0, [0,0]) in φapp_conv_all and < φapp_conv_derived
‹failures›
declare [[
φreason_default_pattern ‹PROP φApplication ?Apps ?State _› ⇒ ‹PROP φApplication ?Apps ?State _› (100),
φdefault_reasoner_group ‹PROP φApplication _ _ _› : %φapplication (100)
]]
subsubsection ‹Common Rules of Application Methods›
context begin
private lemma φApp_L:
‹ PROP φApplication (PROP App) State (PROP Result)
⟹ PROP φApplication (PROP App &&& PROP Apps) State (PROP Result)›
unfolding prop_def φApplication_def conjunction_imp .
private lemma φApp_R:
‹ PROP φApplication (PROP Apps) State (PROP Result)
⟹ PROP φApplication (PROP App &&& PROP Apps) State (PROP Result)›
unfolding prop_def φApplication_def conjunction_imp .
declare [[
φreason %φapplication_traverse_apps φApp_L φApp_R
for ‹PROP φApplication (PROP ?App &&& PROP ?Apps) ?State ?Result›
]]
end
lemma φapply_eager_antecedent_meta:
‹ PROP φApplication (PROP App) State (PROP Result)
⟹ PROP Prem
⟹ PROP φApplication (PROP Prem ⟹ PROP App) State (PROP Result)›
unfolding prop_def φApplication_def imp_implication
subgoal premises prems using prems(1)[OF prems(3) prems(4)[OF prems(2)]] . .
lemma φapply_eager_antecedent:
‹ PROP φApplication (Trueprop App) State (PROP Result)
⟹ Prem
⟹ PROP φApplication (Trueprop (Prem ⟶ App)) State (PROP Result)›
unfolding prop_def φApplication_def imp_implication
subgoal premises prems using prems(1)[OF prems(3) prems(4)[OF prems(2)]] . .
lemma φapply_user_antecedent_meta:
‹ PROP φApplication (PROP App) State (PROP Result)
⟹ PROP φApplication (PROP Prem ⟹ PROP App) State (PROP Prem ⟹ PROP Result)›
unfolding prop_def φApplication_def imp_implication
subgoal premises prems using prems(1)[OF prems(2) prems(3)[OF prems(4)]] . .
lemma φapply_user_antecedent:
‹ PROP φApplication (Trueprop App) State Result
⟹ PROP φApplication (Trueprop (Prem ⟶ App)) State (Prem ⟹ PROP Result)›
unfolding prop_def φApplication_def imp_implication
subgoal premises prems using prems(1)[OF prems(2) prems(3)[OF prems(4)]] . .
φreasoner_ML φapply_admit_antecedent %φapplication
( ‹PROP φApplication (PROP ?Prem ⟹ PROP ?App) ?State ?Result›
| ‹PROP φApplication (Trueprop (?Prem' ⟶ ?App')) ?State ?Result› )
= ‹fn (_, (ctxt,sequent)) => Seq.make (fn () =>
let val _ $ app $ _ $ _ = Thm.major_prem_of sequent
val (user_rule, eager_rule) =
case app of Const(\<^const_name>‹Trueprop›, _) $ _ =>
(@{thm φapply_user_antecedent}, @{thm φapply_eager_antecedent})
| Const(\<^const_name>‹Pure.imp›, _) $ _ $ _ =>
(@{thm φapply_user_antecedent_meta}, @{thm φapply_eager_antecedent_meta})
fun process (Const(\<^const_name>‹Trueprop›, _) $ X) met_sequent = process X met_sequent
| process (Const(\<^const_name>‹Pure.imp›, _) $ A $ X) (met,eager,sequent) =
process X (if met > 0 orelse Phi_Sys_Reasoner.is_user_dependent_antecedent A
then (met + 1, eager, user_rule RS sequent)
else (met, eager + 1, eager_rule RS sequent))
| process (Const(\<^const_name>‹HOL.implies›, _) $ A $ X) (met,eager,sequent) =
process X (if met > 0 orelse Phi_Sys_Reasoner.is_user_dependent_antecedent A
then (met + 1, eager, user_rule RS sequent)
else (met, eager + 1, eager_rule RS sequent))
| process _ sequent = sequent
val (_, eager, sequent') = process app (0,0,sequent)
val N = Thm.nprems_of sequent'
val sequent'2 =
if eager <= 1 then sequent'
else let val sequent'3 = Thm.permute_prems 1 (eager-1) sequent'
fun perm i sqt = if i = eager + 1 then sqt
else perm (i+1) (Thm.permute_prems i (N-i-1) sqt)
in perm 2 sequent'3 end
in SOME ((ctxt, sequent'2), Seq.empty)
end
) ›
lemma [φreason %φapplication]:
‹ PROP φApplication (Trueprop App) State (PROP Result)
⟹ PROP φApplication (Trueprop (App @tag Act)) State (PROP Result)›
unfolding prop_def φApplication_def Action_Tag_def
subgoal premises prems using prems(1)[OF prems(2) prems(3)] . .
lemma [φreason %φapplication]:
‹ PROP φApplication (PROP App x) State (PROP Result)
⟹ PROP φApplication (⋀x. PROP App x) State (PROP Result)›
unfolding φApplication_def
proof -
assume p1: ‹PROP State ⟹ PROP App x ⟹ PROP Result›
and p2: ‹PROP State›
and p3: ‹⋀x. PROP App x›
show ‹PROP Result›
by (rule p1, rule p2, rule p3)
qed
lemma [φreason %φapplication+100]:
‹ PROP φApplication (⋀a. PROP App (φV_pair x a)) State (PROP Result)
⟹ PROP φApplication (⋀x. PROP App x) State (PROP Result)›
unfolding φApplication_def
proof -
assume p1: ‹PROP State ⟹ (⋀a. PROP App (x❙, a)) ⟹ PROP Result›
and p2: ‹PROP State›
and p3: ‹⋀x. PROP App x›
show ‹PROP Result›
by (rule p1, rule p2, rule p3)
qed
lemma [φreason %φapplication]:
‹ PROP φApplication (Trueprop (App x)) State (PROP Result)
⟹ PROP φApplication (Trueprop (All App)) State (PROP Result)›
unfolding φApplication_def
subgoal premises p by (rule p(1), rule p(2), rule p(3)[THEN spec[where x=x]]) .
lemma [φreason %φapplication+100]:
‹ PROP φApplication (Trueprop (∀a. App (φV_pair x a))) State (PROP Result)
⟹ PROP φApplication (Trueprop (All App)) State (PROP Result)›
unfolding φApplication_def
subgoal premises p by (rule p(1), rule p(2), rule, rule p(3)[THEN spec]) .
lemma [φreason %φapplication]:
‹ PROP φApplication (Trueprop (X = Y)) S (PROP R)
⟹ PROP φApplication (X ≡ Y) S (PROP R) ›
unfolding atomize_eq .
subsubsection ‹Application as a Resolution›
lemma [φreason %φapplication]:
‹ PROP φApplication_Conv X' X
⟹ PROP φApplication X' (PROP X ⟹ PROP Y) Y›
unfolding φApplication_def φApplication_Conv_def
subgoal premises prems using prems(3)[THEN prems(1), THEN prems(2)] . .
lemma [φreason %φapplication]:
‹ φApp_Conv X' X
⟹ PROP φApplication (Trueprop X') (Trueprop (X ⟶ Y)) (Trueprop Y)›
unfolding φApplication_def φApplication_Conv_def φApp_Conv_def
by blast
subsubsection ‹Conversion of Applying Rule›
paragraph ‹By ‹φApp_Conv››
subparagraph ‹Basic Rules›
lemma [φreason %φapp_conv_success]:
‹ φApp_Conv X Y
⟹ PROP φApplication_Conv (Trueprop X) (Trueprop Y)›
unfolding φApplication_Conv_def φApp_Conv_def
by blast
subparagraph ‹Direct Success›
lemma [φreason %φapp_conv_success for ‹PROP φApplication_Conv (PROP ?X) (PROP ?X')›]:
‹PROP φApplication_Conv (PROP X) (PROP X)›
unfolding φApplication_Conv_def .
lemma [φreason %φapp_conv_success for ‹φApp_Conv ?X ?X'›]:
‹φApp_Conv X X›
unfolding φApp_Conv_def ..
subparagraph ‹Over Logic Connectives›
lemma [φreason %φapp_conv]:
‹ PROP φApplication_Conv (A x) X
⟹ PROP φApplication_Conv (Pure.all A) X›
unfolding φApplication_Conv_def
proof -
assume A: ‹PROP A x ⟹ PROP X›
and B: ‹⋀x. PROP A x›
from A[OF B[of x]] show ‹PROP X› .
qed
lemma [φreason %φapp_conv]:
‹ φApp_Conv (A x) X
⟹ φApp_Conv (All A) X›
unfolding φApp_Conv_def
by blast
lemma [φreason %φapp_conv_normalize]:
‹ (⋀x. PROP φApplication_Conv X (Y x))
⟹ PROP φApplication_Conv X (Pure.all Y) ›
unfolding φApplication_Conv_def
apply (simp add: norm_hhf_eq)
subgoal premises prems for x
by (rule prems(1), rule prems(2)) .
lemma [φreason %φapp_conv_normalize]:
‹ (⋀x. φApp_Conv X (Y x))
⟹ φApp_Conv X (∀x. Y x)›
unfolding φApp_Conv_def
by blast
lemma [φreason %φapp_conv]:
‹ PROP May_By_Assumption X
⟹ PROP φApplication_Conv A Y
⟹ PROP φApplication_Conv (PROP X ⟹ PROP A) Y›
unfolding φApplication_Conv_def May_By_Assumption_def
subgoal premises p using p(1)[THEN p(3), THEN p(2)] . .
lemma [φreason %φapp_conv_normalize]:
‹ (PROP A ⟹ PROP φApplication_Conv X Y)
⟹ PROP φApplication_Conv (PROP X) (PROP A ⟹ PROP Y)›
unfolding φApplication_Conv_def
subgoal premises prems
by (rule prems(1), rule prems(3), rule prems(2)) .
lemma [φreason %φapp_conv]:
‹ PROP May_By_Assumption (Trueprop A)
⟹ φApp_Conv X Y
⟹ φApp_Conv (A ⟶ X) Y›
unfolding φApp_Conv_def May_By_Assumption_def
by blast
lemma [φreason %φapp_conv_normalize]:
‹ (A ⟹ φApp_Conv X Y)
⟹ φApp_Conv X (A ⟶ Y)›
unfolding φApp_Conv_def
by blast
paragraph ‹Reduction›
lemma [φreason %φapp_conv]:
‹ φApp_Conv X Y
⟹ φApp_Conv X (Y @tag A)›
unfolding Action_Tag_def .
lemma [φreason %φapp_conv]:
‹ φApp_Conv Y X
⟹ φApp_Conv (Y @tag A) X›
unfolding Action_Tag_def .
lemma [φreason %φapp_conv]:
‹ φApp_Conv Y X
⟹ φApp_Conv (TECHNICAL Y) X ›
unfolding Technical_def .
lemma [φreason %φapp_conv]:
‹ φApp_Conv Y X
⟹ φApp_Conv Y (TECHNICAL X) ›
unfolding Technical_def .
paragraph ‹Specifically for ToA›
definition ToA_App_Conv :: ‹'ca itself ⇒ 'c itself ⇒ ('c, 'a) φ ⇒ bool ⇒ bool ⇒ bool›
where ‹ToA_App_Conv _ _ T App Converted ≡ App ⟶ Converted›
declare [[φreason_default_pattern ‹ToA_App_Conv ?TYa ?TY ?T' (?x ⦂ ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P) (_ ⦂ _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ _ 𝗐𝗂𝗍𝗁 _)› ⇒
‹ToA_App_Conv ?TYa ?TY ?T' (?x ⦂ ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P) (_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _)› (100)
and ‹ToA_App_Conv ?TYa ?TY ?T' ?var_X (_ ⦂ _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ _ 𝗐𝗂𝗍𝗁 _)› ⇒
‹ToA_App_Conv ?TYa ?TY ?T' ?X (_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _)› (100)
and ‹ToA_App_Conv ?TYa ?TY ?T' (∀a. ?Q a ⟶ (a ⦂ ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P)) (_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _)› ⇒
‹ToA_App_Conv ?TYa ?TY ?T' (∀a. ?Q a ⟶ (a ⦂ ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P)) (_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _)› (100)
and ‹ToA_App_Conv ?TYa ?TY ?T' ?App ?C› ⇒
‹ERROR TEXT(‹Bad rule› (ToA_App_Conv ?TYa ?TY ?T ?App ?C))› (0)]]
subparagraph ‹Basic Rules›
lemma [φreason %φapp_conv_success for ‹ToA_App_Conv ?TY ?TY' ?T ?App _›]:
‹ ToA_App_Conv TY TY T App App ›
unfolding ToA_App_Conv_def
by blast
subparagraph ‹Failure›
lemma [φreason default %φapp_conv_failure for ‹ToA_App_Conv _ _ _ (_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _) (_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _)›]:
‹ ERROR TEXT(‹The programming is working on algbera› TYPE('c) ‹but the applying ToA is on› TYPE('c⇩a)
‹I don't know how to convert› (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P))
⟹ ToA_App_Conv TYPE('c⇩a) TYPE('c) T (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P) (X' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P') ›
for X :: ‹'c⇩a BI› and X' :: ‹'c BI›
unfolding ERROR_def
by blast
subsubsection ‹Application on Procedure Mode›
text ‹TODO: move this to user manual.
\begin{convention}
In an application, source \<^schematic_term>‹?X› denotes the pattern matching the whole state
and the frame rule is not used by which \<^schematic_term>‹?X› can actually match any leading items,
whereas source \<^schematic_term>‹?x ⦂ ?T› matches only the first φ-type.
In this way, we differentiate the representation of the purpose for transforming the whole state
and that for only the single leading item.
\end{convention}
\begin{convention}
The construction in a ready state should always be specified by a simple MTF.
\end{convention}
›
φreasoner_group φapp_on_proc_or_VS = (1000, [1000,2000])
for ‹PROP φApplication App (Trueprop (CurrentConstruction mode blk R S)) Result›
in φapplication_all and > φapplication_traverse_apps
‹applications in construction process of procedures›
and φapp_ToA_on_proc_or_VS = (1000, [1000,1200])
for ‹PROP φApplication (Trueprop (S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T 𝗐𝗂𝗍𝗁 P)) (Trueprop (CurrentConstruction mode blk R S)) Result›
in φapp_on_proc_or_VS
‹applying ToA›
and φapp_VS_on_proc_or_VS = (1000, [1000,1200])
for ‹PROP φApplication (Trueprop (S 𝗌𝗁𝗂𝖿𝗍𝗌 T 𝗐𝗂𝗍𝗁 P)) (Trueprop (CurrentConstruction mode blk R S)) Result›
in φapp_on_proc_or_VS
‹applying VS›
and φapp_proc_on_proc_or_VS = (1000, [1000,1200])
for ‹PROP φApplication (Trueprop (𝗉𝗋𝗈𝖼 f ⦃ S ⟼ T ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ))
(Trueprop (CurrentConstruction mode blk R S)) Result›
‹applying procedures›
paragraph ‹Transformation Methods›
subparagraph ‹Shortcuts›
lemma [φreason %φapp_ToA_on_proc_or_VS+110
for ‹PROP φApplication (Trueprop (?S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (CurrentConstruction ?mode ?blk ?R ?S))
(PROP _)›
‹PROP φApplication (Trueprop (?var 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (CurrentConstruction ?mode ?blk ?R ?S))
(PROP _)› ]:
‹ PROP φApplication (Trueprop (S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (CurrentConstruction mode blk R S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk R T) ∧ P)›
unfolding φApplication_def
using φapply_implication .
lemma [φreason %φapp_ToA_on_proc_or_VS+100
for ‹PROP φApplication (Trueprop (?S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (CurrentConstruction ?mode ?blk ?RR (?S❟ ?R)))
(PROP _) ›
‹PROP φApplication (Trueprop (?var 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (CurrentConstruction ?mode ?blk ?RR (?S❟ ?R)))
(PROP _) ›]:
‹ PROP φApplication (Trueprop (S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (CurrentConstruction mode blk RR (S❟ R)))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk RR (T❟ R)) ∧ P)›
unfolding φApplication_def
using φapply_implication transformation_right_frame by blast
subparagraph ‹ToA_App_Conv›
lemma [φreason %φapp_ToA_on_proc_or_VS+50]:
‹ ToA_App_Conv TYPE('c⇩a) TYPE(fiction) T (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P') (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P)
⟹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X 𝗐𝗂𝗍𝗁 P2
⟹ PROP φApplication (Trueprop (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P'))
(Trueprop (CurrentConstruction mode blk R (x ⦂ T)))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk R Y) ∧ P ∧ P2)›
for T' :: ‹('c⇩a,'a⇩a) φ›
unfolding φApplication_def ToA_App_Conv_def
using φapply_implication by blast
lemma [φreason %φapp_ToA_on_proc_or_VS+50]:
‹ ToA_App_Conv TYPE('c⇩a) TYPE(fiction) T (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P') (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P)
⟹ φIntroFrameVar R' X'' X Y'' Y
⟹ x ⦂ T❟ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X'' 𝗐𝗂𝗍𝗁 P2
⟹ PROP φApplication (Trueprop (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P'))
(Trueprop (CurrentConstruction mode blk RR (x ⦂ T❟ R)))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk RR Y'') ∧ P ∧ P2)›
for T' :: ‹('c⇩a,'a⇩a) φ›
unfolding φApplication_def ToA_App_Conv_def φIntroFrameVar_def
by (cases R'; simp; metis φapply_view_shift φframe_view_right mult.commute view_shift_by_implication)
subparagraph ‹Normal›
lemma φapply_transformation_fully[φreason %φapp_ToA_on_proc_or_VS]:
" φIntroFrameVar R S'' S' T'' T'
⟹ S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S'' 𝗐𝗂𝗍𝗁 Any
⟹ PROP φApplication (Trueprop (S' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T' 𝗐𝗂𝗍𝗁 P))
(Trueprop (CurrentConstruction mode blk RR S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk RR T'') ∧ P)"
unfolding φIntroFrameVar_def φApplication_def Action_Tag_def φApp_Conv_def
by (cases R; simp; meson φapply_view_shift φview_shift_intro_frame view_shift_by_implication)
subparagraph ‹Variant›
lemma [φreason %φapp_ToA_on_proc_or_VS]:
" PROP φApplication (Trueprop (S' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T'))
(Trueprop (CurrentConstruction mode blk RR S))
(PROP Result)
⟹ PROP φApplication (Trueprop (S' = T'))
(Trueprop (CurrentConstruction mode blk RR S))
(PROP Result)"
unfolding φApplication_def BI_eq_ToA
subgoal premises prems
by (rule prems(1); insert prems(2-); blast) .
paragraph ‹View Shift Methods›
lemma φapply_view_shift_fast[φreason %φapp_VS_on_proc_or_VS+200 for ‹
PROP φApplication (Trueprop (?S' 𝗌𝗁𝗂𝖿𝗍𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (CurrentConstruction ?mode ?blk ?RR ?S)) ?Result
›]:
‹ PROP φApplication (Trueprop (S 𝗌𝗁𝗂𝖿𝗍𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (CurrentConstruction mode blk R S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk R T) ∧ P)›
unfolding φApplication_def
using "φapply_view_shift" .
lemma [φreason %φapp_VS_on_proc_or_VS+100 for ‹
PROP φApplication (Trueprop (?S' 𝗌𝗁𝗂𝖿𝗍𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (CurrentConstruction ?mode ?blk ?RR (?S❟ ?R))) ?Result
›]:
‹ PROP φApplication (Trueprop (S 𝗌𝗁𝗂𝖿𝗍𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (CurrentConstruction mode blk RR (S❟ R)))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk RR (T❟ R)) ∧ P)›
unfolding φApplication_def
using "φapply_view_shift" φview_shift_intro_frame by blast
lemma φapply_view_shift_fully[φreason %φapp_VS_on_proc_or_VS for ‹
PROP φApplication (Trueprop (?S' 𝗌𝗁𝗂𝖿𝗍𝗌 ?T' 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (CurrentConstruction ?mode ?blk ?RR ?S)) ?Result
›]:
"φIntroFrameVar R S'' S' T T'
⟹ S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S'' 𝗐𝗂𝗍𝗁 P1
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (S' 𝗌𝗁𝗂𝖿𝗍𝗌 T' 𝗐𝗂𝗍𝗁 P2))
(Trueprop (CurrentConstruction mode blk RR S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (CurrentConstruction mode blk RR T) ∧ (P1 ∧ P2))"
unfolding φIntroFrameVar_def φApplication_def Action_Tag_def
by (cases R; simp, insert φapply_implication φapply_view_shift φview_shift_intro_frame, blast+)
paragraph ‹Procedure Methods›
lemma apply_proc_fast[φreason %φapp_proc_on_proc_or_VS+200 for ‹
PROP φApplication (Trueprop (𝗉𝗋𝗈𝖼 ?f ⦃ ?S ⟼ ?T ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E ))
(Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?S)) ?Result
› ‹
PROP φApplication (Trueprop (𝗉𝗋𝗈𝖼 ?f ⦃ ?var_S ⟼ ?T ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E ))
(Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?S)) ?Result
›
]:
‹ PROP φApplication (Trueprop (𝗉𝗋𝗈𝖼 f ⦃ S ⟼ T ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ))
(Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ 𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f 𝗈𝗇 blk [H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 T 𝗍𝗁𝗋𝗈𝗐𝗌 E)›
unfolding φApplication_def
using φapply_proc .
lemma φapply_proc_fully[φreason %φapp_proc_on_proc_or_VS for
‹PROP φApplication (Trueprop (𝗉𝗋𝗈𝖼 ?f ⦃ ?S' ⟼ ?T' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E ))
(Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?S)) ?Result›
]:
‹ φIntroFrameVar' R S'' S' T T' E'' E'
⟹ S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S'' 𝗐𝗂𝗍𝗁 P
⟹ Simplify (assertion_simps ABNORMAL) E''' E''
⟹ (⋀v. Remove_Values (E''' v) (E v))
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (𝗉𝗋𝗈𝖼 f ⦃ S' ⟼ T' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E' ))
(Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝗉𝖾𝗇𝖽𝗂𝗇𝗀 f 𝗈𝗇 blk [RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 T 𝗍𝗁𝗋𝗈𝗐𝗌 E) ∧ P)›
unfolding φApplication_def φIntroFrameVar'_def
Simplify_def Action_Tag_def Simplify_def Remove_Values_def
apply rule
subgoal premises prems
apply (simp only: prems(1))
using φapply_proc[OF ‹𝖼𝗎𝗋𝗋𝖾𝗇𝗍 _ [_] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 _›,
OF ‹𝗉𝗋𝗈𝖼 f ⦃ S' ⟼ T' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E' ›[THEN φframe[where R=R],
THEN φCONSEQ[rotated 1, OF view_shift_by_implication[OF ‹S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S'' 𝗐𝗂𝗍𝗁 P›],
OF view_shift_refl, OF view_shift_by_implication[OF ‹E''' _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 E _›],
simplified prems(1), unfolded ‹E''' = E''›, simplified prems(1)]]] .
using φapply_implication by blast
subsubsection ‹Application on a Block / End a Block›
definition ‹Simple_HO_Unification f f' ⟷ (f = f')›
text ‹\<^schematic_prop>‹Simple_HO_Unification A (?f x⇩1 … x⇩n)› encodes a higher order unification
which find an instantiation of ‹f› where terms ‹x⇩1, …, x⇩n› are not free in ‹f›.
Such ‹f› is the most general if ‹x⇩1, …, x⇩n› are all variables.
To prove this, we show there is a unique ‹f› such that ‹f x ≡ A› if ‹x› is a variable
not free in ‹f›.
Assume ‹f⇩1 x ≡ A› and ‹f⇩2 x ≡ A› then we have ‹f⇩1 x ≡ f⇩2 x›
and then ‹(λx. f⇩1 x) ≡ (λx. f⇩2 x)›.
Because x is not free in ‹f⇩1, f⇩2›, by eta-contraction, we have ‹f⇩1 ≡ f⇩2›.
The ‹≡› here means alpha-beta-eta equivalence.
›
lemma Simple_HO_Unification_I:
‹ Premise procedure_ss (f = f')
⟹ Simple_HO_Unification f f'›
unfolding Simple_HO_Unification_def Premise_def by simp
φreasoner_ML Simple_HO_Unification 1200 (‹Simple_HO_Unification ?f ?f'›) = ‹
let
fun inc_bound 0 X = X
| inc_bound d (Bound i) = Bound (i+d)
| inc_bound d (A $ B) = inc_bound d A $ inc_bound d B
| inc_bound d (Abs (N,T,X)) = Abs (N,T, inc_bound d X)
| inc_bound _ X = X
fun abstract_bound_over (x, body) =
let
fun abs x lev tm =
if x aconv tm then Bound lev
else
(case tm of
Abs (a, T, t) => Abs (a, T, abs (inc_bound 1 x) (lev + 1) t)
| t $ u =>
(abs x lev t $ (abs x lev u handle Same.SAME => u)
handle Same.SAME => t $ abs x lev u)
| _ => raise Same.SAME)
in abs x 0 body handle Same.SAME => body end
fun my_abstract_over _ (v as Free (name,ty)) body =
Abs (name, ty, abstract_over (v,body))
| my_abstract_over btys (Bound i) body =
Abs ("", nth btys i, abstract_bound_over (Bound i,body))
| my_abstract_over _ (v as Const (_,ty)) body =
Abs ("", ty, abstract_over (v,body))
| my_abstract_over _ v body =
Abs ("", fastype_of v, abstract_bound_over (v,body))
fun dec_bound_level d [] = []
| dec_bound_level d (h::l) = inc_bound (d+1) h :: (dec_bound_level (d+1) l)
in
fn (_, (ctxt,sequent)) =>
let
val (Vs, _, \<^const>‹Trueprop› $ (Const (\<^const_name>‹Simple_HO_Unification›, _) $ f $ f'))
= Phi_Help.leading_antecedent (Thm.prop_of sequent)
val btys = rev (map snd Vs)
val f' = Envir.beta_eta_contract f'
in (case Term.strip_comb f' of (Var v, args) =>
if forall is_Bound args
then sequent
else Thm.instantiate (TVars.empty, Vars.make [
(v, Thm.cterm_of ctxt (fold_rev (my_abstract_over btys)
(dec_bound_level (~ (length args)) args) f))])
sequent
| _ => sequent)
|> (fn seq => Seq.single (ctxt, @{thm Simple_HO_Unification_I} RS seq))
end
end
›
lemma [φreason %φapp_conv for ‹
φApp_Conv (𝗉𝗋𝗈𝖼 ?f ⦃ ?X ⟼ ?Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E) (𝗉𝗋𝗈𝖼 ?f' ⦃ ?X' ⟼ ?Y' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E')
›]:
‹ Simple_HO_Unification f f'
⟹ X' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X 𝗐𝗂𝗍𝗁 Any1
⟹ (⋀ret. Y ret 𝗌𝗁𝗂𝖿𝗍𝗌 Y' ret 𝗐𝗂𝗍𝗁 Any2)
⟹ (⋀ex. E ex 𝗌𝗁𝗂𝖿𝗍𝗌 E' ex 𝗐𝗂𝗍𝗁 Any3)
⟹ φApp_Conv (𝗉𝗋𝗈𝖼 f ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ) (𝗉𝗋𝗈𝖼 f' ⦃ X' ⟼ Y' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E') ›
unfolding φApp_Conv_def Simple_HO_Unification_def Action_Tag_def
using φCONSEQ view_shift_by_implication by blast
lemma [φreason %φapp_conv for ‹
φApp_Conv (PendingConstruction _ _ _ _ _) (PendingConstruction _ _ _ _ _)
›]:
‹ Simple_HO_Unification f f'
⟹ (⋀ret. S ret 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S' ret 𝗐𝗂𝗍𝗁 Any2)
⟹ (⋀ex. E ex 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 E' ex 𝗐𝗂𝗍𝗁 Any3)
⟹ φApp_Conv (PendingConstruction f s R S E) (PendingConstruction f' s R S' E') ›
unfolding φApp_Conv_def Simple_HO_Unification_def Action_Tag_def
using φapply_implication_pending φapply_implication_pending_E by blast
subsubsection ‹Applying on View Shift Construction›
lemma [φreason %φapp_conv for ‹φApp_Conv (?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?Y 𝗐𝗂𝗍𝗁 ?P) (?X' 𝗌𝗁𝗂𝖿𝗍𝗌 ?Y' 𝗐𝗂𝗍𝗁 ?P')›]:
‹ X' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X 𝗐𝗂𝗍𝗁 Any1
⟹ Y 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 Any2
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (Any1 ∧ Any2 ∧ P ⟶ P')
⟹ φApp_Conv (X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P) (X' 𝗌𝗁𝗂𝖿𝗍𝗌 Y' 𝗐𝗂𝗍𝗁 P') ›
unfolding φApp_Conv_def Simple_HO_Unification_def Action_Tag_def Premise_def
by (metis View_Shift_def view_shift_by_implication)
subsubsection ‹Application on ToA Construction›
φreasoner_group φapp_ToA_on_ToA = (1000, [1000, 1200])
for ‹PROP φApplication (Trueprop (S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S))
Result ›
in φapplication_all and > φapplication_traverse_apps
‹applying ToA on ToA construction mode›
lemma apply_cast_on_imply_exact
[φreason %φapp_ToA_on_ToA+110 for ‹PROP φApplication (Trueprop (?S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(?x) 𝗂𝗌 ?S))
(PROP _) ›
‹PROP φApplication (Trueprop (?var_S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(?x) 𝗂𝗌 ?S))
(PROP _) ›
]:
‹ PROP φApplication (Trueprop (S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ ((𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 T) ∧ P))›
unfolding φApplication_def Transformation_def ToA_Construction_def
by blast
lemma apply_cast_on_imply_right_prod
[φreason %φapp_ToA_on_ToA+100 for ‹PROP φApplication (Trueprop (?S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(?x) 𝗂𝗌 ?S * ?R))
(PROP _) ›
‹PROP φApplication (Trueprop (?var 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?T 𝗐𝗂𝗍𝗁 ?P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(?x) 𝗂𝗌 ?S * ?R))
(PROP _) ›
]:
‹ PROP φApplication
(Trueprop (S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S * R))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ ((𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 T * R) ∧ P))›
unfolding φApplication_def ToA_Construction_def
using transformation_right_frame by (metis Transformation_def)
lemma [φreason %φapp_ToA_on_ToA+50]:
" ToA_App_Conv TYPE('c⇩a) TYPE('c) T (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P') (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P)
⟹ φIntroFrameVar R X'' X Y'' Y
⟹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X'' 𝗐𝗂𝗍𝗁 P2
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P'))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭ) 𝗂𝗌 x ⦂ T))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭ) 𝗂𝗌 Y'') ∧ P ∧ P2)"
for T :: ‹('c::sep_magma,'a) φ› and T' :: ‹('c⇩a::sep_magma,'a⇩a) φ›
unfolding φIntroFrameVar_def φApplication_def Action_Tag_def ToA_App_Conv_def
by ((cases R; simp),
metis φapply_implication_impl,
meson φapply_implication_impl transformation_right_frame)
lemma [φreason %φapp_ToA_on_ToA+50]:
" ToA_App_Conv TYPE('c⇩a) TYPE('c) T (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P') (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P)
⟹ φIntroFrameVar R'' X'' X Y'' Y
⟹ (x ⦂ T) * R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X'' 𝗐𝗂𝗍𝗁 P2
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y' 𝗐𝗂𝗍𝗁 P'))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭ) 𝗂𝗌 (x ⦂ T) * R))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭ) 𝗂𝗌 Y'') ∧ P ∧ P2)"
for T :: ‹('c::sep_magma,'a) φ› and T' :: ‹('c⇩a::sep_magma,'a⇩a) φ›
unfolding φIntroFrameVar_def φApplication_def Action_Tag_def ToA_App_Conv_def
by ((cases R''; simp),
metis φapply_implication_impl,
meson φapply_implication_impl transformation_right_frame)
lemma [φreason %φapp_ToA_on_ToA+20]:
"φIntroFrameVar R S'' S' T T'
⟹ S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S'' 𝗐𝗂𝗍𝗁 Any
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (S' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T' 𝗐𝗂𝗍𝗁 P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 T) ∧ P)"
for S' :: ‹'c::sep_magma BI›
unfolding φIntroFrameVar_def φApplication_def Action_Tag_def
by (cases R; simp; meson φapply_implication_impl transformation_right_frame)
lemma [φreason %φapp_ToA_on_ToA+20]:
"φIntroFrameVar R S'' S' T T'
⟹ S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S'' 𝗐𝗂𝗍𝗁 Any
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (S' = T'))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 T))"
for S' :: ‹'c::sep_magma BI›
unfolding φIntroFrameVar_def φApplication_def Action_Tag_def
by (cases R; simp; meson φapply_implication_impl transformation_left_frame)
lemma [φreason %φapp_ToA_on_ToA]:
" S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S' 𝗐𝗂𝗍𝗁 Any
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (S' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 T 𝗐𝗂𝗍𝗁 P))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭ) 𝗂𝗌 S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(ℭ) 𝗂𝗌 T) ∧ P)"
for S' :: ‹'c::type BI›
unfolding φApplication_def Action_Tag_def ToA_Construction_def Transformation_def
by metis
lemma [φreason %φapp_ToA_on_ToA]:
" S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S' 𝗐𝗂𝗍𝗁 Any
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (S' = T))
(Trueprop (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 S))
(𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(x) 𝗂𝗌 T))"
for S' :: ‹'c::type BI›
unfolding φApplication_def Action_Tag_def ToA_Construction_def Transformation_def
by metis
subsection ‹Action›
text ‹Action provides a kind of meta calling mechanism.
The expression of an action is nothing but a syntactical symbol.
The symbol itself does not given any semantic information about what it does exactly.
Its effect to the programming is interpreted by reasoning, or more specifically, by the
configured reasoning rules binding on the action symbol.
The rules perform the actual transformations, applications, or any other operations.
And this performance defines the semantics of the action.
Applying an action can be read as invoking certain automatic operation linked to the name of the
action, to do some transformations or generate some code or do anything feasible.
It makes the action calling very flexible.
Semantic conversion made by reasoners written in ML can be involved, which gives
sufficient space for many automatic operation.
›
text ‹The action symbol is encoded to be a fixed free variable or a constant of \<^typ>‹action›.
Therefore the pattern matching can be native and fast.
Note an action can be parameterized like, \<^typ>‹nat ⇒ bool ⇒ action› parameterized
by a nat and a boolean. Other parameters can come from the sequent.
›
text ‹\<^prop>‹A @tag Act› tells antecedent \<^prop>‹A› is bound to the action Act, typically
a procedure rule or an implication or a view shift rule.›
definition Do_Action :: ‹action ⇒ prop ⇒ prop ⇒ prop›
where ‹Do_Action action sequent result ≡ (PROP sequent ⟹ PROP result)›
text ‹\<^prop>‹PROP Do_Action action sequent result› is the antecedent to be reasoned
to return the construction result of the sequent by the action.›
declare [[φreason_default_pattern ‹PROP Do_Action ?A ?S _› ⇒ ‹PROP Do_Action ?A ?S _› (100) ]]
subsubsection ‹Two Methods of Applying Action›
text ‹There are two way to activate the construction of an action.
One is by application mechanism where user inputs a theorem of shape \<^prop>‹PROP Call_Action action›;
another is by synthesis, where user inputs a cartouche of \<^term>‹action›.›
paragraph ‹First way, by Application›
definition Call_Action :: ‹action ⇒ bool› where ‹Call_Action _ ≡ True›
lemma Call_Action_I[intro!]: ‹Call_Action Act› unfolding Call_Action_def ..
lemma [φreason %φapplication]:
‹ PROP Do_Action action sequent result
⟹ PROP φApplication (Trueprop (Call_Action action)) sequent result›
unfolding φApplication_def Do_Action_def .
paragraph ‹Second way, by Synthesis›
lemma [φreason 1400]:
‹ 𝗋CALL Synthesis_Parse action action'
⟹ PROP Do_Action action' sequent result
⟹ 𝗋Success
⟹ PROP DoSynthesis action sequent result›
for action :: action
unfolding DoSynthesis_def Do_Action_def .
subsubsection ‹Rules of Executing Action›
paragraph ‹Fallback›
lemma [φreason 1]:
‹ FAIL TEXT(‹Don't know how to do› action ‹on› Sequent)
⟹ PROP Do_Action action Sequent Sequent›
unfolding Do_Action_def Action_Tag_def Action_Tag_def .
subsection ‹Generic Element Access›
subsubsection ‹Get Element of Abstract Object›
type_synonym element_index_input = ‹(VAL × VAL BI) list›
definition Get_Abstract_Element :: ‹'x ⇒ ('val,'x) φ ⇒ element_index_input ⇒ 'y ⇒ bool›
where ‹Get_Abstract_Element x T path y ⟷ True›
declare [[
φreason_default_pattern ‹Get_Abstract_Element ?x ?T ?path _ › ⇒ ‹Get_Abstract_Element ?x ?T ?path _› (100)
]]
lemma [φreason 1000]:
‹Get_Abstract_Element x T [] x›
unfolding Get_Abstract_Element_def ..
subsection ‹Streamlined Parse for Element Index›
definition report_unprocessed_element_index :: ‹element_index_input ⇒ action ⇒ bool›
where ‹report_unprocessed_element_index path final_hook ⟷ True›
declare [[
φreason_default_pattern ‹report_unprocessed_element_index ?path _› ⇒ ‹report_unprocessed_element_index ?path _› (100),
φpremise_attribute once? [φreason? %local] for ‹report_unprocessed_element_index _ _› (%φattr)
]]
lemma report_unprocessed_element_index_I:
‹report_unprocessed_element_index path any›
unfolding report_unprocessed_element_index_def ..
definition chk_element_index_all_solved :: ‹element_index_input ⇒ bool›
where ‹chk_element_index_all_solved path ⟷ True›
subsubsection ‹ML›
consts ℰℐℋ𝒪𝒪𝒦_none :: action
ML_file ‹library/system/generic_element_access.ML›
φreasoner_ML chk_element_index_all_solved 1000 (‹chk_element_index_all_solved _›) = ‹
fn (_, (ctxt,sequent)) => Seq.make (fn () =>
let val (_,_,ant,_) =
Phi_Help.strip_meta_hhf_c (fst (Thm.dest_implies (Thm.cprop_of sequent))) ctxt
val idx = Thm.dest_arg (Thm.dest_arg ant)
in if Generic_Element_Access.is_empty_input (Thm.term_of idx)
then SOME ((ctxt, @{thm report_unprocessed_element_index_I} RS sequent),
Seq.empty)
else (
warning (Pretty.string_of (Pretty.block [
Pretty.str "Fail to access element ",
Syntax.pretty_term ctxt (Thm.term_of idx)
])) ;
NONE )
end)
›
φreasoner_ML report_unprocessed_element_index 1000 (‹report_unprocessed_element_index _ _›) = ‹
fn (_, (ctxt,sequent)) => Seq.make (fn () =>
let val (_,_,ant,_) =
Phi_Help.strip_meta_hhf_c (fst (Thm.dest_implies (Thm.cprop_of sequent))) ctxt
val main = Thm.dest_arg ant
val hook = Thm.dest_arg main
val idx = Thm.dest_arg (Thm.dest_fun main)
in if Generic_Element_Access.is_empty_input (Thm.term_of idx)
orelse Generic_Element_Access.is_enabled_report_unprocessed_element_index ctxt
then SOME ((Generic_Element_Access.report_unprocessed_element_index (idx, hook) ctxt,
@{thm report_unprocessed_element_index_I} RS sequent),
Seq.empty)
else Generic_Element_Access.error_unprocessed_element_index ctxt idx
end)
›
subsection ‹Generic Variable Access›
subsubsection ‹Annotation›
definition Value_of :: ‹'x ⇒ 'v ⇒ element_index_input ⇒ 'x› ("_ <val-of> _ <path> _" [23,23,23] 22)
where [iff, φprogramming_base_simps]: ‹(x <val-of> v <path> path) = x›
definition Set_Value :: ‹'x ⇒ 'v ⇒ element_index_input ⇒ 'x› ("_ <set-to> _ <path> _" [51, 1000, 51] 50)
where [iff, φprogramming_base_simps]: ‹(y <set-to> x <path> path) = y›
declare [[
φreason_default_pattern
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. _ <val-of> ?v <path> ?path ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag synthesis› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. _ <val-of> ?v <path> ?path ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag synthesis› (120)
]]
subsubsection ‹Syntax›
nonterminal φidentifier
syntax
"_identifier_" :: "φidentifier ⇒ logic" ("$\"_")
"_identifier_id_" :: ‹id ⇒ φidentifier› ("_")
"_identifier_num_" :: ‹num_token ⇒ φidentifier› ("_")
"_identifier_1_" :: ‹φidentifier› ("1")
"_identifier_logic_" :: ‹logic ⇒ φidentifier› ("'(_')")
"_get_φvar_" :: "φidentifier ⇒ logic" ("$_")
"_set_φvar_" :: "φidentifier ⇒ logic ⇒ logic" ("$_ := _" [910, 51] 50)
consts φidentifier :: "unit ⇒ unit"
subsubsection ‹Rule \& Implementation›
lemma "__value_access_0__":
‹ 𝗉𝗋𝗈𝖼 F ⦃ R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ 𝗉𝗋𝗈𝖼 F ⦃ Void 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
unfolding REMAINS_def
by fastforce
φreasoner_group local_values = (%cutting, [%cutting, %cutting]) for ‹_›
‹Facts demonstrating values of local variables›
section ‹Implementing the Interactive Environment›
text ‹The implementation consists of three steps:
▸ building the ML systems and libraries;
▸ defining the Isar commands;
▸ defining ∗‹φlang_parsers›.
›
text ‹φProcessor realizes specific facilities for programming in a statement,
such as applying an application, setting a parameter or a label, invoking program synthesis,
proving a proof obligation, simplifying or transforming the state sequent,
and fixing an existentially quantified variable.
›
subsection ‹Convention of Operator Precedence›
φreasoner_group φlang_precedence = (100, [0,1000])
‹precedence of component parsers of Isar/φ-lang.
The parser will not be applied until the operator stack is evaluated down to (of a precedence
less than) the designated precedence.
It can be seen as the precedence of the symbol that the parser processes›
and φlang_top = (1000, [1000,1000]) in φlang_precedence
‹technically used. No operator should be of this precedence.›
and φlang_expr = (10, [10, 999]) in φlang_precedence < φlang_top
‹operators of expression›
and φlang_statement = (1, [1, 9]) in φlang_precedence < φlang_expr
‹connectives of statement›
and φlang_push_val = (950, [950,950]) in φlang_expr
‹pushing local value to thestate sequent›
and φlang_dot_opr = (930, [930,930]) in φlang_expr and < φlang_push_val
‹dot operator ‹‣››
and φlang_deref = (910, [910,910]) in φlang_expr and < φlang_dot_opr
‹dereference operator›
and φlang_app = (900, [900,900]) in φlang_expr and < φlang_dot_opr
‹precedence of lambda application›
and φlang_update_opr = (50, [50,50]) in φlang_expr and < φlang_app
‹‹:=›, as an arithmetic operartor›
and φlang_assignment = (5, [5,5]) in φlang_statement and < φlang_update_opr
‹‹←›, as a connective of statement›
φreasoner_group φparser_priority = (0, [0, 10000])
‹priority of component parsers of Isar/φ-lang, deciding which parser will be applied when multiple
candidates are available anytime. Lower is of more priority.›
and φparser_app = (500, [0, 10000]) in φparser_priority
‹parsers for application›
and φparser_lpar = (50, [0,100]) in φparser_priority ‹›
and φparser_rpar = (100, [100,100]) in φparser_priority ‹›
and φparser_cartouch_all = (0, [0,100]) in φparser_priority
‹parsers accepting a cartouche›
and φparser_synthesis = (100, [100,100]) in φparser_cartouch_all ‹›
and φparser_cartouch = (0, [0, 99]) in φparser_cartouch_all and < φparser_synthesis ‹›
and φparser_unique = (500,[500,500]) in φparser_priority
‹a default group for components of no ambiguity›
and φparser_right_arrow = (500,[500,500]) in φparser_priority ‹›
and φparser_left_arrow = (500,[500,500]) in φparser_priority ‹›
and φparser_var_decl = (500,[400,600]) in φparser_priority ‹›
subsection ‹ML codes›
ML_file "library/instructions.ML"
ML_file "library/tools/parse.ML"
ML_file ‹library/system/post-app-handlers.ML›
ML_file "library/system/procedure.ML"
ML_file ‹library/system/sys0.ML›
ML_file ‹library/system/generic_variable_access.ML›
ML_file ‹library/system/sys.ML›
ML_file ‹library/system/opr_stack.ML›
ML_file ‹library/system/toplevel0.ML›
ML_file ‹library/system/opr_stack2.ML›
ML_file "library/system/processor.ML"
ML_file ‹library/system/generic_variable_access2.ML›
ML_file ‹library/system/obtain.ML›
ML_file ‹library/system/modifier.ML›
ML_file ‹library/system/toplevel.ML›
ML_file ‹library/tools/CoP_simp_supp.ML›
ML_file ‹library/system/generic_element_access2.ML›
subsubsection ‹Setups›
hide_fact "__value_access_0__"
setup ‹Context.theory_map (
Generic_Element_Access.register_hook (\<^const_name>‹ℰℐℋ𝒪𝒪𝒦_none›, K (K I))
)›
subsection ‹Isar Commands \& Attributes›
ML ‹Theory.setup (Global_Theory.add_thms_dynamic (@{binding "φinstr"}, NuInstructions.list_definitions #> map snd)) ›
attribute_setup φinstr = ‹Scan.succeed (Thm.declaration_attribute NuInstructions.add) ›
‹Instructions of φ-system›
declare [[φpremise_attribute [THEN Do_D] for ‹𝖽𝗈 PROP _› (%φattr_normalize),
φpremise_attribute [THEN Premise_D] for ‹𝗉𝗋𝖾𝗆𝗂𝗌𝖾 ?x› (%φattr_late_normalize),
φpremise_attribute [THEN Premise_D] for ‹𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇[_] ?x› (%φattr_late_normalize),
φpremise_attribute once? [φreason? %local] for ‹Semantic_Type _ _› ‹𝖽𝗈 Semantic_Type _ _› (%φattr),
φpremise_attribute once? [φreason? %local] for ‹Semantic_Zero_Val _ _ _› ‹𝖽𝗈 Semantic_Zero_Val _ _ _› (%φattr),
φpremise_attribute [THEN Simplify_D] for ‹Simplify _ _ _› ‹𝖽𝗈 Simplify _ _ _› (%φattr_late_normalize),
φpremise_attribute once? [φreason? %local] for ‹Is_Functional ?S› (%φattr),
φpremise_attribute once? [φreason? %local] for ‹_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _› (%φattr)
]]
subsection ‹User Interface Processors›
text ‹Convention of priorities:
▪ Simplifications and Conversions for canonical forms < 1000
▪ Reasoning Antecedents = 1000
▪ General Application not bound on specific pattern or keyword : 9000~9999
›
subsubsection ‹Controls›
φlang_parser set_auto_level (10, %φlang_app) ["!!", "!!!"] (‹PROP ?P›)
‹(fn (oprs, (ctxt, sequent)) => Phi_Parse.auto_level_force >>
(fn auto_level' => fn _ =>
(oprs, (Config.put Phi_Reasoner.auto_level auto_level' ctxt, sequent))))›
subsubsection ‹Constructive›
lemma φcast_exception_UI:
" PendingConstruction f blk H T E
⟹ (⋀a. 𝗎𝗌𝖾𝗋 E a 𝗌𝗁𝗂𝖿𝗍𝗌 E' a)
⟹ PendingConstruction f blk H T E'"
unfolding Argument_def
using φapply_view_shift_pending_E .
φlang_parser "throws" (%φparser_unique, 0) ["throws"] (‹𝗉𝖾𝗇𝖽𝗂𝗇𝗀 ?f 𝗈𝗇 ?blk [?H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?T 𝗍𝗁𝗋𝗈𝗐𝗌 ?E›)
‹fn (oprs, (ctxt, sequent)) => \<^keyword>‹throws› >> (fn _ => fn _ =>
(oprs, (ctxt, sequent RS @{thm "φcast_exception_UI"})) )›
hide_fact φcast_exception_UI
ML ‹Generic_Variable_Access.lookup_bindings›
φlang_parser "apply" (%φparser_app, %φlang_app) ["", "apply_rule"] (‹PROP _›)
‹ fn (oprs,(ctxt,sequent)) =>
Generic_Variable_Access.parser_no_lvar ctxt Phi_App_Rules.parser >> (fn xnames => fn cfg =>
(oprs, (ctxt, sequent)
|> Phi_Reasoners.wrap'' (Phi_Apply.apply1 (Phi_App_Rules.app_rules ctxt [xnames]))
))›
φlang_parser delayed_apply (%φparser_app-200, %φlang_app) ["", "apply_rule"] (‹PROP _›)
‹ fn (opr_ctxt as (_,(ctxt,_))) =>
(Phi_App_Rules.parser --| \<^keyword>‹(›) >> (fn xname => fn cfg =>
let fun name_pos_of (Facts.Named (name_pos, _)) = name_pos
| name_pos_of _ = ("", Position.none)
in
if Phi_Opr_Stack.synt_can_delay_apply' (Context.Proof ctxt) (fst xname)
then Phi_Opr_Stack.begin_apply cfg (name_pos_of (fst xname), Phi_App_Rules.app_rules ctxt [xname]) opr_ctxt
else raise Phi_CP_IDE.Bypass
end)›
φlang_parser apply_operator (%φparser_app-300, %φlang_top) [""] (‹PROP _›)
‹ fn (opr_ctxt as (_,(ctxt,_))) =>
(Phi_App_Rules.symbol_position >> (fn (xname,pos) => fn cfg =>
case Phi_Opr_Stack.lookup_operator (Proof_Context.theory_of ctxt) xname
of NONE => raise Phi_CP_IDE.Bypass
| SOME opr => (
case Phi_Opr_Stack.lookup_meta_opr (Proof_Context.theory_of ctxt) xname
of SOME meta =>
Phi_Opr_Stack.push_meta_operator cfg (opr, (xname,pos), NONE, meta) opr_ctxt
| NONE =>
let val rules = Phi_App_Rules.app_rules ctxt [(Facts.Named ((xname,pos), NONE), [])]
in Phi_Opr_Stack.push_operator cfg (opr, (xname,pos), rules) opr_ctxt
end)
))›
φlang_parser open_parenthesis (%φparser_lpar, %φlang_push_val) ["("] (‹PROP _›)
‹ fn s => (Parse.position \<^keyword>‹(›) >> (fn (_, pos) => fn _ =>
Phi_Opr_Stack.open_parenthesis (NONE, pos) s) ›
φlang_parser close_parenthensis (%φparser_rpar, %φlang_top) [")"] (‹PROP _›)
‹ fn s => \<^keyword>‹)› >> (fn _ => fn cfg => Phi_Opr_Stack.close_parenthesis (cfg, NONE, false) s)›
φlang_parser comma (%φparser_unique, %φlang_top) [","] (‹?P›) ‹ fn s =>
Parse.position \<^keyword>‹,› -- Scan.option (Parse.short_ident --| \<^keyword>‹:›)
>> (fn ((_,pos), arg_name) => fn cfg => Phi_Opr_Stack.comma cfg (arg_name, pos) s)›
φlang_parser embedded_block (%φparser_lpar-20, %φlang_expr) ["("] (‹PROP ?P ⟹ PROP ?Q›)
‹ fn stat => (Parse.position \<^keyword>‹(› >> (fn (_, pos) => fn _ =>
stat |> Phi_Opr_Stack.begin_block pos
|> apsnd (Phi_CP_IDE.proof_state_call (Phi_Toplevel.begin_block_cmd ([],[]) false)) ))›
φlang_parser delimiter_of_statement (%φparser_unique, 0) [";"] (‹CurrentConstruction ?mode ?blk ?H ?S› | ‹𝖺𝖻𝗌𝗍𝗋𝖺𝖼𝗍𝗂𝗈𝗇(?s) 𝗂𝗌 ?S'›)
‹ fn (s as (_, (ctxt, _))) => \<^keyword>‹;› >> (fn _ => fn cfg =>
s |> Phi_Opr_Stack.End_of_Statement.invoke (Context.Proof ctxt) cfg
|> Phi_Opr_Stack.Begin_of_Statement.invoke (Context.Proof ctxt) cfg) ›
φlang_parser set_param (%φparser_cartouch, %φlang_expr) ["<cartouche>", ""] (‹𝗉𝖺𝗋𝖺𝗆 ?P ⟹ PROP _›)
‹fn s => Parse.term >> (fn term => fn _ => apsnd (Phi_Sys.set_param_cmd term) s)›
φlang_parser set_label (%φparser_cartouch, %φlang_expr) ["<cartouche>"] (‹𝗅𝖺𝖻𝖾𝗅 ?P ⟹ PROP _›)
‹fn s => Parse.name >> (fn name => fn _ => apsnd (Phi_Sys.set_label name) s)›
φlang_parser rule (%φparser_app, %φlang_expr) [] (‹PROP ?P ⟹ PROP ?Q›)
‹fn (oprs, (ctxt, sequent)) => Phi_App_Rules.parser >> (fn thm => fn _ =>
let open Phi_Envir
val apps = Phi_App_Rules.app_rules ctxt [thm]
val sequent = perhaps (try (fn th => @{thm Argument_I} RS th)) sequent
in (oprs, Phi_Reasoners.wrap'' (Phi_Apply.apply1 apps) (ctxt,sequent))
end)›
ML ‹
val phi_synthesis_parsing = Attrib.setup_config_bool \<^binding>‹φ_synthesis_parsing› (K false)
fun phi_synthesis_parser (oprs, (ctxt, sequent)) F (raw_term, pos) cfg =
let val ctxt_parser = Proof_Context.set_mode Proof_Context.mode_pattern ctxt
|> Config.put phi_synthesis_parsing true
|> Config.put Generic_Variable_Access.mode_synthesis true
val binds = Variable.binds_of ctxt_parser
val term = Syntax.parse_term ctxt_parser raw_term
|> Term.map_aterms (
fn X as Var (name, _) =>
(case Vartab.lookup binds name of SOME (_,Y) => Y | _ => X)
| X => X
)
|> F ctxt
|> Syntax.check_term ctxt_parser
|> Thm.cterm_of ctxt
val mode_subproc = Phi_Opr_Stack.precedence_of (#1 oprs) < 0 andalso
(case Thm.prop_of sequent
of Const (\<^const_name>‹Pure.imp›, _) $ _ $ _ => true
| _ => false)
in if mode_subproc
then (oprs, Phi_Reasoners.wrap'' (Phi_Sys.synthesis term) (ctxt, sequent))
else Phi_Opr_Stack.push_meta_operator cfg
((@{priority %φlang_push_val}, @{priority loose %φlang_push_val},
(VAR_ARITY_IN_SEQUENT, VAR_ARITY_IN_SEQUENT)), ("<synthesis>", pos), NONE,
(fn (_,_,_,vals) =>
(apsnd ( Generic_Variable_Access.push_values vals
#> Phi_Reasoners.wrap'' (Phi_Sys.synthesis term)
)))) (oprs, (ctxt, sequent))
end
›
φlang_parser synthesis (%φparser_synthesis, %φlang_push_val) ["<cartouche>", "<number>"] (‹PROP _›)
‹fn s =>
Parse.position (Parse.group (fn () => "term") (Parse.inner_syntax (Parse.cartouche || Parse.number)))
>> phi_synthesis_parser s (K I)›
φlang_parser get_var (%φparser_unique, %φlang_push_val) ["$"] (‹PROP _›) ‹
fn (oprs,(ctxt,sequent)) => \<^keyword>‹$› |--
Parse.position (Phi_CP_IDE.long_idt_to_triangle (Parse.short_ident || Parse.number))
>> (fn (var,pos) => fn cfg =>
let val get = Phi_Reasoners.wrap'' (Generic_Variable_Access.get_value var Generic_Element_Access.empty_input)
val mode_subproc = Phi_Opr_Stack.precedence_of (#1 oprs) < 0 andalso
(case Thm.prop_of sequent
of Const (\<^const_name>‹Pure.imp›, _) $ _ $ _ => true
| _ => false)
in if mode_subproc
then (oprs, get (ctxt,sequent))
else Phi_Opr_Stack.push_meta_operator cfg
((@{priority %φlang_push_val}, @{priority loose %φlang_push_val}, (0, 0)),
("$", pos), SOME (Phi_Opr_Stack.String_Param var),
(fn _ => fn (oprs, s) => (oprs, get s)))
(oprs,(ctxt,sequent))
end)
›
φlang_parser assignment (%φparser_right_arrow, 0) ["→"] (‹𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?S›) ‹
fn opr_ctxt => (\<^keyword>‹→› |-- Parse.list1 ( Scan.option \<^keyword>‹$› |-- Scan.option Parse.keyword
--| Scan.option \<^keyword>‹$› -- Parse.binding))
>> (fn vars => fn cfg =>
let open Generic_Element_Access
val (vars', _ ) =
fold_map (fn (NONE,b) => (fn k' => ((k',(b,empty_input)),k'))
| (SOME k, b) => (fn _ => ((SOME k, (b,empty_input)), SOME k))) vars NONE
in apsnd (Generic_Variable_Access.assignment_cmd vars') opr_ctxt
end
)›
φlang_parser left_assignment (%φparser_var_decl, 0) ["var", "val"] (‹𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?H] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?S›) ‹
fn opr_ctxt =>
Parse.list1 ((\<^keyword>‹var› || \<^keyword>‹val›) -- Parse.list1 Parse.binding) --
Parse.position (\<^keyword>‹←› || \<^keyword>‹=›)
>> (fn (vars,(_,pos)) => fn cfg =>
let open Generic_Element_Access
val vars' = maps (fn (k,bs) => map (pair (SOME k) o rpair empty_input) bs) vars
in Phi_Opr_Stack.push_meta_operator cfg
((0,@{priority %φlang_assignment}, (0, length vars')),("←",pos),NONE,
fn (_,_,_,vals) => (apsnd (
Generic_Variable_Access.push_values vals
#> Generic_Variable_Access.assignment_cmd vars'
))) opr_ctxt
end
)›
φlang_parser existential_elimination (%φparser_unique, %φlang_expr) ["∃"]
( ‹CurrentConstruction ?mode ?blk ?H (ExBI ?T)›
| ‹ToA_Construction ?s (ExBI ?S)› )
‹fn s => (\<^keyword>‹∃› |-- Parse.list1 Parse.binding) >> (fn insts => fn _ =>
apsnd (Phi_CP_IDE.proof_state_call (NuObtain.choose insts)) s)›
subsubsection ‹Simplifiers \& Reasoners›
subsubsection ‹Post-Application Process›
setup ‹Context.theory_map (
Phi_CP_IDE.Post_App.add 50 (fn arg => fn (ctxt, sequent) =>
case Thm.prop_of sequent
of Const(\<^const_name>‹Pure.imp›, _) $ _ $ _ =>
(case Thm.major_prem_of sequent
of _ $ (Const (\<^const_name>‹Premise›, _) $ _ $ Const (\<^const_name>‹True›, _))
=> (ctxt, @{thm Premise_True} RS sequent)
| _ $ (Const (\<^const_name>‹Premise›, _) $ mode $ prop) => (
if (case mode of Const(\<^const_name>‹default›, _) => true
| Const(\<^const_name>‹MODE_COLLECT›, _) => true
| _ => false) andalso
Config.get ctxt Phi_Reasoner.auto_level >= 2 andalso
not (Symtab.defined (#config arg) "no_oblg") andalso
not (can \<^keyword>‹certified› (#toks arg))
then let val id = Option.map (Phi_ID.encode o Phi_ID.cons (#id arg)) (Phi_ID.get_if_is_named ctxt)
val sequent' = Phi_Reasoners.obligation_intro_Ex_conv ~1 ctxt sequent
in raise Phi_CP_IDE.Post_App.ReEntry (arg, (ctxt,
Phi_Sledgehammer_Solver.auto id (Phi_Envir.freeze_dynamic_lemmas ctxt) sequent'))
handle Phi_Reasoners.Automation_Fail err =>
error (Pretty.string_of (Pretty.chunks (err ())))
end
else (ctxt, sequent))
| _ => (ctxt, sequent)
) | _ => (ctxt, sequent)
)
#> Phi_CP_IDE.Post_App.add 100 (fn arg => fn (ctxt, sequent0) =>
case Thm.prop_of sequent0
of Const(\<^const_name>‹Pure.imp›, _) $ _ $ _ =>
let val sequent = case Thm.major_prem_of sequent0
of Const(\<^const_name>‹Do›, _) $ _ => @{thm Do_I} RS sequent0
| _ => sequent0
in if Config.get ctxt Phi_Reasoner.auto_level >= 1
andalso not (Phi_Sys_Reasoner.is_user_dependent_antecedent (Thm.major_prem_of sequent))
andalso not (Phi_Sys_Reasoner.is_proof_obligation (Thm.major_prem_of sequent))
then (
Phi_Reasoner.info_print ctxt 2 (fn _ =>
"reasoning the leading antecedent of the state sequent." ^ Position.here ⌂) ;
Phi_Reasoner.reason1 (fn () => let open Pretty in string_of (
chunks [para "Fail to solve a φ-LPR antecedent",
Thm.pretty_thm ctxt sequent]
) end)
NONE (SOME 1) ctxt sequent
|> (fn sequent =>
raise Phi_CP_IDE.Post_App.ReEntry (arg, (ctxt, sequent)) ))
else (ctxt, sequent0)
end
| _ => (ctxt, sequent0)
)
#> Phi_CP_IDE.Post_App.add 200 (K (Phi_Sys.move_lemmata Position.none))
#> let val rewr_objects = Phi_Syntax.conv_all_typings (Conv.arg1_conv o Simplifier.rewrite)
in Phi_CP_IDE.Post_App.add 300 (K (fn (ctxt, sequent) =>
let fun conv_conds ctxt ctm = Phi_Conv.hhf_conv conv_conds
(Phi_Conv.hhf_concl_conv (fn ctxt => Conv.try_conv (
PLPR_Syntax.premise_tag_conv (fn Const(\<^const_name>‹default›, _) => true
| Const(\<^const_name>‹MODE_GUARD›, _) => true
| _ => false) (Simplifier.rewrite ctxt))))
ctxt ctm
fun conv_sequent C ctxt =
Conv.gconv_rule (Phi_Conv.hhf_conv conv_conds
(Phi_Conv.tag_conv o C) ctxt) 1
val simplifier =
case Thm.prop_of sequent
of Const(\<^const_name>‹Trueprop›, _) $ _ =>
let val mode = Phi_Working_Mode.mode1 ctxt
in #IDECP_simp mode (ctxt, sequent)
end
| _ => (
case Term.head_of (PLPR_Syntax.dest_tags (Thm.major_prem_of sequent))
of Const(\<^const_name>‹φProcedure›, _) =>
SOME (conv_sequent (fn ctxt =>
Phi_Syntax.procedure_conv Conv.all_conv
(rewr_objects ctxt) (rewr_objects ctxt) (rewr_objects ctxt)))
| Const(\<^const_name>‹View_Shift›, _) =>
SOME (conv_sequent (fn ctxt =>
Phi_Syntax.view_shift_conv (rewr_objects ctxt) (rewr_objects ctxt) Conv.all_conv))
| Const(\<^const_name>‹Transformation›, _) =>
SOME (conv_sequent (fn ctxt =>
Phi_Syntax.view_shift_conv (rewr_objects ctxt) (rewr_objects ctxt) Conv.all_conv))
| _ => NONE)
in case simplifier
of NONE => (ctxt, sequent)
| SOME rewr =>
let val lev = Config.get ctxt Phi_Reasoner.auto_level
val sctxt = if lev <= 0
then raise Phi_CP_IDE.Post_App.Return (ctxt, sequent)
else equip_Phi_Programming_Simp lev ctxt
val sequent' = rewr sctxt sequent
|> Phi_Help.beta_eta_contract
in (ctxt, sequent')
end
end)) end
#> Phi_CP_IDE.Post_App.add 320 (fn arg => fn (ctxt, sequent) =>
case Thm.prop_of sequent
of prop as Const(\<^const_name>‹Trueprop›, _) $ _ =>
(case Phi_Working_Mode.mode ctxt
of SOME mode =>
if #constr_is_ready mode prop
then (case Phi_CoP_Simp.invoke_when_needed (ctxt,mode) sequent
of SOME sequent' => raise Phi_CP_IDE.Post_App.ReEntry (arg, (ctxt, sequent'))
| NONE => (ctxt, sequent))
else (ctxt, sequent)
| NONE => (ctxt, sequent))
| _ => (ctxt, sequent))
#> Phi_CP_IDE.Post_App.add 400 (K (Phi_Sys.move_lemmata Position.none))
#> Phi_CP_IDE.Post_App.add 500 (fn arg => fn s =>
if (case Thm.prop_of (snd s)
of _ $ (Const(\<^const_name>‹PendingConstruction›, _) $ _ $ _ $ _ $ _ $ _) => true
| _ => false) andalso
not (Symtab.defined (#config arg) "no_accept_proc") andalso
not (can \<^keyword>‹throws› (#toks arg))
then raise Phi_CP_IDE.Post_App.ReEntry (arg, Phi_Sys.accept_proc s)
else s)
#> Phi_CP_IDE.Post_App.add 600 (fn arg => fn (ctxt,sequent) =>
if (case Thm.prop_of sequent of Const(\<^const_name>‹Trueprop›, _) $ _ => true
| _ => false) andalso
Config.get ctxt NuObtain.enable_auto andalso
Config.get ctxt Phi_Reasoner.auto_level >= 2 andalso
not (can \<^keyword>‹∃› (#toks arg))
then let val mode = Phi_Working_Mode.mode1 ctxt
in case #spec_of mode (Thm.concl_of sequent)
of Const (\<^const_name>‹ExBI›, _) $ _ =>
raise Phi_CP_IDE.Post_App.ReEntry (arg, Phi_CP_IDE.proof_state_call NuObtain.auto_choose (ctxt,sequent))
| _ => (ctxt,sequent)
end
else (ctxt,sequent)
)
#> Phi_CP_IDE.Post_App.add 999 (K (fn (ctxt, sequent) =>
(Phi_Envir.update_programming_sequent' sequent ctxt, sequent)
))
)›
φlang_parser enter_proof (%φparser_unique, %φlang_expr) ["certified"]
(‹Premise _ _ ⟹ PROP _› | ‹Simplify _ _ _ ⟹ PROP _› | ‹?Bool›)
‹fn stat => \<^keyword>‹certified› |-- Phi_Opr_Stack.end_of_input >> (fn _ => fn cfg => stat
|> apsnd (fn s =>
let val _ = if Thm.no_prems (#2 s) orelse
(case Thm.major_prem_of (#2 s)
of Const(\<^const_name>‹Trueprop›, _) $ (Const(\<^const_name>‹Premise›, _) $ _ $ _)
=> false
| _ => true)
then error "No Subgoal!"
else ()
in s
|> Phi_Reasoners.wrap'' (Phi_Reasoners.obligation_intro_Ex_conv ~1)
|> Phi_CP_IDE.proof_state_call (snd o Phi_Toplevel.prove_prem (cfg,false) I)
end)
|> Phi_Opr_Stack.interrupt
)›
φlang_parser "holds_fact" (%φparser_unique, %φlang_expr) ["holds_fact"] (‹PROP ?P›) ‹
let
val for_fixes = Scan.optional (Parse.$$$ "for" |-- Parse.!!! Parse.params) [];
val statement = Parse.and_list1 (
Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop -- for_fixes);
in
fn (oprs, (ctxt, sequent)) => Parse.position \<^keyword>‹holds_fact› -- statement >> (
fn ((_,pos), raw_statements) => fn _ =>
let val id = Phi_ID.get ctxt
fun gen_name (_, ids) = String.concatWith "_" ("φfact" :: rev_map string_of_int [] ids)
val ctxt' = fold_index (fn (i,(((b', raw_attrs),bodys'),fixes)) => fn ctxt =>
let val id' = Phi_ID.cons [i] id
fun id'' j = if fst id' = "" then NONE else SOME (Phi_ID.encode (Phi_ID.cons [j] id'))
val attrs = map (Attrib.check_src ctxt #> Attrib.attribute_cmd ctxt) raw_attrs
val b = if Binding.is_empty b'
then Binding.make (gen_name id', pos)
else b'
val ctxt' = Proof_Context.add_fixes_cmd fixes ctxt |> snd
|> Phi_Envir.freeze_dynamic_lemmas
val thms = map (Syntax.parse_prop ctxt') bodys'
|> Syntax.check_props ctxt'
|> map_index (fn (j,term) => term
|> Thm.cterm_of ctxt'
|> Goal.init
|> (fn thm => Phi_Sledgehammer_Solver.auto (id'' j) ctxt'
(@{thm Premise_D[where mode=default]} RS thm))
|> Goal.conclude
|> single
|> Variable.export ctxt' ctxt
|> rpair []
)
in snd (Proof_Context.note_thms "" ((b,attrs), thms) ctxt) end
) raw_statements ctxt
in (oprs, (ctxt', sequent))
end
)
end
›
φlang_parser fold (%φparser_unique, %φlang_expr) ["fold"] (‹PROP ?P›) ‹
fn (oprs, (ctxt, sequent)) => Phi_Parse.$$$ "fold" |-- Parse.list1 Parse.thm >> (fn thms => fn _ =>
(oprs, (ctxt, Local_Defs.fold ctxt (Attrib.eval_thms ctxt thms) sequent))
)›
φlang_parser unfold (%φparser_unique, %φlang_expr) ["unfold"] (‹PROP ?P›) ‹
fn (oprs, (ctxt, sequent)) => Phi_Parse.$$$ "unfold" |-- Parse.list1 Parse.thm >> (fn thms => fn _ =>
(oprs, (ctxt, Local_Defs.unfold ctxt (Attrib.eval_thms ctxt thms) sequent))
)›
φlang_parser simplify (%φparser_unique, %φlang_expr) ["simplify"] (‹PROP ?P›) ‹
fn (oprs, (ctxt, sequent)) => Phi_Parse.$$$ "simplify" |-- \<^keyword>‹(› |-- Parse.list Parse.thm --| \<^keyword>‹)›
>> (fn thms => fn _ =>
(oprs, (ctxt, Simplifier.full_simplify (ctxt addsimps Attrib.eval_thms ctxt thms) sequent))
)›
end