Theory PhiSem_Formalization_Tools
theory PhiSem_Formalization_Tools
imports IDE_CP
keywords ":=" :: quasi_command
begin
section ‹Tools for Formalizing Instructions›
named_theorems discharging_semantic_debt
‹Theorems that discharges or helps to discharge the debt axioms for semantic formalization.›
subsection ‹Elementary Constructions for Formalizing Instructions›
definition ‹semantic_literal = φarg›
notation (do_notation) semantic_literal ("𝗅𝗂𝗍𝖾𝗋𝖺𝗅")
ML ‹Synchronized.change Phi_Syntax.semantic_oprs (Symtab.update (\<^const_name>‹semantic_literal›, 0))›
definition φM_assert :: ‹bool ⇒ unit proc›
where ‹φM_assert P = (λs. if P then Return φV_none s else {Invalid})›
definition φM_assume :: ‹bool ⇒ unit proc›
where ‹φM_assume P = (λs. if P then Return φV_none s else {AssumptionBroken})›
definition φM_getV_raw :: ‹(VAL ⇒ 'v) ⇒ VAL φarg ⇒ ('v ⇒ 'y proc) ⇒ 'y proc›
where ‹φM_getV_raw VDT_dest v F = F (VDT_dest (φarg.dest v))›
definition φM_getV :: ‹TY ⇒ (VAL ⇒ 'v) ⇒ VAL φarg ⇒ ('v ⇒ 'y proc) ⇒ 'y proc›
where ‹φM_getV TY VDT_dest v F =
(φM_assert (φarg.dest v ∈ Well_Type TY) ⪢ F (VDT_dest (φarg.dest v)))›
definition φM_caseV :: ‹(VAL φarg ⇒ ('vr,'ret) proc') ⇒ (VAL × 'vr::FIX_ARITY_VALs,'ret) proc'›
where ‹φM_caseV F = (λarg. case arg of φarg (a1,a2) ⇒ F (φarg a1) (φarg a2))›
lemma Valid_Proc_φM_assert[intro!, φreason 1200]:
‹Valid_Proc (φM_assert P)›
unfolding Valid_Proc_def φM_assert_def Return_def det_lift_def
by clarsimp
lemma Valid_Proc_φM_assume[intro!, φreason 1200]:
‹Valid_Proc (φM_assume P)›
unfolding Valid_Proc_def φM_assume_def Return_def det_lift_def
by clarsimp
lemma Valid_Proc_φM_getV_raw[intro!, φreason 1200]:
‹ (⋀v. Valid_Proc (F v))
⟹ Valid_Proc (φM_getV_raw VDF v F)›
unfolding Valid_Proc_def φM_getV_raw_def
by blast
subsection ‹Basic Rules›
declare φSEQ[intro!]
lemma φM_assert[intro!]:
‹(Satisfiable X ⟹ P) ⟹ 𝗉𝗋𝗈𝖼 φM_assert P ⦃ X ⟼ λ_. X ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 Any›
unfolding φM_assert_def
by (rule φSatisfiable; simp; rule)
lemma semantic_assert_φapp:
‹ 𝗉𝖺𝗋𝖺𝗆 P
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 P
⟹ 𝗉𝗋𝗈𝖼 φM_assert P ⦃ X ⟼ λ_. X ⦄›
unfolding φM_assert_def Premise_def
by (simp; rule)
lemma φM_assert_True[simp]:
‹φM_assert True = Return φV_none›
unfolding φM_assert_def by simp
lemma φM_assert':
‹P ⟹ Q (F args) ⟹ Q ((φM_assert P ⪢ F) args)›
unfolding φM_assert_def bind_def Return_def det_lift_def by simp
lemma φM_assume[intro!]:
‹(P ⟹ 𝗉𝗋𝗈𝖼 F ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E) ⟹ 𝗉𝗋𝗈𝖼 (φM_assume P ⪢ F) ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E›
unfolding φProcedure_def φM_assume_def bind_def Return_def det_lift_def less_eq_BI_iff
by clarsimp
lemma φM_assume1[intro!]:
‹𝗉𝗋𝗈𝖼 (φM_assume P) ⦃ Void ⟼ Void 𝗌𝗎𝖻𝗃 P ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E›
unfolding φM_assume_def φProcedure_def bind_def Return_def det_lift_def less_eq_BI_iff
by clarsimp
lemma semantic_assumption_φapp:
‹ 𝗉𝖺𝗋𝖺𝗆 P
⟹ 𝗉𝗋𝗈𝖼 (φM_assume P) ⦃ Void ⟼ Void 𝗌𝗎𝖻𝗃 P ⦄ ›
using φM_assume1 .
lemma φM_tail_left: ‹𝗉𝗋𝗈𝖼 F ⦃ X❟ 1 ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ⟹ 𝗉𝗋𝗈𝖼 F ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E› by simp
lemma φM_tail_right: ‹𝗉𝗋𝗈𝖼 F ⦃ X ⟼ λv. Y v❟ 1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ⟹ 𝗉𝗋𝗈𝖼 F ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E› by simp
lemma φM_shrink_left: ‹𝗉𝗋𝗈𝖼 F ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ⟹ 𝗉𝗋𝗈𝖼 F ⦃ X❟ 1 ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E› by simp
lemma φM_shrink_right[intro!]: ‹𝗉𝗋𝗈𝖼 F ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ⟹ 𝗉𝗋𝗈𝖼 F ⦃ X ⟼ λv. Y v❟ 1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E› by simp
lemma φM_getV_raw[intro!]:
‹(v ⊨ (x ⦂ A) ⟹ 𝗉𝗋𝗈𝖼 F (VDT_dest v) ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E )
⟹ 𝗉𝗋𝗈𝖼 φM_getV_raw VDT_dest (φarg v) F ⦃ x ⦂ Val (φarg v) A❟ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
unfolding φM_getV_raw_def Premise_def
by (clarsimp simp add: Val.unfold norm_precond_conj)
declare φM_getV_raw[where X=1, simplified, intro!]
lemma φM_getV[intro!]:
‹(v ⊨ (x ⦂ A) ⟹ <φexpn> v ∈ Well_Type TY)
⟹ (v ⊨ (x ⦂ A) ⟹ 𝗉𝗋𝗈𝖼 F (VDT_dest v) ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E )
⟹ 𝗉𝗋𝗈𝖼 φM_getV TY VDT_dest (φarg v) F ⦃ x ⦂ Val (φarg v) A❟ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
unfolding φM_getV_def Premise_def
by (clarsimp simp add: Val.unfold norm_precond_conj)
declare φM_getV[where X=1, simplified, intro!]
lemma φM_caseV[intro!]:
‹ 𝗉𝗋𝗈𝖼 F va vb ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ 𝗉𝗋𝗈𝖼 φM_caseV F (φV_pair va vb) ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
unfolding φM_caseV_def φV_pair_def by simp
lemma "__Return_rule__":
‹ 𝗉𝗋𝗈𝖼 Return v ⦃ X v ⟼ X ⦄ ›
unfolding φProcedure_def det_lift_def Return_def less_eq_BI_iff
by clarsimp
lemma semantic_return_φapp:
‹ 𝗉𝖺𝗋𝖺𝗆 (v ⊨ (y ⦂ T))
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 v ⊨ (y ⦂ T)
⟹ 𝗉𝗋𝗈𝖼 Return (φarg v) ⦃ X ⟼ λu. y ⦂ Val u T❟ X ⦄ ›
unfolding Premise_def φProcedure_def det_lift_def Return_def less_eq_BI_iff
by (clarsimp simp add: Val.unfold)
lemma semantic_literal_φapp:
‹ 𝗉𝖺𝗋𝖺𝗆 (v ⊨ (y ⦂ T))
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 v ⊨ (y ⦂ T)
⟹ Void 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ Val (semantic_literal v) T ›
unfolding Premise_def Transformation_def semantic_literal_def
by clarsimp
lemma semantic_local_value_φapp:
‹ 𝗉𝖺𝗋𝖺𝗆 TY
⟹ Semantic_Type' (x ⦂ T) TY
⟹ 𝗉𝗋𝗈𝖼 φM_assert (φarg.dest v ∈ Well_Type TY) ⦃ x ⦂ 𝗏𝖺𝗅[v] T ⟼ λ_. Void 𝗌𝗎𝖻𝗃 φarg.dest v ⊨ (x ⦂ T) ⦄›
unfolding φM_assert_def Premise_def Semantic_Type'_def subset_iff φProcedure_def det_lift_def Return_def
by (clarsimp simp add: Val.unfold INTERP_SPEC less_eq_BI_iff)
lemma semantic_local_values_nochk_φapp:
‹ x ⦂ 𝗏𝖺𝗅𝗌[v] T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Void 𝗐𝗂𝗍𝗁 φarg.dest v ⊨ (x ⦂ T) ›
unfolding Transformation_def
by clarsimp
lemma semantic_local_value_nochk_φapp:
‹ x ⦂ 𝗏𝖺𝗅[v] T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 1 𝗐𝗂𝗍𝗁 φarg.dest v ⊨ (x ⦂ T) ›
unfolding Transformation_def
by clarsimp
subsection ‹Synthesis of Value›
subsubsection ‹Literal Value›
definition [φprogramming_simps]: ‹literal x ≡ x›
declare [[φreason_default_pattern
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ 𝗏𝖺𝗅[semantic_literal _] ?T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis› ⇒
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ 𝗏𝖺𝗅[semantic_literal _] ?T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis›
‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ 𝗏𝖺𝗅[semantic_literal _] _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis› (500) ]]
setup ‹Context.theory_map (
Phi_Reasoner.add_pass
(Const("Phi_Type_of_Literal.synthesisable_literals", dummyT),
\<^pattern_prop>‹?X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ 𝗏𝖺𝗅[semantic_literal _] ?T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ @tag synthesis›,
fn pos => fn (rules, prio, patterns, guard, ctxt) =>
let val T_names =
fold ((fn Const(\<^const_name>‹REMAINS›, _) $ (
Const(\<^const_name>‹φType›, _) $ _
$ (Const(\<^const_name>‹Val›, _) $ _ $ T)) $ _ =>
(case Term.head_of T
of Const(N, _) => insert (op =) N
| _ => I)
| _ => I)
o #2 o Phi_Syntax.dest_transformation o Thm.concl_of) rules []
in if null T_names then ()
else Synchronized.change Phi_Type_of_Literal.synthesisable_literals
(fold Symtab.insert_set T_names);
(rules, prio, patterns, guard, ctxt)
end
)
)›
lemma "_synthesis_literal_":
‹ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 const ⦂ 𝗏𝖺𝗅[semantic_literal v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R' @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 Return (semantic_literal v) ⦃ R ⟼ λret. const ⦂ 𝗏𝖺𝗅[ret] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R' ⦄ @tag synthesis›
unfolding Action_Tag_def Premise_def φProcedure_def det_lift_def Return_def semantic_literal_def Transformation_def
by (clarsimp simp add: Val.unfold INTERP_SPEC_subj less_eq_BI_iff INTERP_SPEC, blast)
lemmas [φreason %φsynthesis_literal] = "_synthesis_literal_"[where const=‹literal x› for x]
lemma [φreason %is_literal]:
‹ Is_Literal (literal x) ›
unfolding Is_Literal_def ..
subsubsection ‹Value Sequence›
lemma semantic_cons_lval_φapp:
‹ 𝗉𝗋𝗈𝖼 Return (φV_cons v⇩h v⇩L) ⦃ x⇩h ⦂ 𝗏𝖺𝗅[v⇩h] T❟ x⇩L ⦂ 𝗏𝖺𝗅𝗌[v⇩L] L ⟼ λret. (x⇩h, x⇩L) ⦂ 𝗏𝖺𝗅𝗌[ret] (List_Item T ∗ L) ⦄ ›
unfolding Premise_def φProcedure_def det_lift_def Return_def
by (cases v⇩h; cases v⇩L; clarsimp simp add: Val.unfold Vals.unfold times_list_def less_eq_BI_iff,
smt (verit, ccfv_threshold) append_Cons append_Nil list.inject)
lemma semantic_cons_lval⇩1_φapp:
‹ 𝗉𝗋𝗈𝖼 Return (φV_cons v φV_nil) ⦃ x ⦂ 𝗏𝖺𝗅[v] T ⟼ λret. x ⦂ 𝗏𝖺𝗅𝗌[ret] List_Item T ⦄ ›
unfolding Premise_def φProcedure_def det_lift_def Return_def
by (cases v; clarsimp simp add: Val.unfold Vals.unfold times_list_def less_eq_BI_iff)
proc (nodef) [φreason %φsynthesis_cut
for ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. (_, _) ⦂ 𝗏𝖺𝗅𝗌[ret] (List_Item _ ∗ _) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ ⦄ @tag synthesis›]:
requires C1: ‹𝗉𝗋𝗈𝖼 C⇩1 ⦃ R⇩0 ⟼ λret. x⇩h ⦂ 𝗏𝖺𝗅[ret] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩1 ⦄ @tag synthesis›
and C2: ‹𝗉𝗋𝗈𝖼 C⇩2 ⦃ R⇩1 ⟼ λret. x⇩L ⦂ 𝗏𝖺𝗅𝗌[ret] L 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩2 ⦄ @tag synthesis›
input ‹R⇩0›
output ‹λret. (x⇩h, x⇩L) ⦂ 𝗏𝖺𝗅𝗌[ret] (List_Item T ∗ L) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩2›
@tag synthesis
❴
C1 → val h ；
C2 $h semantic_cons_lval
❵ .
proc (nodef) [φreason %φsynthesis_cut
for ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. _ ⦂ 𝗏𝖺𝗅𝗌[ret] (List_Item _) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ ⦄ @tag synthesis›]:
requires C: ‹𝗉𝗋𝗈𝖼 C ⦃ R⇩0 ⟼ λret. x⇩h ⦂ 𝗏𝖺𝗅[ret] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩1 ⦄ @tag synthesis›
input ‹R⇩0›
output ‹λret. x⇩h ⦂ 𝗏𝖺𝗅𝗌[ret] List_Item T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩1›
@tag synthesis
❴
C semantic_cons_lval⇩1
❵ .
lemma [φreason %φsynthesis_cut
for ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. () ⦂ 𝗏𝖺𝗅𝗌[ret] ○ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ ⦄ @tag synthesis›]:
‹ 𝗉𝗋𝗈𝖼 Return φV_nil ⦃ R⇩0 ⟼ λret. () ⦂ 𝗏𝖺𝗅𝗌[ret] ○ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R⇩0 ⦄ ›
unfolding Premise_def φProcedure_def det_lift_def Return_def REMAINS_def
by (clarsimp simp add: Val.unfold Vals.unfold times_list_def less_eq_BI_iff)
subsection ‹Drop & Duplicate Value›
lemma [φreason 1200 for ‹?x ⦂ Val ?raw ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Y 𝗐𝗂𝗍𝗁 ?P @tag action_dup›]:
‹x ⦂ Val raw T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ Val raw T ❟ x ⦂ Val raw T @tag action_dup›
unfolding Transformation_def Action_Tag_def
by (clarsimp simp add: Val.unfold INTERP_SPEC less_eq_BI_iff)
lemma [φreason 1200 for ‹?x ⦂ Val ?raw ?T❟ ?R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?Y 𝗐𝗂𝗍𝗁 ?P @tag action_drop›]:
‹x ⦂ Val raw T❟ Void 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Void @tag action_drop›
unfolding Transformation_def Action_Tag_def
by (clarsimp simp add: Val.unfold)
subsection ‹Abnormal›
definition throw :: ‹ABNM ⇒ 'ret proc›
where ‹throw raw = det_lift (Abnormal raw)›
lemma throw_reduce_tail[procedure_simps,simp]:
‹(throw any ⪢ f) = throw any›
unfolding throw_def bind_def det_lift_def by simp
lemma "__throw_rule__"[intro!]:
‹ (⋀a. X a 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X' a)
⟹ 𝗉𝗋𝗈𝖼 (throw excep :: 'ret proc) ⦃ X excep ⟼ Any ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 X'›
unfolding φProcedure_def subset_iff det_lift_def throw_def Transformation_def
by (clarsimp simp add: INTERP_SPEC less_eq_BI_iff; metis)
lemma throw_φapp:
‹ 𝗉𝖺𝗋𝖺𝗆 excep
⟹ lambda_abstraction excep XX X
⟹ (⋀v. Remove_Values (X v) (X' v))
⟹ 𝗉𝗋𝗈𝖼 throw excep ⦃ XX ⟼ 0 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 X' ›
unfolding φProcedure_def subset_iff det_lift_def throw_def Remove_Values_def Transformation_def
lambda_abstraction_def
by (clarsimp simp add: INTERP_SPEC less_eq_BI_iff, metis)
definition op_try :: "'ret proc ⇒ (ABNM ⇒ 'ret proc) ⇒ 'ret proc"
where ‹op_try f g s = ⋃((λy. case y of Success x s' ⇒ {Success x s'}
| Abnormal v s' ⇒ g v s'
| AssumptionBroken ⇒ {AssumptionBroken}
| NonTerm ⇒ {NonTerm}
| Invalid ⇒ {Invalid}) ` f s)›
lemma "__op_try__"[intro!]:
‹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ Y1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λv. E v)
⟹ (⋀v. 𝗉𝗋𝗈𝖼 g v ⦃ E v ⟼ Y2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 )
⟹ 𝗉𝗋𝗈𝖼 op_try f g ⦃ X ⟼ λv. Y1 v + Y2 v ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 ›
unfolding op_try_def φProcedure_def less_eq_BI_iff
apply clarsimp subgoal for comp R x s
apply (cases s; simp; cases x; clarsimp simp add: INTERP_SPEC set_mult_expn ring_distribs)
subgoal premises prems for a b u v
using prems(1)[THEN spec[where x=comp], THEN spec[where x=R]]
by (metis (no_types, lifting) INTERP_SPEC LooseState_expn(1) prems(3) prems(6) prems(7) prems(8) prems(9) sep_conj_expn)
subgoal premises prems for a b c d u v2 proof -
have ‹Abnormal a b ⊨ LooseState (λv. INTERP_SPEC (Y1 v❟ R)) (λv. INTERP_SPEC (E v❟ R))›
using prems(1)[THEN spec[where x=comp], THEN spec[where x=R]]
using prems(10) prems(3) prems(7) prems(8) prems(9) by blast
note this[simplified]
then have ‹Success c d ⊨ LooseState (λv. INTERP_SPEC (Y2 v❟ R)) (λv. INTERP_SPEC (E2 v❟ R))›
using prems(2)[of a, THEN spec[where x=b], THEN spec[where x=R]]
by (meson INTERP_SPEC prems(4) sep_conj_expn)
note this[simplified]
then show ?thesis
by (metis INTERP_SPEC prems(11) sep_conj_expn)
qed
subgoal premises prems for a b c d u v proof -
have ‹Abnormal a b ⊨ LooseState (λv. INTERP_SPEC (Y1 v❟ R)) (λv. INTERP_SPEC (E v❟ R))›
using prems(1)[THEN spec[where x=comp], THEN spec[where x=R]]
using prems(10) prems(3) prems(7) prems(8) prems(9) by blast
note this[simplified]
then have ‹Abnormal c d ⊨ LooseState (λv. INTERP_SPEC (Y2 v❟ R)) (λv. INTERP_SPEC (E2 v❟ R))›
using prems(2)[THEN spec[where x=b], THEN spec[where x=R]]
by (meson INTERP_SPEC prems(4) sep_conj_expn)
note this[simplified]
then show ?thesis
by (simp add: INTERP_SPEC set_mult_expn)
qed
apply (smt (z3) INTERP_SPEC LooseState_expn(2) LooseState_expn(3) sep_conj_expn)
by blast .
definition "Union_the_Same_Or_Arbitrary_when_Var Z X Y ⟷ (∀v. (Z::'v ⇒ 'a BI) v = X v + Y v)"
lemma Union_the_Same_Or_Arbitrary_when_Var__the_Same:
‹Union_the_Same_Or_Arbitrary_when_Var Z Z Z›
unfolding Union_the_Same_Or_Arbitrary_when_Var_def by simp
lemma Union_the_Same_Or_Arbitrary_when_Var__Arbitrary:
‹Union_the_Same_Or_Arbitrary_when_Var (λv. X v + Y v) X Y›
unfolding Union_the_Same_Or_Arbitrary_when_Var_def by blast
φreasoner_ML Union_the_Same_Or_Arbitrary_when_Var 1200 (‹Union_the_Same_Or_Arbitrary_when_Var ?Z ?X ?Y›) = ‹
fn (_, (ctxt,sequent)) =>
let
val \<^const>‹Trueprop› $ (Const (\<^const_name>‹Union_the_Same_Or_Arbitrary_when_Var›, _)
$ Z $ _ $ _) = Thm.major_prem_of sequent
in (ctxt,
(if is_Var (Term.head_of (Envir.beta_eta_contract Z))
then @{thm Union_the_Same_Or_Arbitrary_when_Var__Arbitrary}
else @{thm Union_the_Same_Or_Arbitrary_when_Var__the_Same})
RS sequent) |> Seq.single
end
›
proc (nodef) try'':
assumes F: ‹𝗉𝗋𝗈𝖼 f ⦃ X ⟼ YY ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
assumes G: ‹(⋀v. 𝗉𝗋𝗈𝖼 g v ⦃ E v ⟼ YY ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 EE2 )›
input X
output YY
throws EE2
❴ apply_rule "__op_try__"
F
G
❵ .
proc (nodef) try':
assumes A: ‹Union_the_Same_Or_Arbitrary_when_Var Z Y1 Y2›
assumes F: ‹𝗉𝗋𝗈𝖼 f ⦃ X ⟼ Y1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
assumes G: ‹⋀v. 𝗉𝗋𝗈𝖼 g v ⦃ E v ⟼ Y2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E2 ›
input X
output Z
throws E2
❴ apply_rule "__op_try__" F G
unfold A[unfolded Union_the_Same_Or_Arbitrary_when_Var_def, THEN spec, symmetric]
❵.
end