Theory IDE_CP_Reasoning3
chapter ‹Reasoning Processes in IDE-CP - Part III›
text ‹Here we give the implementation of all large reasoning processes that are declared in
the previous part I.›
theory IDE_CP_Reasoning3
imports IDE_CP_App2
begin
section ‹Small Processes - I›
consts partial_add_split :: action
non_trivial_partial_add_split :: action
declare [[
φpremise_attribute [unfolded Action_Tag_def] for ‹_ @tag partial_add_split› (%φattr_late_normalize),
φpremise_attribute once? [useful] for ‹_ @tag partial_add_split› (%φattr),
φpremise_attribute [unfolded Action_Tag_def] for ‹_ @tag non_trivial_partial_add_split› (%φattr_late_normalize),
φpremise_attribute once? [useful] for ‹_ @tag non_trivial_partial_add_split› (%φattr)
]]
lemma fst_snt_lambda_pair[simp]:
‹fst o (λx. (f x, g x)) = f›
‹snd o (λx. (f x, g x)) = g›
by (simp add: fun_eq_iff)+
lemma apfst_apsnd_lambda_x_x[simp]:
‹apfst (λx. x) = (λx. x)›
‹apsnd (λx. x) = (λx. x)›
by (simp add: fun_eq_iff)+
section ‹Convergence of Branches›
text ‹The process transforms assertions of form \<^term>‹(If P A B)› into the canonical form (‹∃∧›-MTF).
Assertions \<^term>‹(If P A B)› can be yielded from branch statements.
Data refinements in φ-BI are represented syntactically and the automation upon them is
syntax-driven. We can call ‹∃∧›-MTF canonical because on the form the refinements are expressed
explicitly in a direct syntax. By converting \<^term>‹(If P A B)› into the canonical form, we actually
resolve the join of the refinements from two branches, i.e., we find out for each object what is
its abstraction after the branch join, according to its abstractions in the two branches.
The two branches may have identical φ-types but may disordered. The process sorts the φ-types.
One certain object may be specified by two different refinements. The process
recognizes which two φ-types in the two branches are specifying the object, and applies ToA
to transform one to another.
To recognize this, we rely on syntactic rule binding on each specific φ-type to give an identifier
of the object. An identifier can be a term of any logic type. If the syntactic rule is not given
for a φ-type, we only support the case when the two branches have identical φ-types.
In the implementation, we always transform φ-types in the right-side branch to those in the left side,
i.e., from ‹B› to ‹A› for \<^term>‹(If P A B)›.
›
consts br_join :: ‹action›
definition Identifier_of :: ‹('c,'a) φ ⇒ 'id ⇒ ('c2,'a2) φ ⇒ bool›
where ‹Identifier_of T identifier pattern ≡ True›
φproperty_deriver Identifier_of 555 for (‹Identifier_of _ _ _›)
= ‹Phi_Type_Derivers.meta_Synt_Deriver
("Identifier_of", @{lemma' ‹Identifier_of T identifier pattern› by (simp add: Identifier_of_def)},
SOME @{reasoner_group %cutting})›
subsubsection ‹Conventions›
declare [[φreason_default_pattern
‹If ?P ?A ?B 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ @tag br_join › ⇒ ‹If ?P ?A ?B 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ @tag br_join › (100)
and ‹If ?P ?A ?B = _ @tag br_join › ⇒ ‹If ?P ?A ?B = _ @tag br_join › (100)
and ‹?X @tag br_join › ⇒ ‹ERROR TEXT(‹Bad rule› (?X @tag br_join ))› (0)
and ‹Identifier_of ?T _ _› ⇒ ‹Identifier_of ?T _ _› (100)
]]
φreasoner_group φbr_join_all = (100, [1,3000]) for ‹If C A B @tag br_join›
‹All rules of φ-type branch convergence›
and φbr_join_fail = (1,[1,10]) for ‹If C A B @tag br_join› in φbr_join_all
‹Fallbacks›
and φbr_join_search_counterpart = (30, [28,30]) for ‹If C A B @tag br_join›
in φbr_join_all and > φbr_join_fail
‹Looks from the false-branch for the counterpart of the heading φ-type in the true-branch,
and enters the sub-reasoning for joining the two φ-types.›
and φbr_join_derived = (50,[50,50]) for ‹If C A B @tag br_join›
in φbr_join_all and > φbr_join_search_counterpart
‹Derived from functor properties›
and φbr_join_cut = (1000, [1000, 1030]) for ‹If C A B @tag br_join›
in φbr_join_all > φbr_join_derived
‹Cutting rules›
and φbr_join_spec = (1100, [1100,2000]) for ‹If C A B @tag br_join›
in φbr_join_all and > φbr_join_cut
‹Rules for specific connectives›
and φbr_join_normalize = (2100, [2100,2300]) for ‹If C A B @tag br_join›
in φbr_join_all and > φbr_join_spec
‹Normalization rules›
and φbr_join_red = (2500, [2500, 2800]) for ‹If C A B @tag br_join›
in φbr_join_all and > φbr_join_spec
‹Reductions of high priority›
and φbr_join_red_zero = (2900, [2900,2900]) for ‹If C A B @tag br_join›
in φbr_join_all > φbr_join_red
‹Reductions for zero›
and φbr_join_success = (2990, [2990,3000]) for ‹If C A B @tag br_join›
in φbr_join_all and > φbr_join_red_zero
‹Direct success›
φreasoner_group φidentifier_of = (1000, [1000, 3000]) for ‹Identifier_of T i pattern›
‹User rules giving identifiers of the concrete obejct refining the φ-type abstraction, so that
we can recognize φ-types specifying on an identical object.›
and φidentifier_of_fallback = (10, [10, 10]) for ‹Identifier_of T i pattern›
‹Fallback rules of %φidentifier_of›
subsection ‹Identifier_of›
subsubsection ‹Fallback›
lemma [φreason %φidentifier_of_fallback]:
‹ Identifier_of T T T ›
unfolding Identifier_of_def ..
subsubsection ‹Built-in›
lemma [φreason %φidentifier_of]:
‹ Identifier_of (Val v T) v (Val v T')›
unfolding Identifier_of_def ..
subsection ‹Reasonings of Branch Join›
subsubsection ‹Entry Point›
lemma [φreason %φbr_join_success for ‹If _ _ _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ @tag invoke_br_join›]:
‹ Simplify (assertion_simps undefined) A' A
⟹ Simplify (assertion_simps undefined) B' B
⟹ If P A' B' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 C @tag br_join
⟹ If P A B 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 C @tag invoke_br_join ›
unfolding Action_Tag_def Simplify_def
by blast
subsubsection ‹Fallback and Termination›
lemma [φreason default %φbr_join_fail]:
‹If P A B = If P A B @tag br_join›
unfolding Action_Tag_def ..
lemma [φreason %φbr_join_success for ‹If ?P ?A ?A'' = ?X @tag br_join›]:
‹If P A A = A @tag br_join›
unfolding Action_Tag_def by simp
lemma [φreason default %φbr_join_fail]:
‹ If P A B 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 If P A B @tag br_join ›
unfolding Action_Tag_def
by simp
lemma [φreason default %φbr_join_fail+4]:
" If P T U = Z @tag br_join
⟹ If P (x ⦂ T) (y ⦂ U) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (If P x y ⦂ Z) @tag br_join"
unfolding Action_Tag_def by (cases P; simp)
lemma [φreason %φbr_join_success+5 for ‹If _ (_ ⦂ _) (_ ⦂ _) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ @tag br_join›]:
‹ If P (x ⦂ T) (y ⦂ T) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (If P x y ⦂ T) @tag br_join›
unfolding Action_Tag_def by (cases P; simp)
lemma [φreason %φbr_join_success for ‹If ?P ?A ?A'' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?X @tag br_join›]:
‹If P A A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 A @tag br_join›
unfolding Action_Tag_def Transformation_def by simp
subsubsection ‹Zero›
lemma [φreason %φbr_join_red_zero]:
‹If P A 0 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (A 𝗌𝗎𝖻𝗃 P) @tag br_join›
unfolding Action_Tag_def Transformation_def
by (simp add: zero_set_def)
lemma [φreason %φbr_join_red_zero]:
‹If P 0 A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (A 𝗌𝗎𝖻𝗃 ¬ P) @tag br_join›
unfolding Action_Tag_def Transformation_def
by (simp add: zero_set_def)
subsubsection ‹One›
lemma [φreason %φbr_join_red_zero]:
‹ Identity_Element⇩I A Any
⟹ If P A 1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 1 @tag br_join›
unfolding Identity_Element⇩I_def Action_Tag_def
by (cases P; simp add: transformation_weaken)
lemma [φreason %φbr_join_red_zero]:
‹ Identity_Element⇩I A Any
⟹ If P 1 A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 1 @tag br_join›
unfolding Identity_Element⇩I_def Action_Tag_def
by (cases P; simp add: transformation_weaken)
lemma [φreason %φbr_join_red_zero]:
‹ Identity_Element⇩I A Any
⟹ If P A (x ⦂ ○) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 1 @tag br_join›
unfolding Identity_Element⇩I_def Action_Tag_def
by (cases P; simp add: transformation_weaken)
lemma [φreason %φbr_join_red_zero]:
‹ Identity_Element⇩I A Any
⟹ If P (x ⦂ ○) A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 1 @tag br_join›
unfolding Identity_Element⇩I_def Action_Tag_def
by (cases P; simp add: transformation_weaken)
subsubsection ‹Subjection›
φreasoner_group φbr_join_subj = (%φbr_join_spec+800, [%φbr_join_spec+800, %φbr_join_spec+820]) for ‹If C A B @tag br_join›
in φbr_join_spec
‹Reductions for Subejction›
lemma [φreason %φbr_join_subj+20]:
‹ If P (L 𝗌𝗎𝖻𝗃 Q1 ∧ Q2) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z @tag br_join
⟹ If P (L 𝗌𝗎𝖻𝗃 Q1 𝗌𝗎𝖻𝗃 Q2) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z @tag br_join ›
unfolding Subjection_Subjection .
lemma [φreason %φbr_join_subj+20]:
‹ If P L (R 𝗌𝗎𝖻𝗃 Q1 ∧ Q2) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z @tag br_join
⟹ If P L (R 𝗌𝗎𝖻𝗃 Q1 𝗌𝗎𝖻𝗃 Q2) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z @tag br_join ›
unfolding Subjection_Subjection .
lemma [φreason %φbr_join_subj+10]:
‹ If P QL QR = Q @tag br_join
⟹ If P L R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P (L 𝗌𝗎𝖻𝗃 QL) (R 𝗌𝗎𝖻𝗃 QR) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (X 𝗌𝗎𝖻𝗃 Q) @tag br_join›
unfolding Action_Tag_def Transformation_def by force
lemma [φreason %φbr_join_subj]:
‹ If P L R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P (L 𝗌𝗎𝖻𝗃 Q) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (X 𝗌𝗎𝖻𝗃 P ⟶ Q) @tag br_join›
unfolding Transformation_def Action_Tag_def by simp
lemma [φreason %φbr_join_subj]:
‹ If P L R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P L (R 𝗌𝗎𝖻𝗃 Q) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (X 𝗌𝗎𝖻𝗃 ¬P ⟶ Q) @tag br_join›
unfolding Action_Tag_def Transformation_def by simp
subsubsection ‹Existential›
φreasoner_group φbr_join_ex = (%φbr_join_spec+700, [%φbr_join_spec+700, %φbr_join_spec+720])
for ‹If C A B @tag br_join› in φbr_join_spec and < φbr_join_subj
‹Reductions for Existence›
lemma Conv_Merge_Ex_both_imp:
‹ (⋀x. If P (L x) (R x) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X x @tag br_join)
⟹ If P (∃* x. L x) (∃* x. R x) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (∃* x. X x) @tag br_join ›
unfolding Action_Tag_def Transformation_def
by (cases P; clarsimp simp add: set_eq_iff; blast)
lemma Conv_Merge_Ex_R_imp [φreason %φbr_join_ex]:
‹ (⋀x. If P L (R x) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X x @tag br_join)
⟹ If P L (∃* x. R x) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (∃* x. X x) @tag br_join ›
unfolding Action_Tag_def Transformation_def
by (cases P; simp add: set_eq_iff; blast)
lemma [φreason %φbr_join_ex]:
‹ (⋀x. If P (L x) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X x @tag br_join)
⟹ If P (∃* x. L x) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (∃* x. X x) @tag br_join ›
unfolding Action_Tag_def Transformation_def
by (cases P; simp add: set_eq_iff; blast)
text ‹The merging recognizes two existential quantifier are identical if their type and variable name
are the same. If so it uses Conv_Merge_Ex_both to merge the quantification,
or else the right side is expanded first.›
φreasoner_ML Merge_Existential_imp %φbr_join_ex+20 (‹If ?P (∃* x. ?L x) (∃* x. ?R x) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?X›) = ‹
fn (_, (ctxt,sequent)) =>
let
val ((Const (\<^const_name>‹If›, _) $ _ $ (Const (\<^const_name>‹ExBI›, _) $ Abs (exa,tya,_))
$ (Const (\<^const_name>‹ExBI›, _) $ Abs (exb,tyb,_))), _, _)
= Phi_Syntax.dest_transformation (Thm.major_prem_of sequent)
val sequent' = if exa = exb andalso tya = tyb
then @{thm Conv_Merge_Ex_both_imp} RS sequent
else @{thm Conv_Merge_Ex_R_imp} RS sequent
in Seq.single (ctxt, sequent')
end
›
subsubsection ‹Looks for the counterpart›
definition br_join_counter_part_fail :: ‹'c BI ⇒ 'c BI ⇒ bool›
where ‹br_join_counter_part_fail _ _ ≡ False›
lemma [φreason default %cutting]:
‹ FAIL TEXT(‹φ-Type› (x ⦂ T) ‹is given in the true-branch but its counterpart› B ‹is not seen in the false-branch.› ⏎
‹Perhaps, I should search a more general form › T'' ‹of the counterpart and if so, feed φ-LPR a rule› ⏎
(Identifier_of T identifier T''))
⟹ br_join_counter_part_fail (x ⦂ T) B ›
unfolding FAIL_def
by blast
lemma [φreason default %φbr_join_search_counterpart]:
‹ Identifier_of T identifier T'
⟹ (R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ T' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R') ∨⇩c⇩u⇩t
br_join_counter_part_fail (x ⦂ T) (y ⦂ T')
⟹ If P (x ⦂ T) (y ⦂ T') 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z @tag br_join
⟹ If P L R' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P ((x ⦂ T) * L) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z * X @tag br_join›
unfolding Action_Tag_def Transformation_def Premise_def Orelse_shortcut_def
br_join_counter_part_fail_def
by (cases P; clarsimp; blast)
lemma [φreason default %φbr_join_search_counterpart]:
‹ Identifier_of T identifier T'
⟹ (y, w) ⦂ U ✼ W 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y' ⦂ T' ✼ U'⇩R @tag 𝒯𝒫'
⟹ Identity_Element⇩E (w ⦂ W) ∨⇩c⇩u⇩t br_join_counter_part_fail (fst x ⦂ T) (y'' ⦂ T')
⟹ If P (fst x ⦂ T) (fst y' ⦂ T') 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z @tag br_join
⟹ If P (snd x ⦂ T⇩R) (snd y' ⦂ U'⇩R) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z⇩R @tag br_join
⟹ Z * Z⇩R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z' @clean
⟹ If P (x ⦂ T ∗ T⇩R) (y ⦂ U) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Z' @tag br_join ›
for Z' :: ‹'c::sep_magma_1 BI›
unfolding Action_Tag_def Transformation_def Premise_def br_join_counter_part_fail_def
Orelse_shortcut_def Ant_Seq_def Identity_Element⇩I_def Identity_Element⇩E_def φProd'_def
by ((cases P; clarsimp), blast, metis mult_1_class.mult_1_right sep_magma_1_left)
lemma Br_join_atom_assertion[no_atp]:
‹ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 A 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R'
⟹ If P L R' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P (A * L) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 A * X @tag br_join ›
unfolding Action_Tag_def
by ((cases P; simp), simp add: transformation_left_frame,
metis REMAINS_def mk_elim_transformation transformation_left_frame)
lemma Br_join_atom_assertion'[no_atp]:
‹ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 A
⟹ If P A R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 A @tag br_join ›
unfolding Action_Tag_def
by (cases P; simp)
subsubsection ‹Joapplyin Two φ-Types›
φreasoner_group br_join_fallback = (20, [11,20]) for ‹If C (x ⦂ T) (y ⦂ U) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y @tag br_join›
in φbr_join_all and > φbr_join_fail
‹Fallbacks of joining two φ-types, using ToA›
paragraph ‹Fallback by ToA›
definition Common_Base_Types :: ‹('c,'a1) φ ⇒ ('c,'a2) φ ⇒ ('c,'a3) φ ⇒ bool›
where ‹Common_Base_Types T U Base ≡ True›
φreasoner_group Common_Base_Types = (1000, [1000,1100])
‹specifying the common base type between two given types, used in by_join.›
and Common_Base_Types_derived = (40, [40,50]) ‹derived›
and Common_Base_Types_fallback = (10, [10,20])
‹fallbacks›
declare [[
φdefault_reasoner_group ‹Common_Base_Types _ _ _› : %Common_Base_Types (100),
φreason_default_pattern ‹Common_Base_Types ?T ?U _› ⇒ ‹Common_Base_Types ?T ?U _› (100)
]]
φproperty_deriver Common_Base_Types 555 for (‹Common_Base_Types _ _ _›)
= ‹Phi_Type_Derivers.meta_Synt_Deriver
("Common_Base_Types", @{lemma' ‹Common_Base_Types T U Base› by (simp add: Common_Base_Types_def)},
SOME @{reasoner_group %cutting})›
lemma [φreason default %Common_Base_Types_fallback]:
‹Common_Base_Types T U T›
unfolding Common_Base_Types_def by simp
lemma [φreason default %br_join_fallback]:
‹ Common_Base_Types T U V
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 P ⟹ 𝗀𝗎𝖺𝗋𝖽 x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x' ⦂ V)
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 ¬ P ⟹ 𝗀𝗎𝖺𝗋𝖽 y ⦂ U 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y' ⦂ V)
⟹ If P (x ⦂ T) (y ⦂ U) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 If P x' y' ⦂ V @tag br_join ›
unfolding Action_Tag_def Transformation_def 𝗋Guard_def Premise_def
by clarsimp
φreasoner_ML br_join_fallback %br_join_fallback-4 (‹If _ (_ ⦂ _) (_ ⦂ _) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ @tag br_join›) = ‹
fn (_, (ctxt, sequent)) => Seq.make (fn () =>
let exception NOT_AVAILABLE
fun conv ctm =
let val (A,B) = case Thm.term_of ctm of Const(\<^const_name>‹If›, _) $ _ $ A $ B => (A,B)
in if A aconv B
then Conv.rewr_conv @{thm' if_cancel} ctm
else case (A,B)
of (Const(\<^const_name>‹φType›, _) $ x $ T, Const(\<^const_name>‹φType›, _) $ x' $ T') =>
if Term.head_of T aconv Term.head_of T'
then (Conv.rewr_conv @{lemma' ‹If P (x ⦂ T) (y ⦂ U) ≡ (If P x y) ⦂ (If P T U)›
by (unfold atomize_eq, cases P, simp, simp)}
then_conv Conv.arg_conv conv) ctm
else raise NOT_AVAILABLE
| (F $ x, G $ y) =>
let val Pc = Thm.dest_arg (Thm.dest_fun2 ctm)
val (Ac, Bc) = (Thm.dest_arg1 ctm, Thm.dest_arg ctm)
val (Fc, xc) = (Thm.dest_fun Ac, Thm.dest_arg Ac)
val (Gc, yc) = (Thm.dest_fun Bc, Thm.dest_arg Bc)
in if x aconv y
then (Conv.rewr_conv (@{print} \<^instantiate>‹
C=Pc and fa=Fc and fb=Gc and a=xc and
'b=‹Thm.ctyp_of_cterm xc› and 'a=‹Thm.dest_ctyp1 (Thm.ctyp_of_cterm Fc)›
in lemma ‹if C then fa a else fb a ≡ (if C then fa else fb) a›
by (simp add: if_distribR)›)
then_conv Conv.fun_conv conv) ctm
else if F aconv G
then Conv.rewr_conv \<^instantiate>‹
c=Pc and f=Fc and x=xc and y=yc and
'b=‹Thm.ctyp_of_cterm xc› and 'a=‹Thm.dest_ctyp1 (Thm.ctyp_of_cterm Fc)›
in lemma ‹(if c then f x else f y) ≡ f (if c then x else y)›
by (unfold atomize_eq, cases c, simp, simp)› ctm
else (Conv.rewr_conv \<^instantiate>‹
C=Pc and fa=Fc and fb=Gc and va=xc and vb=yc and
'b=‹Thm.ctyp_of_cterm xc› and 'a=‹Thm.dest_ctyp1 (Thm.ctyp_of_cterm Fc)›
in lemma ‹if C then fa va else fb vb ≡ (if C then fa else fb) (if C then va else vb)›
by (simp add: If_distrib_fx)›
then_conv Conv.fun_conv conv) ctm
end
end
in let
val sequent'1 = Conv.gconv_rule (
Phi_Conv.hhf_concl_conv (fn ctxt =>
Phi_Syntax.transformation_conv conv Conv.all_conv Conv.all_conv
) ctxt ) 1 sequent
val sequent'2 = @{thm' transformation_refl} RS (@{thm' Action_Tag_I} RS sequent'1)
in SOME ((ctxt, sequent'2), Seq.empty)
end
handle NOT_AVAILABLE => NONE
| E => error "!!!"
end)
›
lemma [φreason default %br_join_fallback-8]:
‹ WARNING TEXT(‹Fail to join φtype› T ‹and› U)
⟹ If P (x ⦂ T) (y ⦂ U) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 If P x y ⦂ If P T U @tag br_join ›
unfolding Action_Tag_def Transformation_def
by (cases P; clarsimp)
paragraph ‹By Transformation Functor›
definition Gen_Br_Join :: ‹ 'a ⇒ 'b ⇒ 'c
⇒ bool ⇒ bool
⇒ bool ›
where ‹ Gen_Br_Join F⇩T F⇩U F' P conds ≡ True ›
setup ‹PLPR_Template_Properties.add_property_kinds [
\<^pattern_prop>‹Gen_Br_Join _ _ _ _ _›
]›
φproperty_deriver Gen_Br_Join 555 for (‹Gen_Br_Join _ _ _ _ _›)
= ‹Phi_Type_Derivers.meta_Synt_Deriver
("Gen_Br_Join", @{lemma' ‹Gen_Br_Join F⇩T F⇩U F' P conds› by (simp add: Gen_Br_Join_def)},
SOME @{reasoner_group %cutting})›
φreasoner_ML Default_Simplify %cutting (‹𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[br_join] _ : _›)
= ‹ Phi_Reasoners.wrap (PLPR_Simplifier.simplifier (K Seq.empty)
(fn ctxt => ctxt addsimps Useful_Thms.get ctxt
|> Simplifier.del_cong @{thm' if_weak_cong}
|> Simplifier.add_cong @{thm' if_cong}) {fix_vars=true})
o snd›
lemma [φreason_template default %φbr_join_derived]:
‹ Gen_Br_Join F⇩T F⇩U F' P conds
⟹ 𝗀𝗎𝖺𝗋𝖽 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 conds
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 conds ∧ P ⟹ Functional_Transformation_Functor F⇩T F' T Z D⇩T R⇩T pm⇩T fm⇩T)
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 conds ∧ ¬ P ⟹ Functional_Transformation_Functor F⇩U F' U Z D⇩U R⇩U pm⇩U fm⇩U)
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (∀a ∈ D⇩T x. z (Inl a) ∈ R⇩T x) ∧
(∀b ∈ D⇩U y. z (Inr b) ∈ R⇩U y)
⟹ (⋀a ∈ (If P (Inl ` D⇩T x) (Inr ` D⇩U y)). If P (projl a ⦂ T) (projr a ⦂ U) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 z a ⦂ Z @tag br_join)
⟹ (𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[φinstantiation] zzz : (If P (fm⇩T (λx. z (Inl x)) (λ_. True) x) (fm⇩U (λx. z (Inr x)) (λ_. True) y))) @tag 𝒜_template_reason undefined
⟹ NO_SIMP (If P (x ⦂ F⇩T T) (y ⦂ F⇩U U)) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 zzz ⦂ F' Z @tag br_join ›
unfolding Action_Tag_def Premise_def Functional_Transformation_Functor_def Transformation_def
meta_Ball_def meta_case_prod_def Simplify_def 𝗋Guard_def NO_SIMP_def
by (cases P; clarsimp)
lemma [φreason_template default %φbr_join_derived]:
‹ Gen_Br_Join F⇩T F⇩U F' P conds
⟹ 𝗀𝗎𝖺𝗋𝖽 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 conds
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 conds ∧ P ⟹ Functional_Transformation_Functor⇩Λ F⇩T F' T Z D⇩T R⇩T pm⇩T fm⇩T)
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 conds ∧ ¬ P ⟹ Functional_Transformation_Functor⇩Λ F⇩U F' U Z D⇩U R⇩U pm⇩U fm⇩U)
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (∀p. ∀a ∈ D⇩T p x. z p (Inl a) ∈ R⇩T p x) ∧
(∀p. ∀b ∈ D⇩U p y. z p (Inr b) ∈ R⇩U p y)
⟹ (⋀p. ⋀a ∈ (If P (Inl ` D⇩T p x) (Inr ` D⇩U p y)). If P (projl a ⦂ T p) (projr a ⦂ U p) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 z p a ⦂ Z p @tag br_join)
⟹ NO_SIMP (If P (x ⦂ F⇩T T) (y ⦂ F⇩U U)) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌
(If P (fm⇩T (λp. z p o Inl) (λ_ _. True) x) (fm⇩U (λp. z p o Inr) (λ_ _. True) y)) ⦂ F' Z @tag br_join ›
unfolding Action_Tag_def Premise_def Functional_Transformation_Functor⇩Λ_def Transformation_def
meta_Ball_def meta_case_prod_def Simplify_def 𝗋Guard_def NO_SIMP_def
by (cases P; clarsimp)
let_φtype Set_Abst deriving ‹Gen_Br_Join 𝒮 𝒮 𝒮 P True›
let_φtype φComposition deriving ‹Gen_Br_Join ((⨾) B) ((⨾) B') ((⨾) B) P (B = B')›
let_φtype φMul_Quant deriving ‹Gen_Br_Join (✱⇧φ⇩0 I) (✱⇧φ⇩0 J) (✱⇧φ⇩0 (If P I J)) P True›
let_φtype φMul_Quant⇩Λ deriving ‹Gen_Br_Join (✱⇧φ I) (✱⇧φ J) (✱⇧φ (If P I J)) P True›
let_φtype φScalarMul deriving ‹Gen_Br_Join (φScalarMul f s) (φScalarMul f s') (φScalarMul f s) P (s' = s)›
let_φtype List_Item deriving ‹Gen_Br_Join List_Item List_Item List_Item P True›
let_φtype φFun' deriving ‹Gen_Br_Join ((⨾⇩f) f) ((⨾⇩f) f') ((⨾⇩f) f) P (f' = f)›
let_φtype φSome deriving ‹Gen_Br_Join φSome φSome φSome P True›
let_φtype φMapAt deriving ‹Gen_Br_Join ((❙→) k) ((❙→) k') ((❙→) k) P (k' = k)›
let_φtype φMapAt_L deriving ‹Gen_Br_Join ((❙→⇩@) k) ((❙→⇩@) k') ((❙→⇩@) k) P (k' = k)›
let_φtype φShare deriving ‹Gen_Br_Join ((⨸) n) ((⨸) m) ((⨸) (If P n m)) P True›
let_φtype Discrete deriving ‹Gen_Br_Join Discrete Discrete Discrete P True›
let_φtype Val deriving ‹Gen_Br_Join (Val v) (Val v) (Val v) P True›
lemma [φreason_template default %Common_Base_Types_derived]:
‹ Functional_Transformation_Functor F⇩T F' T V D⇩T R⇩T pm⇩T fm⇩T
⟹ Functional_Transformation_Functor F⇩U F' U V D⇩U R⇩U pm⇩U fm⇩U
⟹ Common_Base_Types T U V
⟹ Common_Base_Types (F⇩T T) (F⇩U U) (F' V) ›
unfolding Common_Base_Types_def
by simp
lemma [φreason add]:
‹ Common_Base_Types T U V
⟹ Common_Base_Types (◒ T) (● U) (◒ V)›
unfolding Common_Base_Types_def
by simp
lemma [φreason add]:
‹ Common_Base_Types T U V
⟹ Common_Base_Types (● T) (◒ U) (◒ V)›
unfolding Common_Base_Types_def
by simp
subsubsection ‹Unfold›
lemma [φreason %φbr_join_normalize]:
" If P L (N * (R1 * R2)) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P L (N * R1 * R2) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join"
for N :: ‹'a::sep_semigroup BI›
unfolding Action_Tag_def by (metis mult.assoc)
lemma [φreason %φbr_join_normalize]:
" If P (L1 * (L2 * L3)) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P (L1 * L2 * L3) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join"
for R :: ‹'a::sep_semigroup BI›
unfolding Action_Tag_def by (metis mult.assoc)
subsubsection ‹Eliminate Void Hole›
lemma [φreason %φbr_join_normalize]:
" If P L R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P L (R * 1) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join"
for R :: ‹'a::sep_magma_1 BI›
unfolding Action_Tag_def by (cases P; simp)
lemma [φreason %φbr_join_normalize]:
" If P L R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P L (1 * R) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join"
for R :: ‹'a::sep_magma_1 BI›
unfolding Action_Tag_def by (cases P; simp)
lemma [φreason %φbr_join_normalize]:
" If P L (R' * R) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P L (R' * 1 * R) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join"
for R :: ‹'a::sep_magma_1 BI›
unfolding Action_Tag_def by (cases P; simp)
lemma [φreason %φbr_join_normalize]:
" If P L R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P (L * 1) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join"
for R :: ‹'a::sep_magma_1 BI›
unfolding Action_Tag_def by (cases P; simp)
lemma [φreason %φbr_join_normalize]:
" If P L R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join
⟹ If P (1 * L) R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X @tag br_join"
for R :: ‹'a::sep_magma_1 BI›
unfolding Action_Tag_def by (cases P; simp)
section ‹Implementation of Synthesis Mechanism›
subsubsection ‹Multi-Target›
lemma [φreason %φsynthesis_split+20]:
‹ 𝗉𝗋𝗈𝖼 f1 ⦃ R1 ⟼ λret. A ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 f2 ⦃ R2 ⟼ λret. B ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 (f1 ⤜ (λv1. f2 ⤜ (λv2. Return (φV_pair v1 v2))))
⦃ R1 ⟼ λret. A (φV_fst ret)❟ B (φV_snd ret) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E1 e + (E2 e❟ ExBI A)) @tag synthesis›
❴ premises F1 and F2
F1 F2 ‹A 𝗏0›
❵ .
lemma [φreason %φsynthesis_split]:
‹ 𝗉𝗋𝗈𝖼 f1 ⦃ R1 ⟼ λret. A ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 f2 ⦃ R2 ⟼ λret. B 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 (f1 ⤜ (λv. f2 ⪢ Return v)) ⦃ R1 ⟼ λret. A ret ❟ B 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E1 e + (ExBI A ❟ E2 e)) @tag synthesis›
❴ premises F1 and F2
F1 F2
❵ .
lemma [φreason %φsynthesis_split+10]:
‹ 𝗉𝗋𝗈𝖼 f1 ⦃ R1 ⟼ λret. A 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 f2 ⦃ R2 ⟼ λret. B ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 (f1 ⪢ f2) ⦃ R1 ⟼ λret. A ❟ B ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E1 e + (A ❟ E2 e)) @tag synthesis›
❴ premises F1 and F2
F1 F2
❵ .
lemma [φreason %φsynthesis_split+20]:
‹ 𝗉𝗋𝗈𝖼 f1 ⦃ R1 ⟼ λret::unit φarg. A 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 f2 ⦃ R2 ⟼ λret::unit φarg. B 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 (f1 ⪢ f2) ⦃ R1 ⟼ λret. A ❟ B 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E1 e + (A ❟ E2 e)) @tag synthesis›
❴ premises F1 and F2
F1 F2
❵ .
section ‹Generation of Synthesis Rule›
definition Gen_Synthesis_Rule :: ‹prop ⇒ prop ⇒ prop ⇒ prop›
where ‹Gen_Synthesis_Rule Given Antecedents Result
≡ ((PROP Antecedents ⟹ PROP Given) ⟹ PROP Result)›
declare [[φreason_default_pattern
‹PROP Gen_Synthesis_Rule ?G ?A _› ⇒ ‹PROP Gen_Synthesis_Rule ?G ?A _› (100)
]]
lemma Gen_Synthesis_Rule:
‹ PROP G
⟹ PROP Gen_Synthesis_Rule G PURE_TOP R
⟹ 𝗋Success
⟹ PROP R›
unfolding Gen_Synthesis_Rule_def PURE_TOP_imp .
ML_file ‹library/additions/gen_synthesis_rule.ML›
subsubsection ‹Conventions›
declare [[generate_pattern_of_synthesis_rule
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜 &&& TERM ()› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜› (120)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜 &&& TERM ?Z› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜› (110)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜 &&& (TERM ?X &&& TERM ?Z)› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜› (110)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜 &&& TERM ()› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜› (125)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. _ ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜 &&& TERM ?z› ⇒
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?z ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag ?𝒜› (106)
and ‹(?X::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜 &&& TERM ()› ⇒
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜› (120)
and ‹(?X::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜 &&& TERM ?Z› ⇒
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜› (110)
and ‹ _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜 &&& (TERM ?X &&& TERM ?Z)› ⇒
‹(?X::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Z 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜› (110)
and ‹(?X::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜 &&& TERM ()› ⇒
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜› (125)
and ‹(?X::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜 &&& TERM ?z› ⇒
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?z ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag ?𝒜› (106)
]]
φreasoner_group φsynthesis_gen = (1000, [1, 3000]) for ‹PROP Gen_Synthesis_Rule (PROP _) (PROP _) (PROP _)›
‹All rules describing how to convert a given lemma to a synthesis rule›
and φsynthesis_gen_hhf = (1000, [1000, 1000]) in φsynthesis_gen
‹handling meta structure of the given lemma as a HHF rule, though actually only meta imp
is considered because no meta all should occur in a normalized HHF rule.›
and φsynthesis_gen_ToA = (1000, [10,3000]) in φsynthesis_gen
‹when the given lemma is a ToA›
and φsynthesis_gen_proc = (1000, [10,3000]) in φsynthesis_gen
‹when the given lemma is a procedure›
attribute_setup φsynthesis = ‹
let val arrow = (\<^keyword>‹=>› || \<^keyword>‹⇒›)
fun named_term2 read =
Args.internal_term --| arrow -- Args.internal_term ||
Parse.token Parse.embedded --| arrow -- Parse.token Parse.embedded
>> (fn (tok1, tok2) =>
let val [term1, term2] = read [Token.inner_syntax_of tok1, Token.inner_syntax_of tok2]
in Token.assign (SOME (Token.Term term1)) tok1 ;
Token.assign (SOME (Token.Term term2)) tok2 ;
(term1, term2)
end)
val pattern = Scan.peek (fn ctxt =>
let val ctxt' = Proof_Context.set_mode Proof_Context.mode_pattern (Context.proof_of ctxt)
fun read_term raw =
let val raw1 = map (Syntax.parse_term ctxt') raw
fun chk tagged [] = Syntax.check_terms ctxt' tagged
| chk tagged (X::L) =
(chk (Type.constraint \<^typ>‹_::type φarg ⇒ assn› X :: tagged) L
handle ERROR err =>
chk (Type.constraint \<^typ>‹assn› X :: tagged) L
handle ERROR _ => raise (ERROR err))
val terms = chk [] (rev raw1)
val ctxt'' = fold Proof_Context.augment terms ctxt'
val terms' = Variable.export_terms ctxt'' ctxt' terms
in terms' end
in (Args.$$$ "_" >> (K Phi_Synthesis.No_Pattern))
|| named_term2 read_term >> Phi_Synthesis.Arg_and_Ret
|| (Args.named_term (singleton read_term) >> Phi_Synthesis.Ret_only)
end )
val priority = Scan.lift (Scan.option (\<^keyword>‹(› |-- Reasoner_Group.parser --| \<^keyword>‹)›))
val pat2 = (Scan.optional (Scan.lift \<^keyword>‹for› |-- Parse.and_list1' (pattern -- priority)) [] --
Scan.optional (Scan.lift \<^keyword>‹except› |-- Parse.and_list1' pattern) [] )
in Phi_Reasoner.attr_syntax' pat2
(fn (pos, mode, group, raw_pats) =>
Thm.declaration_attribute (fn rule => fn ctxt =>
let val pats = apfst (map (apsnd (Option.map (fst o Reasoner_Group.check_group true ctxt)))) raw_pats
in Phi_Synthesis.declare_rule pos (mode, SOME (the_default @{reasoner_group %φsynthesis} group))
pats rule ctxt
end))
end
›
declare [[φreason_default_pattern
‹PROP Gen_Synthesis_Rule
(Trueprop (𝗉𝗋𝗈𝖼 _ ⦃ ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ ⟼ ?Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _))
(PROP ?P) (PROP _)›
⇒ ‹PROP Gen_Synthesis_Rule
(Trueprop (𝗉𝗋𝗈𝖼 _ ⦃ ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ ⟼ ?Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _))
(PROP ?P) (PROP _)› (120)
and ‹PROP Gen_Synthesis_Rule
(Trueprop (𝗉𝗋𝗈𝖼 _ ⦃ ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ ⟼ λr. ?Y r 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?RN ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _))
(PROP ?P) (PROP _)›
⇒ ‹PROP Gen_Synthesis_Rule
(Trueprop (𝗉𝗋𝗈𝖼 _ ⦃ ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ ⟼ λr. ?Y r 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?RN'' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _))
(PROP ?P) (PROP _)› (125)
and ‹PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 ?f v ⦃ ?X v 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⟼ ?Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E))
(PROP ?P) (PROP _)›
⇒ ‹PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 ?f' v ⦃ ?X v 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⟼ ?Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E'))
(PROP ?P) (PROP _)› (120)
and ‹PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 ?f v ⦃ ?X v 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⟼ λr. ?Y r 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?RN ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _))
(PROP ?P) (PROP _)›
⇒ ‹PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 ?f' v ⦃ ?X' v 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⟼ λr. ?Y r 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?RN'' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _))
(PROP ?P) (PROP _)› (125)
]]
subsection ‹General Rule›
lemma [φreason %φsynthesis_gen_hhf]:
‹ PROP Gen_Synthesis_Rule Q (PROP Ant &&& PROP P) X
⟹ PROP Gen_Synthesis_Rule (PROP P ⟹ PROP Q) Ant X›
unfolding Gen_Synthesis_Rule_def conjunction_imp
subgoal premises P by (rule P(1), rule P(2), assumption, assumption) .
subsection ‹Synthesis Mode›
definition synthesis_gen_mode :: ‹'c BI ⇒ action ⇒ bool›
where ‹synthesis_gen_mode Assertion Mode ≡ True›
declare [[φreason_default_pattern ‹synthesis_gen_mode ?A _› ⇒ ‹synthesis_gen_mode ?A _› (100)]]
φreasoner_group synthesis_gen_mode_all = (1000, [10,2000]) for ‹synthesis_gen_mode A M›
‹determines whether the rule to be generated is in normal mode or overloaded mode›
and synthesis_gen_mode_default = (10,[10,10]) in synthesis_gen_mode_all
‹the default is normal mode›
and synthesis_gen_mode_overridded = (1000, [1000,1000]) in synthesis_gen_mode_all > synthesis_gen_mode_default ‹›
and synthesis_gen_mode_pass = (1200, [1200, 1200]) in synthesis_gen_mode_all and > synthesis_gen_mode_overridded ‹›
lemma [φreason default %synthesis_gen_mode_default]:
‹ synthesis_gen_mode A synthesis ›
unfolding synthesis_gen_mode_def ..
paragraph ‹Passes›
lemma [φreason %synthesis_gen_mode_pass]:
‹ synthesis_gen_mode A M
⟹ synthesis_gen_mode (A 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) M ›
unfolding synthesis_gen_mode_def REMAINS_def ..
subsection ‹ToA›
φreasoner_group φsynthesis_gen_ToA_default = (10, [10,10]) in φsynthesis_gen_ToA ‹›
and φsynthesis_gen_ToA_convert = (50, [11,80]) in φsynthesis_gen_ToA
‹Synthesis ToA rules must be on fiction algebra. The group tries to convert ToAs that are not
on the fiction algebra.›
subsubsection ‹Conversion›
lemma [φreason default %φsynthesis_gen_ToA_convert]:
‹ PROP Gen_Synthesis_Rule
(Trueprop (x ⦂ 𝗏𝖺𝗅[v] T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (y ⦂ 𝗏𝖺𝗅[v] U :: assn) 𝗐𝗂𝗍𝗁 P))
Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ U 𝗐𝗂𝗍𝗁 P))
Ant Result ›
unfolding Gen_Synthesis_Rule_def Transformation_def
by clarsimp
subsubsection ‹Success›
lemma Gen_Synthesis_Rule_transformation_12:
‹ synthesis_gen_mode Y mode
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[assertion_simps SOURCE] X' : X * R
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[assertion_simps TARGET] Y' : Yr * R
⟹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y * Yr 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Y' 𝗐𝗂𝗍𝗁 P @tag mode) ›
for X :: assn
unfolding Gen_Synthesis_Rule_def Action_Tag_def Simplify_def REMAINS_def
by (simp; rule transformation_right_frame[where U=‹Y * Yr›, simplified mult.assoc]; simp)
lemma Gen_Synthesis_Rule_transformation_11:
‹ synthesis_gen_mode Y mode
⟹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X * R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag mode) ›
for X :: assn
unfolding Gen_Synthesis_Rule_def Action_Tag_def REMAINS_def
by (rule transformation_right_frame, simp)
lemma Gen_Synthesis_Rule_transformation_01:
‹ synthesis_gen_mode Y mode
⟹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y * R 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag mode) ›
for X :: assn
unfolding Gen_Synthesis_Rule_def Action_Tag_def REMAINS_def
by simp
lemma Gen_Synthesis_Rule_transformation_00:
‹ synthesis_gen_mode Y mode
⟹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P @tag mode) ›
for X :: assn
unfolding Gen_Synthesis_Rule_def Action_Tag_def
by simp
φreasoner_ML Gen_Synthesis_Rule_transformation %φsynthesis_gen_ToA_default
(‹PROP Gen_Synthesis_Rule (Trueprop ((_::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ 𝗐𝗂𝗍𝗁 _)) (PROP _) (PROP _)›)
= ‹fn (_,(ctxt,sequent)) => Seq.make (fn () =>
let val _ $ (_ $ TM) $ _ $ _ = Thm.major_prem_of sequent
fun last_ele (Const (\<^const_name>‹times›, _) $ _ $ X ) = last_ele X
| last_ele X = X
fun first_ele (Const (\<^const_name>‹times›, _) $ X $ _ ) = first_ele X
| first_ele X = X
val (has_R,X,Y) =
case TM
of Const(\<^const_name>‹Transformation›, _) $ X $ Y $ _ => (last_ele X = last_ele Y,X,Y)
| Const(\<^const_name>‹View_Shift›, _) $ X $ Y $ _ => (last_ele X = last_ele Y,X,Y)
fun warn () = warning "You have multiple separated items and it is unclear which one is \
\the target to be synthesised or the residue of the synthesis.\n\
\We assume the synthesis target is the first item.\n\
\You should use ‹ Target 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Residue › to annotate the target."
fun chk_target (Abs (_,_,tm)) = chk_target tm
| chk_target (Const (\<^const_name>‹ExBI›, _) $ _)
= error ("Exisential quantification has not been supported in synthesis.")
| chk_target (Const (\<^const_name>‹Subjection›, _) $ _ $ _)
= Phi_Reasoner.bad_config "Subjection shouldn't occur here."
| chk_target (Const (\<^const_name>‹REMAINS›, _) $ _ $ _)
= @{thm' Gen_Synthesis_Rule_transformation_00} RS sequent
| chk_target (Const (\<^const_name>‹times›, _) $ (Const (\<^const_name>‹times›, _) $ _ $ _) $ _)
= (warn () ;
if has_R then @{thm' Gen_Synthesis_Rule_transformation_01} RS sequent
else @{thm' Gen_Synthesis_Rule_transformation_12} RS sequent)
| chk_target (Const (\<^const_name>‹times›, _) $ _ $ _)
= if has_R then @{thm' Gen_Synthesis_Rule_transformation_01} RS sequent
else (warn (); @{thm' Gen_Synthesis_Rule_transformation_12} RS sequent)
| chk_target _ = @{thm Gen_Synthesis_Rule_transformation_11} RS sequent
in case X of Const (\<^const_name>‹REMAINS›, _) $ _ $ _ => NONE
| _ => SOME ((ctxt, chk_target Y), Seq.empty)
end)›
subsection ‹View Shift›
lemma Gen_Synthesis_Rule_VS_12:
‹ synthesis_gen_mode Y mode
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[assertion_simps SOURCE] X' : X * R
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[assertion_simps TARGET] Y' : Yr * R
⟹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗌𝗁𝗂𝖿𝗍𝗌 Y * Yr 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X' 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Y' 𝗐𝗂𝗍𝗁 P @tag mode) ›
unfolding Gen_Synthesis_Rule_def Action_Tag_def Simplify_def REMAINS_def
by (simp; rule φview_shift_intro_frame[where U=‹Y * Yr›, unfolded mult.assoc]; simp)
lemma Gen_Synthesis_Rule_VS_11:
‹ synthesis_gen_mode Y mode
⟹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X * R 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag mode) ›
unfolding Gen_Synthesis_Rule_def Action_Tag_def REMAINS_def
by (rule φview_shift_intro_frame, simp)
lemma Gen_Synthesis_Rule_VS_01:
‹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗌𝗁𝗂𝖿𝗍𝗌 Y * R 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag synthesis) ›
unfolding Gen_Synthesis_Rule_def Action_Tag_def REMAINS_def
by simp
lemma Gen_Synthesis_Rule_VS_00:
‹ PROP Gen_Synthesis_Rule
(Trueprop (X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P))
Ant
(PROP Ant ⟹ X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P @tag synthesis) ›
unfolding Gen_Synthesis_Rule_def Action_Tag_def
by simp
φreasoner_ML Gen_Synthesis_Rule_VS 10
(‹PROP Gen_Synthesis_Rule (Trueprop (_ 𝗌𝗁𝗂𝖿𝗍𝗌 _ 𝗐𝗂𝗍𝗁 _)) (PROP _) (PROP _)›)
= ‹fn (_,(ctxt,sequent)) => Seq.make (fn () =>
let val _ $ (_ $ TM) $ _ $ _ = Thm.major_prem_of sequent
fun last_ele (Const (\<^const_name>‹times›, _) $ _ $ X ) = last_ele X
| last_ele X = X
val (has_R,X,Y) =
case TM
of Const(\<^const_name>‹Transformation›, _) $ X $ Y $ _ => (last_ele X = last_ele Y,X,Y)
| Const(\<^const_name>‹View_Shift›, _) $ X $ Y $ _ => (last_ele X = last_ele Y,X,Y)
fun warn () = warning "You have multiple separated items and it is unclear which one is \
\the target to be synthesised or the residue of the synthesis.\n\
\We assume the synthesis target is the last item.\n\
\You should use ‹ Target 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Residue › to annotate the target."
fun chk_target (Abs (_,_,tm)) = chk_target tm
| chk_target (Const (\<^const_name>‹ExBI›, _) $ _)
= error ("Exisential quantification has not been supported in synthesis.")
| chk_target (Const (\<^const_name>‹Subjection›, _) $ _ $ _)
= Phi_Reasoner.bad_config "Subjection shouldn't occur here."
| chk_target (Const (\<^const_name>‹REMAINS›, _) $ _ $ _)
= @{thm' Gen_Synthesis_Rule_VS_00} RS sequent
| chk_target (Const (\<^const_name>‹times›, _) $ (Const (\<^const_name>‹times›, _) $ _ $ _) $ _)
= (warn () ;
if has_R then @{thm' Gen_Synthesis_Rule_VS_01} RS sequent
else @{thm' Gen_Synthesis_Rule_VS_12} RS sequent)
| chk_target (Const (\<^const_name>‹times›, _) $ _ $ _)
= if has_R then @{thm' Gen_Synthesis_Rule_VS_01} RS sequent
else (warn (); @{thm' Gen_Synthesis_Rule_VS_12} RS sequent)
| chk_target _ = @{thm Gen_Synthesis_Rule_VS_11} RS sequent
in case X of Const (\<^const_name>‹REMAINS›, _) $ _ $ _ => NONE
| _ => SOME ((ctxt, chk_target Y), Seq.empty)
end)›
subsection ‹Procedure Application - General Methods›
φreasoner_group φsynthesis_gen_proc_cut = (1200, [1200, 1300]) in φsynthesis_gen_proc
‹cutting rules›
and φsynthesis_gen_proc_normalize = (2000, [2000, 2100])
in φsynthesis_gen_proc and > φsynthesis_gen_proc_cut
‹normalizing rules›
and φsynthesis_gen_proc_init = (10, [10, 10]) in φsynthesis_gen_proc and < φsynthesis_gen_proc_cut
‹initiating reasoning›
and φsynthesis_gen_by_overloading = (2500, [2500,2510]) in φsynthesis_gen_proc and > φsynthesis_gen_proc_normalize ‹›
lemma [φreason %φsynthesis_gen_proc_cut for ‹PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 _ ⦃ ?X v❟ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⟼ ?Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E )) _ _›]:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 (f ⤜ (λv. F (φV_pair v vs)))
⦃ Xr vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. (E1 e❟ ExBI Xr) + EF e)))
((𝗉𝗋𝗈𝖼 f ⦃ R ⟼ λret. X ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis) &&& PROP Ant)
Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X (φV_fst vs)❟ Xr (φV_snd vs) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 EF))
Ant Result ›
unfolding Gen_Synthesis_Rule_def conjunction_imp REMAINS_def
subgoal premises prems apply (rule prems(1))
❴ premises f and A
f
apply_rule prems(2)[OF A]
❵. .
lemma [φreason %φsynthesis_gen_proc_cut]:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀_::unit φarg. 𝗉𝗋𝗈𝖼 (f ⤜ F) ⦃ Xr 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. (E1 e❟ Xr) + EF e)))
(𝗉𝗋𝗈𝖼 f ⦃ R ⟼ λret. X ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis &&& PROP Ant)
Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 F v ⦃ X v❟ Xr 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 EF))
Ant Result ›
unfolding Gen_Synthesis_Rule_def conjunction_imp
subgoal premises prems apply (rule prems(1))
❴ premises f and A
f
apply_rule prems(2)[OF A]
❵ . .
lemma [φreason %φsynthesis_gen_proc_cut]:
‹ (⋀e. Remove_Values (E e) (E' e))
⟹ Simplify (assertion_simps ABNORMAL) E'' E'
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀_::unit φarg. 𝗉𝗋𝗈𝖼 F ⦃ Void 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant
(PROP Ant ⟹ 𝗉𝗋𝗈𝖼 F ⦃ R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E'' @tag synthesis) ›
unfolding Gen_Synthesis_Rule_def Remove_Values_def Simplify_def Action_Tag_def REMAINS_def
subgoal premises P
apply (unfold P(2))
using P(3)[OF P(4), THEN spec, THEN φCONSEQ'E[OF view_shift_by_implication, OF P(1)],
simplified] . .
lemma [φreason %φsynthesis_gen_proc_cut+10]:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 (f ⪢ F v) ⦃ Xr v 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. (E1 e❟ ExBI Xr) + EF e)))
(𝗉𝗋𝗈𝖼 f ⦃ R ⟼ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis &&& PROP Ant)
Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀v. 𝗉𝗋𝗈𝖼 F v ⦃ X❟ Xr v 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 EF))
Ant Result ›
unfolding Gen_Synthesis_Rule_def conjunction_imp
subgoal premises prems apply (rule prems(1))
❴ premises f and A
f
apply_rule prems(2)[OF A]
❵ . .
lemma [φreason %φsynthesis_gen_proc_normalize]:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ Rx vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ Void❟ Rx vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result›
unfolding Gen_Synthesis_Rule_def by simp
lemma [φreason %φsynthesis_gen_proc_normalize]:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs❟ Rx vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ (X vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Rx vs) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result›
unfolding Gen_Synthesis_Rule_def REMAINS_def by simp
lemma [φreason %φsynthesis_gen_proc_normalize]:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ A vs❟ B vs❟ Rx vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ (A vs❟ B vs)❟ Rx vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result›
unfolding Gen_Synthesis_Rule_def by (simp add: mult.assoc)
subsection ‹Entry Point›
context begin
private lemma Gen_Synthesis_Rule_start_proc:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs❟ Void 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E e❟ R)))
Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result›
unfolding Gen_Synthesis_Rule_def REMAINS_def
by (simp add: φframe)
private lemma Gen_Synthesis_Rule_start_proc_focus_the_last:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs❟ Void 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Yr ret❟ R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E e❟ R )))
Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs ⟼ λret. Y ret❟ Yr ret ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result›
unfolding Gen_Synthesis_Rule_def REMAINS_def
by (simp add: φframe mult.assoc[symmetric])
private lemma Gen_Synthesis_Rule_start_proc_having_target:
‹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs❟ Void 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ λret. Y ret❟ R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E e❟ R )))
Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant Result›
unfolding Gen_Synthesis_Rule_def REMAINS_def
by (simp add: φframe)
φreasoner_ML Gen_Synthesis_Rule_init_for_proc %φsynthesis_gen_proc_init
(‹PROP Gen_Synthesis_Rule (Trueprop (∀vs. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ ?Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E)) (PROP _) (PROP _)›)
= ‹fn (_, (ctxt,sequent)) => Seq.make (fn () =>
let fun dest_proc (Const (\<^const_name>‹Gen_Synthesis_Rule›, _) $ tm $ _ $ _) = dest_proc tm
| dest_proc (Const (\<^const_name>‹Trueprop›, _) $ tm) = dest_proc tm
| dest_proc (Const (\<^const_name>‹All›, _) $ tm) = dest_proc tm
| dest_proc (Abs (_,_,tm)) = dest_proc tm
| dest_proc tm = Phi_Syntax.dest_procedure tm
val (_,X,Y,_) = dest_proc (Thm.major_prem_of sequent)
fun chk_target (Abs (_,_,tm)) = chk_target tm
| chk_target (Const (\<^const_name>‹ExBI›, _) $ _)
= error ("Exisential quantification has not been supported in synthesis.")
| chk_target (Const (\<^const_name>‹Subjection›, _) $ _ $ _)
= Phi_Reasoner.bad_config "Subjection shouldn't occur here."
| chk_target (Const(\<^const_name>‹REMAINS›, _) $ _ $ _)
= @{thm Gen_Synthesis_Rule_start_proc_having_target}
| chk_target (Const (\<^const_name>‹times›, _) $ _ $ _)
= (warning "You have multiple separated items and it is unclear which one is \
\the target to be synthesised or the residue of the synthesis.\n\
\We assume the synthesis target is the last item.\n\
\You should use ‹ Residue ❟ ❬ Target ❭ › to annotate the target, \
\or ‹ ❬ Target ❭ › if there is no residue.";
@{thm Gen_Synthesis_Rule_start_proc_focus_the_last})
| chk_target _ = @{thm Gen_Synthesis_Rule_start_proc}
in case X
of Const (\<^const_name>‹REMAINS›, _) $ _ $ _ => NONE
| _ => SOME ((ctxt, (chk_target Y) RS sequent), Seq.empty)
end)›
end
lemma [φreason %φsynthesis_gen_proc_cut]:
‹ WARNING TEXT(‹Pure fact› P ‹will be discarded during the synthesis.›)
⟹ PROP Gen_Synthesis_Rule
(Trueprop (𝗉𝗋𝗈𝖼 F ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E)) Ant Result
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F ⦃ X ⟼ λv. Y v 𝗌𝗎𝖻𝗃 P v ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E)) Ant Result›
unfolding Gen_Synthesis_Rule_def
subgoal premises prems apply (rule prems(2))
❴ premises Ant
apply_rule prems(3)[OF Ant]
❵ . .
subsection ‹Tools›
lemma make_synthesis_rule:
‹ Simplify (assertion_simps ABNORMAL) E' (λe. E e❟ R)
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant
((⋀vs. X' vs 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 Any1 vs)
⟹ PROP Ant
⟹ ∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X' vs ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E'
@tag synthesis)›
unfolding Gen_Synthesis_Rule_def
❴ premises E[assertion_simps] and F and X and A
X
apply_rule F[OF A]
❵ .
lemma make_synthesis_rule':
‹ Simplify (assertion_simps ABNORMAL) E' (λe. E e❟ R')
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant
((⋀vs. X' vs 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R' 𝗐𝗂𝗍𝗁 Any1 vs)
⟹ PROP Ant
⟹ ∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X' vs ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R❟ R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E'
@tag synthesis)›
unfolding REMAINS_def
using make_synthesis_rule[unfolded REMAINS_def, where Y = ‹λv. Y v❟ R›, unfolded mult.assoc] .
subsection ‹Overloaded Synthesis›
consts overloaded_synthesis :: action
lemma synthesis_gen_mode_overloaded_I:
‹ synthesis_gen_mode A overloaded_synthesis ›
unfolding synthesis_gen_mode_def ..
subsubsection ‹Conventions›
declare [[φreason_default_pattern
‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret::_ φarg. ?x ⦂ ?Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag overloaded_synthesis›
⇒ ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret::_ φarg. ?x ⦂ ?Y' ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E' @tag overloaded_synthesis› (100)
and ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret::_ φarg. ?Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag overloaded_synthesis›
⇒ ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret::_ φarg. ?Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E' @tag overloaded_synthesis› (90)
and ‹(?A::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag overloaded_synthesis›
⇒ ‹(?A::assn) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag overloaded_synthesis› (100)
and ‹(?A::assn) 𝗌𝗁𝗂𝖿𝗍𝗌 ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag overloaded_synthesis›
⇒ ‹(?A::assn) 𝗌𝗁𝗂𝖿𝗍𝗌 ?X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag overloaded_synthesis› (100)
and ‹?X @tag overloaded_synthesis› ⇒ ‹ERROR TEXT(‹Bad form of overloaded synthesis› ?X)› (0),
generate_pattern_of_synthesis_rule
‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis &&& TERM ()›
⇒ ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis› (110)
and ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis &&& TERM ()›
⇒ ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Z ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis› (110)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis &&& TERM ()›
⇒ ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis› (120)
and ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis &&& TERM ()›
⇒ ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?x ⦂ _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 _ @tag overloaded_synthesis› (120)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag overloaded_synthesis &&& TERM ?Y'›
⇒ ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Y' ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E' @tag overloaded_synthesis› (110)
and ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag overloaded_synthesis &&& TERM ?Y'›
⇒ ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Y' ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E' @tag overloaded_synthesis› (110)
and ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag overloaded_synthesis &&& (TERM ?X' &&& TERM ?Y')›
⇒ ‹𝗉𝗋𝗈𝖼 _ ⦃ ?X' ⟼ λret. ?Y' ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E' @tag overloaded_synthesis› (110)
and ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag overloaded_synthesis &&& (TERM ?X' &&& TERM ?Y')›
⇒ ‹∀vs::?'a. 𝗉𝗋𝗈𝖼 _ ⦃ ?X' vs ⟼ λret. ?Y' ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E' @tag overloaded_synthesis› (110)
]]
φreasoner_group φoverloaded_synthesis_all = (100, [10, 3000]) for ‹𝗉𝗋𝗈𝖼 f ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag overloaded_synthesis›
‹Synthesizes an overloaded given operator›
and φoverloaded_synthesis = (100, [100,100]) in φoverloaded_synthesis_all
‹the default reasoner group›
and φoverloaded_synthesis_fallback = (10, [10,10]) in φoverloaded_synthesis_all
‹fallbacks›
consts synthesis_pattern1 :: ‹'ret::{} ⇒ 'any::{}›
consts synthesis_pattern2 :: ‹'arg::{} ⇒ 'ret::{} ⇒ 'any::{}›
subsubsection ‹Rules of Overloaded Synthesis›
lemma [φreason default %φoverloaded_synthesis_fallback]:
‹ (⋀vs. S1 vs❟ R 𝗌𝗁𝗂𝖿𝗍𝗌 YY vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 𝗐𝗂𝗍𝗁 Any @tag overloaded_synthesis)
⟹ ∀vs. 𝗉𝗋𝗈𝖼 Return vs ⦃ S1 vs❟ R ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ @tag overloaded_synthesis›
❴ premises I
I
❵ .
lemma [φreason default %φoverloaded_synthesis_fallback]:
‹ A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag overloaded_synthesis
⟹ A 𝗌𝗁𝗂𝖿𝗍𝗌 X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag overloaded_synthesis ›
unfolding Action_Tag_def
by (simp add: view_shift_by_implication)
lemma overloaded_synthesis_nullary:
‹ 𝗉𝗋𝗈𝖼 H ⦃ R1 ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag overloaded_synthesis
⟹ 𝗉𝗋𝗈𝖼 H ⦃ R1 ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis›
unfolding Action_Tag_def .
lemma overloaded_synthesis_unary:
‹ 𝗉𝗋𝗈𝖼 h1 ⦃ R1 ⟼ λret. S1 ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis
⟹ ∀vs. 𝗉𝗋𝗈𝖼 H vs ⦃ S1 vs❟ R2 ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 E @tag overloaded_synthesis
⟹ 𝗉𝗋𝗈𝖼 (h1 ⤜ H) ⦃ R1 ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (E1 + E) @tag synthesis›
❴ premises H1 and H
H1 H
❵ .
lemma overloaded_synthesis_binary:
‹ 𝗉𝗋𝗈𝖼 h1 ⦃ R1 ⟼ λret. S1 ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 h2 ⦃ R2 ⟼ λret. S2 ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 @tag synthesis
⟹ ∀vs. 𝗉𝗋𝗈𝖼 H vs ⦃ S1 (φV_fst vs)❟ S2 (φV_snd vs)❟ R3 ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R4 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 E @tag overloaded_synthesis
⟹ 𝗉𝗋𝗈𝖼 (h1 ⤜ (λv1. h2 ⤜ (λv2. H (φV_pair v1 v2))))
⦃ R1 ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R4 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E1 e + (E2 e❟ (∃*v. S1 v)) + E e) @tag synthesis›
❴ premises H1 and H2 and H
H1 H2 H
❵ .
lemma overloaded_synthesis_ternary:
‹ 𝗉𝗋𝗈𝖼 h1 ⦃ R1 ⟼ λret::VAL φarg. S1 ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E1 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 h2 ⦃ R2 ⟼ λret::VAL φarg. S2 ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R3 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 h3 ⦃ R3 ⟼ λret::VAL φarg. S3 ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R4 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E3 @tag synthesis
⟹ ∀vs. 𝗉𝗋𝗈𝖼 H vs ⦃ S1 (φV_fst vs)❟ S2 (φV_fst (φV_snd vs))❟ S3 (φV_snd (φV_snd vs))❟ R4
⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R5 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 E @tag overloaded_synthesis
⟹ 𝗉𝗋𝗈𝖼 (h1 ⤜ (λv1. h2 ⤜ (λv2. h3 ⤜ (λv3. H (φV_pair v1 (φV_pair v2 v3))))))
⦃ R1 ⟼ λret. YY ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R5 ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. E1 e + ((∃*v. S1 v)❟ E2 e) + ((∃*v. S1 v)❟ (∃*v. S2 v)❟ E3 e) + E e)
@tag synthesis›
❴ premises H1 and H2 and H3 and H
H1 H2 H3 H
❵ .
lemma make_overloaded_synthesis_rule:
‹ Simplify (assertion_simps ABNORMAL) E' (λe. E e❟ R)
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant
((⋀vs. X' vs 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 Any1 vs)
⟹ PROP Ant
⟹ ∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X' vs ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E'
@tag overloaded_synthesis)›
unfolding Gen_Synthesis_Rule_def
❴ premises E[assertion_simps] and F and X and A
X
apply_rule F[OF A]
❵ .
lemma make_overloaded_synthesis_rule':
‹ Simplify (assertion_simps ABNORMAL) E' (λe. E e❟ R')
⟹ PROP Gen_Synthesis_Rule
(Trueprop (∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X vs ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E))
Ant
((⋀vs. X' vs 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X vs 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R' 𝗐𝗂𝗍𝗁 Any1 vs)
⟹ PROP Ant
⟹ ∀vs. 𝗉𝗋𝗈𝖼 F vs ⦃ X' vs ⟼ λret. Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R❟ R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E'
@tag overloaded_synthesis)›
unfolding REMAINS_def
using make_overloaded_synthesis_rule[unfolded REMAINS_def, where Y = ‹λv. Y v❟ R›, unfolded mult.assoc] .
ML_file ‹library/additions/overloaded_synthesis.ML›
attribute_setup overloaded_operator_in_synthesis = ‹
let val signat = Scan.peek (fn ctxt =>
(( (\<^keyword>‹(› -- \<^keyword>‹)›) >> (K []) || Scan.repeat Parse.term)
--| (\<^keyword>‹=>› || \<^keyword>‹⇒›) -- Parse.term
>> (fn (A,Y) =>
let val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic (Context.proof_of ctxt)
val terms = map (Type.constraint \<^typ>‹_ φarg ⇒ assn› o Syntax.parse_term ctxt') (Y::A)
|> Syntax.check_terms ctxt'
val ctxt'' = fold Proof_Context.augment terms ctxt'
val (Y'::A') = Variable.export_terms ctxt'' ctxt' terms
in Phi_Synthesis.Signature (A',Y')
end))
|| (Parse.term >>
(Phi_Synthesis.Operator o Context.cases Syntax.read_term_global Syntax.read_term ctxt)))
in Phi_Reasoner.attr_syntax' signat
(fn (pos, mode, group, signat) =>
Thm.declaration_attribute (K (
Phi_Synthesis.declare_overloaded_operator signat pos
(mode, SOME (the_default @{reasoner_group %φoverloaded_synthesis} group)))))
end
›
‹Declare the given term will be parsed as an overloaded operator in generating synthesis rules›
section ‹Small Process - II›
subsection ‹Collect Return Values›
definition collect_return_values' :: ‹('vs::VALs φarg ⇒ assn) ⇒ 'vs::VALs φarg ⇒ assn›
where ‹collect_return_values' S vs = S vs›
abbreviation ‹collect_return_values S vs ≡ TAIL (collect_return_values' S vs)›
definition Collect_Return_Values :: ‹assn ⇒ ('vs::VALs φarg ⇒ assn) ⇒ 'vs::VALs φarg ⇒ bool›
where ‹Collect_Return_Values S S_out V_out ⟷ S = S_out V_out›
lemma Collect_Return_Values_I: ‹Collect_Return_Values (S V) S V›
unfolding Collect_Return_Values_def ..
φreasoner_ML Collect_Return_Values 1000 (‹Collect_Return_Values ?S ?var_S_out ?var_V_out›) = ‹
fn (_, (ctxt,sequent)) =>
let
val \<^const>‹Trueprop› $ (\<^Const_>‹Collect_Return_Values _› $ S $ Var S' $ Var V')
= Thm.major_prem_of sequent
val (V'',S'') = Procedure_Syntax.package_values0
"𝗏𝗌" (TVar (("ret", Thm.maxidx_of sequent),\<^sort>‹VALs›)) false NONE S
|> apply2 (Thm.cterm_of ctxt)
in Drule.infer_instantiate_types ctxt [(S',S''),(V',V'')] sequent
|> (fn th => @{thm Collect_Return_Values_I} RS th)
|> pair ctxt |> Seq.single
end
›
lemma [φreason 2550]:
‹ Collect_Return_Values X S vs
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 collect_return_values S vs›
unfolding Collect_Return_Values_def collect_return_values'_def TAIL_def
by simp
lemma [φreason 3200]:
‹ 0 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 collect_return_values 0 φV_none›
unfolding Collect_Return_Values_def collect_return_values'_def TAIL_def
by simp
subsection ‹Compilibility / Validity of Semantics›
definition ‹chk_semantics_validity x ⟷ True›
section ‹Finale›
hide_const synthesis_gen_mode
end