--- a/Nominal/Ex/Lambda.thy Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Ex/Lambda.thy Tue Mar 22 12:18:30 2016 +0000
@@ -72,23 +72,6 @@
unfolding Ident_def
by simp
-thm lam.strong_induct
-
-lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"
- unfolding alpha_lam_raw_def
- by perm_simp rule
-
-lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"
-proof -
- have "alpha_lam_raw (rep_lam (abs_lam t)) t"
- using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis
- then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"
- unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .
- then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"
- using Quotient3_rel Quotient3_lam by metis
- thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
-qed
-
section {* Simple examples from Norrish 2004 *}
--- a/Nominal/Ex/Pi.thy Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Ex/Pi.thy Tue Mar 22 12:18:30 2016 +0000
@@ -1,571 +1,555 @@
-(* Theory be Kirstin Peters *)
-
-theory Pi
- imports "../Nominal2"
-begin
-
-atom_decl name
-
-subsection {* Capture-Avoiding Substitution of Names *}
-
-definition
- subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110)
-where
- "a[b:::=c] \<equiv> if (a = b) then c else a"
-
-declare subst_name_def[simp]
-
-lemma subst_name_mix_eqvt[eqvt]:
- fixes p :: perm
- and a :: name
- and b :: name
- and c :: name
-
- shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]"
-proof -
- show ?thesis
- by(auto)
-qed
-
-nominal_function
- subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
-where
- "subst_name_list a [] = a"
-| "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"
- apply(simp add: eqvt_def subst_name_list_graph_aux_def)
- apply(simp)
- apply(auto)
- apply(rule_tac y="b" in list.exhaust)
- by(auto)
-
-nominal_termination (eqvt)
- by (lexicographic_order)
-
-
-section {* The Synchronous Pi-Calculus *}
-
-subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *}
-
-nominal_datatype
- guardedTerm_mix = Output name name piMix ("_!<_>\<onesuperior>._" [120, 120, 110] 110)
- | Input name b::name P::piMix binds b in P ("_?<_>\<onesuperior>._" [120, 120, 110] 110)
- | Tau piMix ("<\<tau>\<onesuperior>>._" [110] 110)
- and sumList_mix = SumNil ("\<zero>\<onesuperior>")
- | AddSummand guardedTerm_mix sumList_mix (infixr "\<oplus>\<onesuperior>" 65)
- and piMix = Res a::name P::piMix binds a in P ("<\<nu>_>\<onesuperior>_" [100, 100] 100)
- | Par piMix piMix (infixr "\<parallel>\<onesuperior>" 85)
- | Match name name piMix ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110)
- | Sum sumList_mix ("\<oplus>\<onesuperior>{_}" 90)
- | Rep name b::name P::piMix binds b in P ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110)
- | Succ ("succ\<onesuperior>")
-
-lemmas piMix_strong_induct = guardedTerm_mix_sumList_mix_piMix.strong_induct
-lemmas piMix_fresh = guardedTerm_mix_sumList_mix_piMix.fresh
-lemmas piMix_eq_iff = guardedTerm_mix_sumList_mix_piMix.eq_iff
-lemmas piMix_distinct = guardedTerm_mix_sumList_mix_piMix.distinct
-lemmas piMix_size = guardedTerm_mix_sumList_mix_piMix.size
-
-subsection {* Alpha-Conversion Lemmata *}
-
-lemma alphaRes_mix:
- fixes a :: name
- and P :: piMix
- and z :: name
-
- assumes "atom z \<sharp> P"
-
- shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)"
-proof(cases "a = z")
- assume "a = z"
- thus ?thesis
- by(simp)
-next
- assume "a \<noteq> z"
- thus ?thesis
- using assms
- by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
-qed
-
-lemma alphaInput_mix:
- fixes a :: name
- and b :: name
- and P :: piMix
- and z :: name
-
- assumes "atom z \<sharp> P"
-
- shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
-proof(cases "b = z")
- assume "b = z"
- thus ?thesis
- by(simp)
-next
- assume "b \<noteq> z"
- thus ?thesis
- using assms
- by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
-qed
-
-lemma alphaRep_mix:
- fixes a :: name
- and b :: name
- and P :: piMix
- and z :: name
-
- assumes "atom z \<sharp> P"
-
- shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
-proof(cases "b = z")
- assume "b = z"
- thus ?thesis
- by(simp)
-next
- assume "b \<noteq> z"
- thus ?thesis
- using assms
- by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
-qed
-
-subsection {* Capture-Avoiding Substitution of Names *}
-
-lemma testl:
- assumes a: "\<exists>y. f = Inl y"
- shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
-using a by auto
-
-lemma testrr:
- assumes a: "\<exists>y. f = Inr (Inr y)"
- shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
-using a by auto
-
-lemma testlr:
- assumes a: "\<exists>y. f = Inr (Inl y)"
- shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
-using a by auto
-
-nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
- subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
- subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
- subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
-where
- "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])"
-| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
-| "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])"
-| "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>"
-| "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])"
-| "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])"
-| "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"
-| "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"
-| "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"
-| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
-| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
- using [[simproc del: alpha_lst]]
- apply(auto simp add: piMix_distinct piMix_eq_iff)
- apply(simp add: eqvt_def subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
- --"Covered all cases"
- apply(case_tac x)
- apply(simp)
- apply(case_tac a)
- apply(simp)
- apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1))
- apply(blast)
- apply(auto simp add: fresh_star_def)[1]
- apply(blast)
- apply(simp)
- apply(case_tac b)
- apply(simp)
- apply(case_tac a)
- apply(simp)
- apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2))
- apply(blast)
- apply(blast)
- apply(simp)
- apply(case_tac ba)
- apply(simp)
- apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))
- using [[simproc del: alpha_lst]]
- apply(auto simp add: fresh_star_def)[1]
- apply(blast)
- apply(blast)
- apply(blast)
- using [[simproc del: alpha_lst]]
- apply(auto simp add: fresh_star_def)[1]
- apply(simp)
- --"compatibility"
- apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
- apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
- apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
- apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
- prefer 2
- apply (simp only: eqvt_at_def subs_mix_def)
- apply rule
- apply(simp (no_asm))
- apply (subst testrr)
- apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
- apply (simp add: THE_default_def)
-apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
-apply simp_all[2]
-apply auto[1]
-apply (erule_tac x="x" in allE)
-apply simp
-apply (thin_tac "\<forall>p\<Colon>perm.
- p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
- (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
- then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
- else Inr (Inr undefined))")
-apply (thin_tac "\<forall>p\<Colon>perm.
- p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
- then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
- else Inr (Inr undefined)) =
- (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
- then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
- else Inr (Inr undefined))")
-apply (thin_tac "atom b \<sharp> (xa, ya)")
-apply (thin_tac "atom ba \<sharp> (xa, ya)")
-apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
-apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-apply assumption
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
- (Sum_Type.projr
- (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="Sum_Type.projr
- (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
- Sum_Type.projr
- (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
- (Sum_Type.projr
-(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
- (Sum_Type.projr
- (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
- (Sum_Type.projr
- (subsGuard_mix_subsList_mix_subs_mix_sum
- (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="succ\<onesuperior>" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply simp
-(* Here the only real goal compatibility is left *)
- apply (erule Abs_lst1_fcb)
- apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
- apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
- apply simp
- apply (erule fresh_eqvt_at)
- apply(simp add: finite_supp)
- apply(simp)
- apply(simp add: eqvt_at_def)
- apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
- apply(simp)
- apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
- apply(rename_tac b P ba xa ya Pa)
- apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
- apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
- apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
- prefer 2
- apply (simp only: eqvt_at_def subs_mix_def)
- apply rule
- apply(simp (no_asm))
- apply (subst testrr)
- apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
- apply (simp add: THE_default_def)
-apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
-apply simp_all[2]
-apply auto[1]
-apply (erule_tac x="x" in allE)
-apply simp
-apply (thin_tac "\<forall>p\<Colon>perm.
- p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
- (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
- then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
- else Inr (Inr undefined))")
-apply (thin_tac "\<forall>p\<Colon>perm.
- p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
- then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
- else Inr (Inr undefined)) =
- (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
- then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
- subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
- else Inr (Inr undefined))")
-apply (thin_tac "atom b \<sharp> (xa, ya)")
-apply (thin_tac "atom ba \<sharp> (xa, ya)")
-apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
-apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-apply assumption
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
- (Sum_Type.projr
- (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="Sum_Type.projr
- (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
- Sum_Type.projr
- (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
- (Sum_Type.projr
-(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
- (Sum_Type.projr
- (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
- (Sum_Type.projr
- (subsGuard_mix_subsList_mix_subs_mix_sum
- (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="succ\<onesuperior>" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply simp
-(* Here the only real goal compatibility is left *)
- apply (erule Abs_lst1_fcb)
- apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
- apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
- apply simp
- apply (erule fresh_eqvt_at)
- apply(simp add: finite_supp)
- apply(simp)
- apply(simp add: eqvt_at_def)
- apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
- apply(simp)
- done
-
-nominal_termination (eqvt)
- by (lexicographic_order)
-
-lemma forget_mix:
- fixes g :: guardedTerm_mix
- and xg :: sumList_mix
- and P :: piMix
- and x :: name
- and y :: name
-
- shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
- and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
- and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
-proof -
- show "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
- and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
- and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
- using assms
- apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
- by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)
-qed
-
-lemma fresh_fact_mix:
- fixes g :: guardedTerm_mix
- and xg :: sumList_mix
- and P :: piMix
- and x :: name
- and y :: name
- and z :: name
-
- assumes "atom z \<sharp> y"
-
- shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
- and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
- and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
-proof -
- show "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
- and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
- and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
- using assms
- apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct)
- by(auto simp add: piMix_fresh fresh_at_base)
-qed
-
-lemma substitution_lemma_mix:
- fixes g :: guardedTerm_mix
- and xg :: sumList_mix
- and P :: piMix
- and s :: name
- and u :: name
- and x :: name
- and y :: name
-
- assumes "x \<noteq> y"
- and "atom x \<sharp> u"
-
- shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
- and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
- and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
-proof -
- show "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
- and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
- and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
- using assms
- apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct)
- apply(simp_all add: fresh_fact_mix forget_mix)
- by(auto simp add: fresh_at_base)
-qed
-
-lemma perm_eq_subst_mix:
- fixes g :: guardedTerm_mix
- and xg :: sumList_mix
- and P :: piMix
- and x :: name
- and y :: name
-
- shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
- and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
- and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
-proof -
- show "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
- and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
- and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
- apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
- by(auto simp add: piMix_fresh fresh_at_base)
-qed
-
-lemma subst_id_mix:
- fixes g :: guardedTerm_mix
- and xg :: sumList_mix
- and P :: piMix
- and x :: name
-
- shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
-proof -
- show "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
- apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct)
- by(auto)
-qed
-
-lemma alphaRes_subst_mix:
- fixes a :: name
- and P :: piMix
- and z :: name
-
- assumes "atom z \<sharp> P"
-
- shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])"
-proof(cases "a = z")
- assume "a = z"
- thus ?thesis
- by(simp add: subst_id_mix)
-next
- assume "a \<noteq> z"
- thus ?thesis
- using assms
- by(simp add: alphaRes_mix perm_eq_subst_mix)
-qed
-
-lemma alphaInput_subst_mix:
- fixes a :: name
- and b :: name
- and P :: piMix
- and z :: name
-
- assumes "atom z \<sharp> P"
-
- shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
-proof(cases "b = z")
- assume "b = z"
- thus ?thesis
- by(simp add: subst_id_mix)
-next
- assume "b \<noteq> z"
- thus ?thesis
- using assms
- by(simp add: alphaInput_mix perm_eq_subst_mix)
-qed
-
-lemma alphaRep_subst_mix:
- fixes a :: name
- and b :: name
- and P :: piMix
- and z :: name
-
- assumes "atom z \<sharp> P"
-
- shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
-proof(cases "b = z")
- assume "b = z"
- thus ?thesis
- by(simp add: subst_id_mix)
-next
- assume "b \<noteq> z"
- thus ?thesis
- using assms
- by(simp add: alphaRep_mix perm_eq_subst_mix)
-qed
-
-inductive
- fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool"
-where
- "fresh_list_guard_mix [] g"
-| "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g"
-
-equivariance fresh_list_guard_mix
-nominal_inductive fresh_list_guard_mix
- done
-
-inductive
- fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool"
-where
- "fresh_list_sumList_mix [] xg"
-| "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg"
-
-equivariance fresh_list_sumList_mix
-nominal_inductive fresh_list_sumList_mix
- done
-
-inductive
- fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool"
-where
- "fresh_list_mix [] P"
-| "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P"
-
-equivariance fresh_list_mix
-nominal_inductive fresh_list_mix
- done
-
+(* Theory be Kirstin Peters *)
+
+theory Pi
+ imports "../Nominal2"
+begin
+
+atom_decl name
+
+subsection {* Capture-Avoiding Substitution of Names *}
+
+definition
+ subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110)
+where
+ "a[b:::=c] \<equiv> if (a = b) then c else a"
+
+declare subst_name_def[simp]
+
+lemma subst_name_mix_eqvt[eqvt]:
+ fixes p :: perm
+ and a :: name
+ and b :: name
+ and c :: name
+
+ shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]"
+proof -
+ show ?thesis
+ by(auto)
+qed
+
+nominal_function
+ subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
+where
+ "subst_name_list a [] = a"
+| "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"
+ apply(simp add: eqvt_def subst_name_list_graph_aux_def)
+ apply(simp)
+ apply(auto)
+ apply(rule_tac y="b" in list.exhaust)
+ by(auto)
+
+nominal_termination (eqvt)
+ by (lexicographic_order)
+
+
+section {* The Synchronous Pi-Calculus *}
+
+subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *}
+
+nominal_datatype
+ guardedTerm_mix = Output name name piMix ("_!<_>\<onesuperior>._" [120, 120, 110] 110)
+ | Input name b::name P::piMix binds b in P ("_?<_>\<onesuperior>._" [120, 120, 110] 110)
+ | Tau piMix ("<\<tau>\<onesuperior>>._" [110] 110)
+ and sumList_mix = SumNil ("\<zero>\<onesuperior>")
+ | AddSummand guardedTerm_mix sumList_mix (infixr "\<oplus>\<onesuperior>" 65)
+ and piMix = Res a::name P::piMix binds a in P ("<\<nu>_>\<onesuperior>_" [100, 100] 100)
+ | Par piMix piMix (infixr "\<parallel>\<onesuperior>" 85)
+ | Match name name piMix ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110)
+ | Sum sumList_mix ("\<oplus>\<onesuperior>{_}" 90)
+ | Rep name b::name P::piMix binds b in P ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110)
+ | Succ ("succ\<onesuperior>")
+
+lemmas piMix_strong_induct = guardedTerm_mix_sumList_mix_piMix.strong_induct
+lemmas piMix_fresh = guardedTerm_mix_sumList_mix_piMix.fresh
+lemmas piMix_eq_iff = guardedTerm_mix_sumList_mix_piMix.eq_iff
+lemmas piMix_distinct = guardedTerm_mix_sumList_mix_piMix.distinct
+lemmas piMix_size = guardedTerm_mix_sumList_mix_piMix.size
+
+subsection {* Alpha-Conversion Lemmata *}
+
+lemma alphaRes_mix:
+ fixes a :: name
+ and P :: piMix
+ and z :: name
+
+ assumes "atom z \<sharp> P"
+
+ shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)"
+proof(cases "a = z")
+ assume "a = z"
+ thus ?thesis
+ by(simp)
+next
+ assume "a \<noteq> z"
+ thus ?thesis
+ using assms
+ by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+qed
+
+lemma alphaInput_mix:
+ fixes a :: name
+ and b :: name
+ and P :: piMix
+ and z :: name
+
+ assumes "atom z \<sharp> P"
+
+ shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
+proof(cases "b = z")
+ assume "b = z"
+ thus ?thesis
+ by(simp)
+next
+ assume "b \<noteq> z"
+ thus ?thesis
+ using assms
+ by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+qed
+
+lemma alphaRep_mix:
+ fixes a :: name
+ and b :: name
+ and P :: piMix
+ and z :: name
+
+ assumes "atom z \<sharp> P"
+
+ shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
+proof(cases "b = z")
+ assume "b = z"
+ thus ?thesis
+ by(simp)
+next
+ assume "b \<noteq> z"
+ thus ?thesis
+ using assms
+ by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+qed
+
+subsection {* Capture-Avoiding Substitution of Names *}
+
+lemma testl:
+ assumes a: "\<exists>y. f = Inl y"
+ shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
+using a by auto
+
+lemma testrr:
+ assumes a: "\<exists>y. f = Inr (Inr y)"
+ shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
+using a by auto
+
+lemma testlr:
+ assumes a: "\<exists>y. f = Inr (Inl y)"
+ shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
+using a by auto
+
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+ subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
+ subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
+ subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
+where
+ "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])"
+| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
+| "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])"
+| "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>"
+| "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])"
+| "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])"
+| "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"
+| "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"
+| "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"
+| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
+| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
+ using [[simproc del: alpha_lst]]
+ apply(auto simp add: piMix_distinct piMix_eq_iff)
+ apply(simp add: eqvt_def subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
+ --"Covered all cases"
+ apply(case_tac x)
+ apply(simp)
+ apply(case_tac a)
+ apply(simp)
+ apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1))
+ apply(blast)
+ apply(auto simp add: fresh_star_def)[1]
+ apply(blast)
+ apply(simp)
+ apply(case_tac b)
+ apply(simp)
+ apply(case_tac a)
+ apply(simp)
+ apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2))
+ apply(blast)
+ apply(blast)
+ apply(simp)
+ apply(case_tac ba)
+ apply(simp)
+ apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))
+ using [[simproc del: alpha_lst]]
+ apply(auto simp add: fresh_star_def)[1]
+ apply(blast)
+ apply(blast)
+ apply(blast)
+ using [[simproc del: alpha_lst]]
+ apply(auto simp add: fresh_star_def)[1]
+ apply(simp)
+ --"compatibility"
+ apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+ apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
+ apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
+ apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
+ prefer 2
+ apply (simp only: eqvt_at_def subs_mix_def)
+ apply rule
+ apply(simp (no_asm))
+ apply (subst testrr)
+ apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
+ apply (simp add: THE_default_def)
+apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
+apply simp_all[2]
+apply auto[1]
+apply (erule_tac x="x" in allE)
+apply simp
+apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
+ (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+ then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+ else Inr (Inr undefined))")
+apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+ then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+ else Inr (Inr undefined)) =
+ (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+ then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+ else Inr (Inr undefined))")
+apply (thin_tac "atom b \<sharp> (xa, ya)")
+apply (thin_tac "atom ba \<sharp> (xa, ya)")
+apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
+apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
+apply assumption
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+ (Sum_Type.projr
+ (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+ Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+ (Sum_Type.projr
+(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+ (Sum_Type.projr
+ (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+ (Sum_Type.projr
+ (subsGuard_mix_subsList_mix_subs_mix_sum
+ (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="succ\<onesuperior>" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply simp
+(* Here the only real goal compatibility is left *)
+ apply (erule Abs_lst1_fcb)
+ apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
+ apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
+ apply simp
+ apply (erule fresh_eqvt_at)
+ apply(simp add: finite_supp)
+ apply(simp)
+ apply(simp add: eqvt_at_def)
+ apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
+ apply(simp)
+ apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+ apply(rename_tac b P ba xa ya Pa)
+ apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
+ apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
+ apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
+ prefer 2
+ apply (simp only: eqvt_at_def subs_mix_def)
+ apply rule
+ apply(simp (no_asm))
+ apply (subst testrr)
+ apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
+ apply (simp add: THE_default_def)
+apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
+apply simp_all[2]
+apply auto[1]
+apply (erule_tac x="x" in allE)
+apply simp
+apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
+ (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+ then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+ else Inr (Inr undefined))")
+apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+ then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+ else Inr (Inr undefined)) =
+ (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+ then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+ else Inr (Inr undefined))")
+apply (thin_tac "atom b \<sharp> (xa, ya)")
+apply (thin_tac "atom ba \<sharp> (xa, ya)")
+apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
+apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
+apply assumption
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+ (Sum_Type.projr
+ (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+ Sum_Type.projr
+ (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+ (Sum_Type.projr
+(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+ (Sum_Type.projr
+ (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+ (Sum_Type.projr
+ (subsGuard_mix_subsList_mix_subs_mix_sum
+ (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="succ\<onesuperior>" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply simp
+(* Here the only real goal compatibility is left *)
+ apply (erule Abs_lst1_fcb)
+ apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
+ apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
+ apply simp
+ apply (erule fresh_eqvt_at)
+ apply(simp add: finite_supp)
+ apply(simp)
+ apply(simp add: eqvt_at_def)
+ apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
+ apply(simp)
+ done
+
+nominal_termination (eqvt)
+ by (lexicographic_order)
+
+lemma forget_mix:
+ fixes g :: guardedTerm_mix
+ and xg :: sumList_mix
+ and P :: piMix
+ and x :: name
+ and y :: name
+
+ shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
+ and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
+ and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
+proof -
+ show "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
+ and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
+ and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
+ using assms
+ apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
+ by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)
+qed
+
+lemma fresh_fact_mix:
+ fixes g :: guardedTerm_mix
+ and xg :: sumList_mix
+ and P :: piMix
+ and x :: name
+ and y :: name
+ and z :: name
+
+ assumes "atom z \<sharp> y"
+
+ shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
+ and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
+ and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
+proof -
+ show "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
+ and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
+ and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
+ using assms
+ apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct)
+ by(auto simp add: piMix_fresh fresh_at_base)
+qed
+
+lemma substitution_lemma_mix:
+ fixes g :: guardedTerm_mix
+ and xg :: sumList_mix
+ and P :: piMix
+ and s :: name
+ and u :: name
+ and x :: name
+ and y :: name
+
+ assumes "x \<noteq> y"
+ and "atom x \<sharp> u"
+
+ shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
+ and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
+ and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
+proof -
+ show "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
+ and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
+ and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
+ using assms
+ apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct)
+ apply(simp_all add: fresh_fact_mix forget_mix)
+ by(auto simp add: fresh_at_base)
+qed
+
+lemma perm_eq_subst_mix:
+ fixes g :: guardedTerm_mix
+ and xg :: sumList_mix
+ and P :: piMix
+ and x :: name
+ and y :: name
+
+ shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
+ and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
+ and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
+proof -
+ show "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
+ and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
+ and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
+ apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
+ by(auto simp add: piMix_fresh fresh_at_base)
+qed
+
+lemma subst_id_mix:
+ fixes g :: guardedTerm_mix
+ and xg :: sumList_mix
+ and P :: piMix
+ and x :: name
+
+ shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
+proof -
+ show "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
+ apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct)
+ by(auto)
+qed
+
+lemma alphaRes_subst_mix:
+ fixes a :: name
+ and P :: piMix
+ and z :: name
+
+ assumes "atom z \<sharp> P"
+
+ shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])"
+proof(cases "a = z")
+ assume "a = z"
+ thus ?thesis
+ by(simp add: subst_id_mix)
+next
+ assume "a \<noteq> z"
+ thus ?thesis
+ using assms
+ by(simp add: alphaRes_mix perm_eq_subst_mix)
+qed
+
+lemma alphaInput_subst_mix:
+ fixes a :: name
+ and b :: name
+ and P :: piMix
+ and z :: name
+
+ assumes "atom z \<sharp> P"
+
+ shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
+proof(cases "b = z")
+ assume "b = z"
+ thus ?thesis
+ by(simp add: subst_id_mix)
+next
+ assume "b \<noteq> z"
+ thus ?thesis
+ using assms
+ by(simp add: alphaInput_mix perm_eq_subst_mix)
+qed
+
+lemma alphaRep_subst_mix:
+ fixes a :: name
+ and b :: name
+ and P :: piMix
+ and z :: name
+
+ assumes "atom z \<sharp> P"
+
+ shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
+proof(cases "b = z")
+ assume "b = z"
+ thus ?thesis
+ by(simp add: subst_id_mix)
+next
+ assume "b \<noteq> z"
+ thus ?thesis
+ using assms
+ by(simp add: alphaRep_mix perm_eq_subst_mix)
+qed
+
+inductive
+ fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool"
+where
+ "fresh_list_guard_mix [] g"
+| "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g"
+
+equivariance fresh_list_guard_mix
+nominal_inductive fresh_list_guard_mix
+ done
+
+inductive
+ fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool"
+where
+ "fresh_list_sumList_mix [] xg"
+| "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg"
+
+equivariance fresh_list_sumList_mix
+nominal_inductive fresh_list_sumList_mix
+ done
+
+inductive
+ fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool"
+where
+ "fresh_list_mix [] P"
+| "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P"
+
+equivariance fresh_list_mix
+nominal_inductive fresh_list_mix
+ done
+
end
--- a/Nominal/Nominal2.thy Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2.thy Tue Mar 22 12:18:30 2016 +0000
@@ -178,7 +178,7 @@
val raw_induct_thms = #inducts (hd dtinfos)
val raw_exhaust_thms = map #exhaust dtinfos
val raw_size_trms = map HOLogic.size_const raw_tys
- val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd)
+ val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o #2 o #2)
(BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names')))
val raw_result = RawDtInfo
--- a/Nominal/Nominal2_Abs.thy Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2_Abs.thy Tue Mar 22 12:18:30 2016 +0000
@@ -537,7 +537,7 @@
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
instance
- apply(default)
+ apply standard
apply(case_tac [!] x)
apply(simp_all)
done
@@ -559,7 +559,7 @@
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
instance
- apply(default)
+ apply standard
apply(case_tac [!] x)
apply(simp_all)
done
@@ -581,7 +581,7 @@
by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
instance
- apply(default)
+ apply standard
apply(case_tac [!] x)
apply(simp_all)
done
@@ -700,19 +700,19 @@
by (simp_all add: Abs_finite_supp finite_supp)
instance abs_set :: (fs) fs
- apply(default)
+ apply standard
apply(case_tac x)
apply(simp add: supp_Abs finite_supp)
done
instance abs_res :: (fs) fs
- apply(default)
+ apply standard
apply(case_tac x)
apply(simp add: supp_Abs finite_supp)
done
instance abs_lst :: (fs) fs
- apply(default)
+ apply standard
apply(case_tac x)
apply(simp add: supp_Abs finite_supp)
done
@@ -933,7 +933,7 @@
|> Thm.cterm_of ctxt
val cvrs_ty = Thm.ctyp_of_cterm cvrs
val thm' = thm
- |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs]
+ |> Thm.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs]
in
SOME thm'
end
--- a/Nominal/Nominal2_Base.thy Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2_Base.thy Tue Mar 22 12:18:30 2016 +0000
@@ -13,6 +13,9 @@
"atom_decl" "equivariance" :: thy_decl
begin
+declare [[typedef_overloaded]]
+
+
section {* Atoms and Sorts *}
text {* A simple implementation for atom_sorts is strings. *}
@@ -183,7 +186,7 @@
by (simp add: Abs_perm_inverse perm_inv Rep_perm)
instance
-apply default
+apply standard
unfolding Rep_perm_inject [symmetric]
unfolding minus_perm_def
unfolding Rep_perm_add
@@ -325,7 +328,7 @@
"p \<bullet> a = (Rep_perm p) a"
instance
-apply(default)
+apply standard
apply(simp_all add: permute_atom_def Rep_perm_simps)
done
@@ -363,7 +366,7 @@
"p \<bullet> q = p + q - p"
instance
-apply default
+apply standard
apply (simp add: permute_perm_def)
apply (simp add: permute_perm_def algebra_simps)
done
@@ -390,7 +393,7 @@
"p \<bullet> f = (\<lambda>x. p \<bullet> (f (- p \<bullet> x)))"
instance
-apply default
+apply standard
apply (simp add: permute_fun_def)
apply (simp add: permute_fun_def minus_add)
done
@@ -413,7 +416,7 @@
definition "p \<bullet> (b::bool) = b"
instance
-apply(default)
+apply standard
apply(simp_all add: permute_bool_def)
done
@@ -438,7 +441,7 @@
"p \<bullet> X = {p \<bullet> x | x. x \<in> X}"
instance
-apply default
+apply standard
apply (auto simp: permute_set_def)
done
@@ -510,7 +513,7 @@
definition "p \<bullet> (u::unit) = u"
instance
-by (default) (simp_all add: permute_unit_def)
+ by standard (simp_all add: permute_unit_def)
end
@@ -526,7 +529,7 @@
Pair_eqvt: "p \<bullet> (x, y) = (p \<bullet> x, p \<bullet> y)"
instance
-by default auto
+ by standard auto
end
@@ -542,7 +545,7 @@
| Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
instance
-by (default) (case_tac [!] x, simp_all)
+ by standard (case_tac [!] x, simp_all)
end
@@ -558,7 +561,7 @@
| Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
instance
-by (default) (induct_tac [!] x, simp_all)
+ by standard (induct_tac [!] x, simp_all)
end
@@ -580,7 +583,7 @@
| Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"
instance
-by (default) (induct_tac [!] x, simp_all)
+ by standard (induct_tac [!] x, simp_all)
end
@@ -667,7 +670,7 @@
done
instance
-apply(default)
+apply standard
apply(transfer)
apply(simp)
apply(transfer)
@@ -685,7 +688,7 @@
definition "p \<bullet> (c::char) = c"
instance
-by (default) (simp_all add: permute_char_def)
+ by standard (simp_all add: permute_char_def)
end
@@ -695,7 +698,7 @@
definition "p \<bullet> (n::nat) = n"
instance
-by (default) (simp_all add: permute_nat_def)
+ by standard (simp_all add: permute_nat_def)
end
@@ -705,7 +708,7 @@
definition "p \<bullet> (i::int) = i"
instance
-by (default) (simp_all add: permute_int_def)
+ by standard (simp_all add: permute_int_def)
end
@@ -729,22 +732,22 @@
text {* Other type constructors preserve purity. *}
instance "fun" :: (pure, pure) pure
-by default (simp add: permute_fun_def permute_pure)
+ by standard (simp add: permute_fun_def permute_pure)
instance set :: (pure) pure
-by default (simp add: permute_set_def permute_pure)
+ by standard (simp add: permute_set_def permute_pure)
instance prod :: (pure, pure) pure
-by default (induct_tac x, simp add: permute_pure)
+ by standard (induct_tac x, simp add: permute_pure)
instance sum :: (pure, pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+ by standard (induct_tac x, simp_all add: permute_pure)
instance list :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+ by standard (induct_tac x, simp_all add: permute_pure)
instance option :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+ by standard (induct_tac x, simp_all add: permute_pure)
subsection {* Types @{typ char}, @{typ nat}, and @{typ int} *}
@@ -1069,7 +1072,7 @@
begin
instance
-apply(default)
+apply standard
unfolding le_bool_def
apply(perm_simp)
apply(rule refl)
@@ -1081,7 +1084,7 @@
begin
instance
-apply(default)
+apply standard
unfolding le_fun_def
apply(perm_simp)
apply(rule refl)
@@ -1093,7 +1096,7 @@
begin
instance
-apply(default)
+apply standard
unfolding Inf_bool_def
apply(perm_simp)
apply(rule refl)
@@ -1105,7 +1108,7 @@
begin
instance
-apply(default)
+apply standard
unfolding Inf_fun_def INF_def
apply(perm_simp)
apply(rule refl)
@@ -1145,7 +1148,7 @@
by (cases x) simp
lemma split_eqvt [eqvt]:
- shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+ shows "p \<bullet> (case_prod P x) = case_prod (p \<bullet> P) (p \<bullet> x)"
unfolding split_def
by simp
@@ -1456,7 +1459,7 @@
unfolding fresh_def by (simp add: pure_supp)
instance pure < fs
-by default (simp add: pure_supp)
+ by standard (simp add: pure_supp)
subsection {* Type @{typ atom} is finitely-supported. *}
@@ -1474,7 +1477,7 @@
unfolding fresh_def supp_atom by simp
instance atom :: fs
-by default (simp add: supp_atom)
+ by standard (simp add: supp_atom)
section {* Type @{typ perm} is finitely-supported. *}
@@ -1623,7 +1626,7 @@
instance perm :: fs
-by default (simp add: supp_perm finite_perm_lemma)
+ by standard (simp add: supp_perm finite_perm_lemma)
@@ -1649,7 +1652,7 @@
by (simp add: fresh_def supp_Unit)
instance prod :: (fs, fs) fs
-apply default
+apply standard
apply (case_tac x)
apply (simp add: supp_Pair finite_supp)
done
@@ -1674,7 +1677,7 @@
by (simp add: fresh_def supp_Inr)
instance sum :: (fs, fs) fs
-apply default
+apply standard
apply (case_tac x)
apply (simp_all add: supp_Inl supp_Inr finite_supp)
done
@@ -1699,7 +1702,7 @@
by (simp add: fresh_def supp_Some)
instance option :: (fs) fs
-apply default
+apply standard
apply (induct_tac x)
apply (simp_all add: supp_None supp_Some finite_supp)
done
@@ -1752,7 +1755,7 @@
(simp_all add: supp_Nil supp_Cons supp_atom)
instance list :: (fs) fs
-apply default
+apply standard
apply (induct_tac x)
apply (simp_all add: supp_Nil supp_Cons finite_supp)
done
@@ -1895,7 +1898,7 @@
val cty_inst =
[SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))]
val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)]
- val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+ val thm = Thm.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
in
SOME(thm RS @{thm Eq_TrueI})
end
@@ -2120,12 +2123,12 @@
subsection {* Type @{typ "'a multiset"} is finitely supported *}
-lemma set_of_eqvt [eqvt]:
- shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
+lemma set_mset_eqvt [eqvt]:
+ shows "p \<bullet> (set_mset M) = set_mset (p \<bullet> M)"
by (induct M) (simp_all add: insert_eqvt empty_eqvt)
-lemma supp_set_of:
- shows "supp (set_of M) \<subseteq> supp M"
+lemma supp_set_mset:
+ shows "supp (set_mset M) \<subseteq> supp M"
apply (rule supp_fun_app_eqvt)
unfolding eqvt_def
apply(perm_simp)
@@ -2165,11 +2168,11 @@
fixes M::"('a::fs multiset)"
shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
proof -
- have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
- also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
- also have "... = supp (set_of M)"
+ have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
+ also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
+ also have "... = supp (set_mset M)"
by (simp add: supp_of_finite_sets)
- also have " ... \<subseteq> supp M" by (rule supp_set_of)
+ also have " ... \<subseteq> supp M" by (rule supp_set_mset)
finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
qed
@@ -2199,9 +2202,7 @@
by simp
instance multiset :: (fs) fs
- apply (default)
- apply (rule multisets_supp_finite)
- done
+ by standard (rule multisets_supp_finite)
subsection {* Type @{typ "'a fset"} is finitely supported *}
@@ -2252,9 +2253,7 @@
by (simp add: supp_union_fset)
instance fset :: (fs) fs
- apply (default)
- apply (rule fset_finite_supp)
- done
+ by standard (rule fset_finite_supp)
subsection {* Type @{typ "('a, 'b) finfun"} is finitely supported *}
@@ -2279,7 +2278,7 @@
by (auto simp: fresh_def supp_Pair)
instance finfun :: (fs, fs) fs
- apply(default)
+ apply standard
apply(induct_tac x rule: finfun_weak_induct)
apply(simp add: supp_finfun_const finite_supp)
apply(rule finite_subset)
--- a/Nominal/nominal_atoms.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_atoms.ML Tue Mar 22 12:18:30 2016 +0000
@@ -12,7 +12,7 @@
val add_atom_decl: (binding * (binding option)) -> theory -> theory
end;
-structure Atom_Decl :> ATOM_DECL =
+structure Atom_Decl : ATOM_DECL =
struct
val simp_attr = Attrib.internal (K Simplifier.simp_add)
@@ -32,9 +32,9 @@
(* typedef *)
val set = atom_decl_set str;
- fun tac _ = rtac @{thm exists_eq_simple_sort} 1;
+ fun tac ctxt = resolve_tac ctxt @{thms exists_eq_simple_sort} 1;
val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
- Typedef.add_typedef_global false (name, [], NoSyn) set NONE tac thy;
+ Typedef.add_typedef_global {overloaded = false} (name, [], NoSyn) set NONE tac thy;
(* definition of atom and permute *)
val newT = #abs_type (fst info);
@@ -68,7 +68,7 @@
val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def]
val thy = lthy
|> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm]))
- |> Class.prove_instantiation_instance (K (rtac class_thm 1))
+ |> Class.prove_instantiation_instance (fn ctxt => resolve_tac ctxt [class_thm] 1)
|> Local_Theory.exit_global;
in
thy
--- a/Nominal/nominal_dt_alpha.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_alpha.ML Tue Mar 22 12:18:30 2016 +0000
@@ -248,16 +248,19 @@
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
- val (alpha_info, lthy') = Inductive.add_inductive_i
+ val (alpha_info, lthy') = lthy
+ |> Inductive.add_inductive_i
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = false}
- all_alpha_names [] all_alpha_intros [] lthy
+ all_alpha_names [] all_alpha_intros []
val all_alpha_trms_loc = #preds alpha_info;
val alpha_raw_induct_loc = #raw_induct alpha_info;
val alpha_intros_loc = #intrs alpha_info;
val alpha_cases_loc = #elims alpha_info;
- val phi = Proof_Context.export_morphism lthy' lthy;
+ val phi =
+ Proof_Context.export_morphism lthy'
+ (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy);
val all_alpha_trms = all_alpha_trms_loc
|> map (Morphism.term phi)
@@ -313,7 +316,7 @@
fun tac ctxt =
HEADGOAL
- (DETERM o (rtac induct_thm)
+ (DETERM o (resolve_tac ctxt [induct_thm])
THEN_ALL_NEW
(REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt])))
in
@@ -360,8 +363,8 @@
fun tac ctxt =
HEADGOAL
- (DETERM o (rtac alpha_induct_thm)
- THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
+ (DETERM o (resolve_tac ctxt [alpha_induct_thm])
+ THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt])
in
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
|> singleton (Proof_Context.export ctxt' ctxt)
@@ -392,7 +395,7 @@
end
fun distinct_tac ctxt cases_thms distinct_thms =
- rtac notI THEN' eresolve_tac ctxt cases_thms
+ resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms
THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms)
fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info =
@@ -427,7 +430,7 @@
fun alpha_eq_iff_tac ctxt dist_inj intros elims =
SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE'
- (rtac @{thm iffI} THEN'
+ (resolve_tac ctxt @{thms iffI} THEN'
RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj),
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)])
@@ -465,14 +468,15 @@
let
val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv}
- val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' assume_tac ctxt
+ val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt
val bound_tac =
- EVERY' [ rtac exi_zero,
+ EVERY' [ resolve_tac ctxt [exi_zero],
resolve_tac ctxt @{thms alpha_refl},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]
in
- resolve_tac ctxt intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
+ resolve_tac ctxt intros THEN_ALL_NEW
+ FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac]
end
fun raw_prove_refl ctxt alpha_result raw_dt_induct =
@@ -498,19 +502,20 @@
fun prem_bound_tac pred_names alpha_eqvt ctxt =
let
fun trans_prem_tac pred_names ctxt =
- SUBPROOF (fn {prems, context, ...} =>
+ SUBPROOF (fn {prems, context = ctxt', ...} =>
let
- val prems' = map (transform_prem1 context pred_names) prems
+ val prems' = map (transform_prem1 ctxt' pred_names) prems
in
- resolve_tac ctxt prems' 1
+ resolve_tac ctxt' prems' 1
end) ctxt
val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas}
in
EVERY'
- [ etac exi_neg,
+ [ eresolve_tac ctxt [exi_neg],
resolve_tac ctxt @{thms alpha_sym_eqvt},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps),
- eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+ eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
+ resolve_tac ctxt @{thms refl},
trans_prem_tac pred_names ctxt]
end
@@ -527,7 +532,7 @@
fun tac ctxt =
resolve_tac ctxt alpha_intros THEN_ALL_NEW
FIRST' [assume_tac ctxt,
- rtac @{thm sym} THEN' assume_tac ctxt,
+ resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt,
prem_bound_tac alpha_names alpha_eqvt ctxt]
in
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt
@@ -539,7 +544,7 @@
(* applies cases rules and resolves them with the last premise *)
fun ecases_tac cases =
Subgoal.FOCUS (fn {context = ctxt, prems, ...} =>
- HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems)))
+ HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems]))
fun aatac pred_names =
SUBPROOF (fn {context = ctxt, prems, ...} =>
@@ -547,13 +552,13 @@
(* instantiates exI with the permutation p + q *)
val perm_inst_tac =
- Subgoal.FOCUS (fn {params, ...} =>
+ Subgoal.FOCUS (fn {context = ctxt, params, ...} =>
let
val (p, q) = apply2 snd (last2 params)
val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q]
- val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
+ val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
in
- HEADGOAL (rtac exi_inst)
+ HEADGOAL (resolve_tac ctxt [exi_inst])
end)
fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt =
@@ -563,13 +568,14 @@
resolve_tac ctxt intros
THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN'
TRY o EVERY' (* if binders are present *)
- [ etac @{thm exE},
- etac @{thm exE},
+ [ eresolve_tac ctxt @{thms exE},
+ eresolve_tac ctxt @{thms exE},
perm_inst_tac ctxt,
resolve_tac ctxt @{thms alpha_trans_eqvt},
assume_tac ctxt,
aatac pred_names ctxt,
- eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+ eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
+ resolve_tac ctxt @{thms refl},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ])
end
@@ -582,8 +588,9 @@
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms)
THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt
in
- EVERY' [ rtac @{thm allI}, rtac @{thm impI},
- ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
+ EVERY' [ resolve_tac ctxt @{thms allI},
+ resolve_tac ctxt @{thms impI},
+ ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
end
fun prep_trans_goal alpha_trm (arg1, arg2) =
@@ -633,7 +640,7 @@
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
in
Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
- (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN'
+ (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN'
RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans']))))
|> chop (length alpha_trms)
end
@@ -642,20 +649,20 @@
(* proves that alpha_raw implies alpha_bn *)
fun raw_prove_bn_imp_tac alpha_result ctxt =
- SUBPROOF (fn {prems, context, ...} =>
+ SUBPROOF (fn {prems, context = ctxt', ...} =>
let
val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result
val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
- val prems'' = map (transform_prem1 context alpha_names) prems'
+ val prems'' = map (transform_prem1 ctxt' alpha_names) prems'
in
HEADGOAL
(REPEAT_ALL_NEW
- (FIRST' [ rtac @{thm TrueI},
- rtac @{thm conjI},
- resolve_tac ctxt prems',
- resolve_tac ctxt prems'',
- resolve_tac ctxt alpha_intros ]))
+ (FIRST' [ resolve_tac ctxt' @{thms TrueI},
+ resolve_tac ctxt' @{thms conjI},
+ resolve_tac ctxt' prems',
+ resolve_tac ctxt' prems'',
+ resolve_tac ctxt' alpha_intros ]))
end) ctxt
@@ -711,7 +718,7 @@
put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv
permute_prod_def prod.case prod.rec})
- val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset
+ val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset
in
alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
end
@@ -728,7 +735,7 @@
asm_full_simp_tac pre_simpset
THEN' REPEAT o (resolve_tac ctxt @{thms allI impI})
THEN' resolve_tac ctxt alpha_intros
- THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset)
+ THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset)
end
fun raw_constrs_rsp ctxt alpha_result constrs simps =
@@ -796,21 +803,21 @@
by (simp add: rel_fun_def)}
fun raw_prove_perm_bn_tac alpha_result simps ctxt =
- SUBPROOF (fn {prems, context, ...} =>
+ SUBPROOF (fn {prems, context = ctxt', ...} =>
let
val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result
val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
- val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
+ val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems'
in
HEADGOAL
- (simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ prems'))
+ (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems'))
THEN' TRY o REPEAT_ALL_NEW
- (FIRST' [ rtac @{thm TrueI},
- rtac @{thm conjI},
- rtac @{thm refl},
- resolve_tac ctxt prems',
- resolve_tac ctxt prems'',
- resolve_tac ctxt alpha_intros ]))
+ (FIRST' [ resolve_tac ctxt' @{thms TrueI},
+ resolve_tac ctxt' @{thms conjI},
+ resolve_tac ctxt' @{thms refl},
+ resolve_tac ctxt' prems',
+ resolve_tac ctxt' prems'',
+ resolve_tac ctxt' alpha_intros ]))
end) ctxt
fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
--- a/Nominal/nominal_dt_quot.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_quot.ML Tue Mar 22 12:18:30 2016 +0000
@@ -61,7 +61,7 @@
val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1
val qty_args3 = qty_args2 ~~ alpha_equivp_thms
in
- fold_map Quotient_Type.add_quotient_type qty_args3 lthy
+ fold_map (Quotient_Type.add_quotient_type {overloaded = false}) qty_args3 lthy
end
(* a wrapper for lifting a raw constant *)
@@ -73,7 +73,7 @@
val rhs_raw = rconst
val raw_var = (Binding.name qconst_name, NONE, mx')
- val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
+ val ((binding, _, mx), ctxt) = Proof_Context.cert_var raw_var lthy
val lhs = Syntax.check_term ctxt lhs_raw
val rhs = Syntax.check_term ctxt rhs_raw
@@ -91,7 +91,9 @@
let
val (qconst_infos, lthy') =
fold_map (lift_raw_const qtys) consts_specs lthy
- val phi = Proof_Context.export_morphism lthy' lthy
+ val phi =
+ Proof_Context.export_morphism lthy'
+ (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy)
in
(map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy')
end
@@ -153,14 +155,14 @@
|> fst
end
-fun unraw_vars_thm thm =
+fun unraw_vars_thm ctxt thm =
let
fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
val vars = Term.add_vars (Thm.prop_of thm) []
- val vars' = map (Var o unraw_var_str) vars
+ val vars' = map (Thm.cterm_of ctxt o Var o unraw_var_str) vars
in
- Thm.certify_instantiate ([], (vars ~~ vars')) thm
+ Thm.instantiate ([], (vars ~~ vars')) thm
end
fun unraw_bounds_thm th =
@@ -174,7 +176,7 @@
fun lift_thms qtys simps thms ctxt =
(map (Quotient_Tacs.lifted ctxt qtys simps
#> unraw_bounds_thm
- #> unraw_vars_thm
+ #> unraw_vars_thm ctxt
#> Drule.zero_var_indexes) thms, ctxt)
@@ -228,13 +230,13 @@
|> HOLogic.mk_Trueprop
val tac =
- EVERY' [ rtac @{thm supports_finite},
+ EVERY' [ resolve_tac ctxt' @{thms supports_finite},
resolve_tac ctxt' qsupports_thms,
asm_simp_tac (put_simpset HOL_ss ctxt'
addsimps @{thms finite_supp supp_Pair finite_Un}) ]
in
Goal.prove ctxt' [] [] goals
- (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
+ (K (HEADGOAL (resolve_tac ctxt' [qinduct] THEN_ALL_NEW tac)))
|> singleton (Proof_Context.export ctxt' ctxt)
|> Old_Datatype_Aux.split_conj_thm
|> map zero_var_indexes
@@ -500,7 +502,7 @@
@ @{thms finite.intros finite_Un finite_set finite_fset}
in
Goal.prove ctxt [] [] goal
- (K (HEADGOAL (rtac @{thm at_set_avoiding1}
+ (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding1}
THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss)))))
end
@@ -559,7 +561,7 @@
let
fun aux_tac prem bclauses =
case (get_all_binders bclauses) of
- [] => EVERY' [rtac prem, assume_tac ctxt]
+ [] => EVERY' [resolve_tac ctxt [prem], assume_tac ctxt]
| binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
let
val parms = map (Thm.term_of o snd) params
@@ -567,18 +569,18 @@
val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
val (([(_, fperm)], fprops), ctxt') = Obtain.result
- (fn ctxt' => EVERY1 [etac exE,
+ (fn ctxt' => EVERY1 [eresolve_tac ctxt [exE],
full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
- REPEAT o (etac @{thm conjE})]) [fthm] ctxt
+ REPEAT o (eresolve_tac ctxt @{thms conjE})]) [fthm] ctxt
val abs_eq_thms = flat
(map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses)
val ((_, eqs), ctxt'') = Obtain.result
(fn ctxt'' => EVERY1
- [ REPEAT o (etac @{thm exE}),
- REPEAT o (etac @{thm conjE}),
- REPEAT o (dtac setify),
+ [ REPEAT o (eresolve_tac ctxt @{thms exE}),
+ REPEAT o (eresolve_tac ctxt @{thms conjE}),
+ REPEAT o (dresolve_tac ctxt [setify]),
full_simp_tac (put_simpset HOL_basic_ss ctxt''
addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt'
@@ -592,24 +594,24 @@
val tac1 = SOLVED' (EVERY'
[ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
- conj_tac (DETERM o resolve_tac ctxt'' fprops') ])
+ conj_tac ctxt'' (DETERM o resolve_tac ctxt'' fprops') ])
(* for equalities between constructors *)
val tac2 = SOLVED' (EVERY'
- [ rtac (@{thm ssubst} OF prems),
+ [ resolve_tac ctxt [@{thm ssubst} OF prems],
rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms),
rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs),
- conj_tac (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
+ conj_tac ctxt'' (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
(* proves goal "P" *)
val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl)
- (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
+ (K (EVERY1 [ resolve_tac ctxt'' [prem], RANGE [tac1, tac2] ]))
|> singleton (Proof_Context.export ctxt'' ctxt)
in
- rtac side_thm 1
+ resolve_tac ctxt [side_thm] 1
end) ctxt
in
- EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
+ EVERY1 [resolve_tac ctxt [qexhaust_thm], RANGE (map2 aux_tac prems bclausess)]
end
@@ -726,12 +728,10 @@
val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params
val vs = Term.add_vars (Thm.prop_of thm) []
val vs_tys = map (Type.legacy_freeze_type o snd) vs
- val vs_ctrms = map (Thm.cterm_of ctxt' o Var) vs
val assigns = map (lookup ty_parms) vs_tys
-
- val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
+ val thm' = infer_instantiate ctxt' (map #1 vs ~~ assigns) thm
in
- rtac thm' 1
+ resolve_tac ctxt' [thm'] 1
end) ctxt
THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt)
--- a/Nominal/nominal_dt_rawfuns.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML Tue Mar 22 12:18:30 2016 +0000
@@ -261,7 +261,9 @@
val {fs, simps, inducts, ...} = info;
- val morphism = Proof_Context.export_morphism lthy'' lthy
+ val morphism =
+ Proof_Context.export_morphism lthy''
+ (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy)
val simps_exp = map (Morphism.thm morphism) (the simps)
val inducts_exp = map (Morphism.thm morphism) (the inducts)
@@ -334,7 +336,9 @@
val {fs, simps, ...} = info;
- val morphism = Proof_Context.export_morphism lthy'' lthy
+ val morphism =
+ Proof_Context.export_morphism lthy''
+ (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy)
val simps_exp = map (Morphism.thm morphism) (the simps)
in
(fs, simps_exp, lthy'')
@@ -355,13 +359,12 @@
val goals =
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
- val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs)
-
- val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
- THEN_ALL_NEW asm_simp_tac simpset) 1
in
- Goal.prove ctxt perm_indnames [] goals (K tac)
+ Goal.prove ctxt perm_indnames [] goals
+ (fn {context = ctxt', ...} =>
+ (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW
+ asm_simp_tac
+ (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_zero} :: perm_defs))) 1)
|> Old_Datatype_Aux.split_conj_thm
end
@@ -379,14 +382,12 @@
val goals =
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
- (* FIXME proper goal context *)
- val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs)
-
- val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
- THEN_ALL_NEW asm_simp_tac simpset) 1
in
- Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac)
+ Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals
+ (fn {context = ctxt', ...} =>
+ (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW
+ asm_simp_tac
+ (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_plus} :: perm_defs))) 1)
|> Old_Datatype_Aux.split_conj_thm
end
--- a/Nominal/nominal_eqvt.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_eqvt.ML Tue Mar 22 12:18:30 2016 +0000
@@ -33,7 +33,7 @@
fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
let
val cpi = Thm.cterm_of ctxt pi
- val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
+ val pi_intro_rule = Thm.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
val eqvt_sconfig = eqvt_strict_config addexcls pred_names
val simps1 =
put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all}
@@ -47,7 +47,8 @@
val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems'
val prems''' = map (simplify simps2 o simplify simps1) prems''
in
- HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems'''))
+ HEADGOAL (resolve_tac ctxt [intro] THEN_ALL_NEW
+ resolve_tac ctxt (prems' @ prems'' @ prems'''))
end) ctxt
end
@@ -55,7 +56,7 @@
let
val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros
in
- EVERY' ((DETERM o rtac induct) :: cases)
+ EVERY' ((DETERM o resolve_tac ctxt [induct]) :: cases)
end
--- a/Nominal/nominal_function.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_function.ML Tue Mar 22 12:18:30 2016 +0000
@@ -151,7 +151,7 @@
let
val NominalFunctionResult {fs, R, psimps, simple_pinducts,
termination, domintros, cases, eqvts, ...} =
- cont (Thm.close_derivation proof)
+ cont lthy (Thm.close_derivation proof)
val fnames = map (fst o fst) fixes
fun qualify n = Binding.name n
@@ -214,7 +214,7 @@
in
lthy'
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
- |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
+ |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
end
val nominal_function =
--- a/Nominal/nominal_function_core.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_function_core.ML Tue Mar 22 12:18:30 2016 +0000
@@ -22,7 +22,7 @@
* thm list (* GIntros *)
* thm (* Ginduct *)
* thm (* goalstate *)
- * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
+ * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
) * local_theory
val inductive_def : (binding * typ) * mixfix -> term list -> local_theory
@@ -520,7 +520,7 @@
val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
val exactly_one =
- ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
+ ex1I |> Thm.instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
|> curry (op COMP) existence
|> curry (op COMP) uniqueness
|> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
@@ -556,7 +556,7 @@
val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
- |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
+ |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
@@ -602,6 +602,7 @@
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
lthy
+ |> Config.put Inductive.inductive_internals true
|> Proof_Context.concealed
|> Inductive.add_inductive_i
{quiet_mode = true,
@@ -616,6 +617,7 @@
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
[] (* no special monos *)
||> Proof_Context.restore_naming lthy
+ ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals)
val cert = Thm.cterm_of lthy
fun requantify orig_intro thm =
@@ -849,9 +851,9 @@
subset_induct_rule
|> Thm.forall_intr (Thm.cterm_of ctxt D)
|> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
- |> atac 1 |> Seq.hd
+ |> assume_tac ctxt 1 |> Seq.hd
|> (curry op COMP) (acc_downward
- |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)]
+ |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)]
(map (SOME o Thm.cterm_of ctxt) [R, x, z]))
|> Thm.forall_intr (Thm.cterm_of ctxt z)
|> Thm.forall_intr (Thm.cterm_of ctxt x))
@@ -1063,11 +1065,8 @@
(prove_stuff lthy globals G f R xclauses complete compat
compat_store G_elim G_eqvt invariant) f_defthm
- fun mk_partial_rules provedgoal =
+ fun mk_partial_rules newctxt provedgoal =
let
- val newthy = Thm.theory_of_thm provedgoal (*FIXME*)
- val newctxt = Proof_Context.init_global newthy (*FIXME*)
-
val ((graph_is_function, complete_thm), graph_is_eqvt) =
provedgoal
|> Conjunction.elim
--- a/Nominal/nominal_induct.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_induct.ML Tue Mar 22 12:18:30 2016 +0000
@@ -5,9 +5,8 @@
structure NominalInduct:
sig
- val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
- (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> Rule_Cases.cases_tactic
-
+ val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list ->
+ (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> context_tactic
val nominal_induct_method: (Proof.context -> Proof.method) context_parser
end =
@@ -19,7 +18,7 @@
fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
fun tuple_fun Ts (xi, T) =
- Library.funpow (length Ts) HOLogic.mk_split
+ Library.funpow (length Ts) HOLogic.mk_case_prod
(Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
fun split_all_tuples ctxt =
@@ -57,9 +56,9 @@
end;
val substs =
map2 subst insts concls |> flat |> distinct (op =)
- |> map (apply2 (Thm.cterm_of ctxt));
+ |> map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of ctxt u));
in
- (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule)
+ (((cases, nconcls), consumes), infer_instantiate ctxt substs joined_rule)
end;
fun rename_params_rule internal xs rule =
@@ -79,12 +78,12 @@
fun rename_prems prop =
let val (As, C) = Logic.strip_horn prop
in Logic.list_implies (map rename As, C) end;
- in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
+ in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;
(* nominal_induct_tac *)
-fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
+fun nominal_induct_tac simp def_insts avoiding fixings rules facts i (ctxt, st) =
let
val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs;
@@ -97,8 +96,8 @@
fun rule_cases ctxt r =
let val r' = if simp then Induct.simplified_rule ctxt r else r
in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
- in
- (fn i => fn st =>
+
+ fun context_tac _ _ =
rules
|> inst_mutual_rule ctxt insts avoiding
|> Rule_Cases.consume ctxt (flat defs) facts
@@ -111,7 +110,7 @@
val xs = nth_list fixings (j - 1);
val k = nth concls (j - 1) + more_consumes
in
- Method.insert_tac (more_facts @ adefs) THEN'
+ Method.insert_tac ctxt (more_facts @ adefs) THEN'
(if simp then
Induct.rotate_tac k (length adefs) THEN'
Induct.arbitrary_tac defs_ctxt k
@@ -124,13 +123,15 @@
Induct.guess_instance ctxt
(finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
|> Seq.maps (fn rule' =>
- CASES (rule_cases ctxt rule' cases)
- (Tactic.rtac (rename_params_rule false [] rule') i THEN
- PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
- THEN_ALL_NEW_CASES
+ CONTEXT_CASES (rule_cases ctxt rule' cases)
+ (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN
+ PRIMITIVE
+ (singleton (Proof_Context.export defs_ctxt
+ (Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) ctxt)))) (ctxt, st'))));
+ in
+ (context_tac CONTEXT_THEN_ALL_NEW
((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
- else K all_tac)
- THEN_ALL_NEW Induct.rulify_tac ctxt)
+ else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt)) i (ctxt, st)
end;
@@ -173,8 +174,8 @@
Scan.lift (Args.mode Induct.no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) >>
- (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
- HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
+ (fn (no_simp, (((x, y), z), w)) => fn _ => fn facts =>
+ nominal_induct_tac (not no_simp) x y z w facts 1);
end
--- a/Nominal/nominal_inductive.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_inductive.ML Tue Mar 22 12:18:30 2016 +0000
@@ -24,11 +24,11 @@
fun mk_cminus p =
Thm.apply @{cterm "uminus :: perm => perm"} p
-fun minus_permute_intro_tac p =
- rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})
+fun minus_permute_intro_tac ctxt p =
+ resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}]
fun minus_permute_elim p thm =
- thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
+ thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
(* fixme: move to nominal_library *)
fun real_head_of (@{term Trueprop} $ t) = real_head_of t
@@ -156,23 +156,23 @@
val all_elims =
let
fun spec' ct =
- Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
+ Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
in
fold (fn ct => fn th => th RS spec' ct)
end
fun helper_tac flag prm p ctxt =
- Subgoal.SUBPROOF (fn {context, prems, ...} =>
+ Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} =>
let
val prems' = prems
|> map (minus_permute_elim p)
- |> map (eqvt_srule context)
+ |> map (eqvt_srule ctxt')
val prm' = (prems' MRS prm)
|> flag ? (all_elims [p])
- |> flag ? (eqvt_srule context)
+ |> flag ? (eqvt_srule ctxt')
in
- asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
+ asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
end) ctxt
fun non_binder_tac prem intr_cvars Ps ctxt =
@@ -183,15 +183,15 @@
val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms
val prem' = prem
- |> cterm_instantiate (intr_cvars ~~ p_prms)
- |> eqvt_srule ctxt
+ |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms)
+ |> eqvt_srule ctxt'
(* for inductive-premises*)
fun tac1 prm = helper_tac true prm p ctxt'
(* for non-inductive premises *)
fun tac2 prm =
- EVERY' [ minus_permute_intro_tac p,
+ EVERY' [ minus_permute_intro_tac ctxt' p,
eqvt_stac ctxt',
helper_tac false prm p ctxt' ]
@@ -199,7 +199,7 @@
(if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
in
EVERY1 [ eqvt_stac ctxt',
- rtac prem',
+ resolve_tac ctxt' [prem'],
RANGE (map (SUBGOAL o select) prems) ]
end) ctxt
@@ -217,8 +217,9 @@
val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss)
in
Goal.prove ctxt [] [] fresh_goal
- (K (HEADGOAL (rtac @{thm at_set_avoiding2}
- THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp])))
+ (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2}
+ THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o
+ eresolve_tac ctxt @{thms conjE}, simp])))
end
val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x"
@@ -238,27 +239,27 @@
val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm
val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args
- val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm
+ val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm
|> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems)))
val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm'
val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result
- (K (EVERY1 [etac @{thm exE},
+ (K (EVERY1 [eresolve_tac ctxt @{thms exE},
full_simp_tac (put_simpset HOL_basic_ss ctxt
addsimps @{thms supp_Pair fresh_star_Un}),
- REPEAT o etac @{thm conjE},
- dtac fresh_star_plus,
- REPEAT o dtac supp_perm_eq'])) [fthm] ctxt
+ REPEAT o eresolve_tac ctxt @{thms conjE},
+ dresolve_tac ctxt [fresh_star_plus],
+ REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt
val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs)
fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt
- val cperms = map (Thm.cterm_of ctxt o perm_const) prm_tys
+ val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms
val prem' = prem
- |> cterm_instantiate (intr_cvars ~~ qp_prms)
- |> eqvt_srule ctxt
+ |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms)
+ |> eqvt_srule ctxt'
val fprop' = eqvt_srule ctxt' fprop
val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop'])
@@ -268,8 +269,8 @@
(* for non-inductive premises *)
fun tac2 prm =
- EVERY' [ minus_permute_intro_tac (mk_cplus q p),
- eqvt_stac ctxt,
+ EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p),
+ eqvt_stac ctxt',
helper_tac false prm (mk_cplus q p) ctxt' ]
fun select prm (t, i) =
@@ -279,11 +280,11 @@
(fn {context = ctxt'', ...} =>
EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
eqvt_stac ctxt'',
- rtac prem',
+ resolve_tac ctxt'' [prem'],
RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
|> singleton (Proof_Context.export ctxt' ctxt)
in
- rtac side_thm 1
+ resolve_tac ctxt [side_thm] 1
end) ctxt
fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =
@@ -291,17 +292,17 @@
val tac1 = non_binder_tac prem intr_cvars Ps ctxt
val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
in
- EVERY' [ rtac @{thm allI}, rtac @{thm allI},
+ EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI},
if null avoid then tac1 else tac2 ]
end
fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args
- {prems, context} =
+ {prems, context = ctxt} =
let
val cases_tac =
- map7 (case_tac context Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
+ map7 (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
in
- EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ]
+ EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ]
end
val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp}
--- a/Nominal/nominal_library.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_library.ML Tue Mar 22 12:18:30 2016 +0000
@@ -104,7 +104,7 @@
val atomize_concl: Proof.context -> thm -> thm
(* applies a tactic to a formula composed of conjunctions *)
- val conj_tac: (int -> tactic) -> int -> tactic
+ val conj_tac: Proof.context -> (int -> tactic) -> int -> tactic
end
@@ -450,9 +450,9 @@
val monos = Inductive.get_monos ctxt
val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def}
in
- EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
+ EVERY [cut_facts_tac [thm] 1, eresolve_tac ctxt [rev_mp] 1,
REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)),
- REPEAT_DETERM (rtac impI 1 THEN (assume_tac ctxt 1 ORELSE tac))]
+ REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))]
end
fun map_thm ctxt f tac thm =
@@ -485,10 +485,10 @@
| split_conj2 _ _ = NONE;
fun transform_prem1 ctxt names thm =
- map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm
+ map_thm ctxt (split_conj1 names) (eresolve_tac ctxt [conjunct1] 1) thm
fun transform_prem2 ctxt names thm =
- map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm
+ map_thm ctxt (split_conj2 names) (eresolve_tac ctxt [conjunct2] 1) thm
(* transforms a theorem into one of the object logic *)
@@ -499,12 +499,13 @@
(* applies a tactic to a formula composed of conjunctions *)
-fun conj_tac tac i =
+fun conj_tac ctxt tac i =
let
fun select (trm, i) =
case trm of
@{term "Trueprop"} $ t' => select (t', i)
- | @{term "op &"} $ _ $ _ => EVERY' [rtac @{thm conjI}, RANGE [conj_tac tac, conj_tac tac]] i
+ | @{term "op &"} $ _ $ _ =>
+ EVERY' [resolve_tac ctxt @{thms conjI}, RANGE [conj_tac ctxt tac, conj_tac ctxt tac]] i
| _ => tac i
in
SUBGOAL select i
--- a/Nominal/nominal_mutual.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_mutual.ML Tue Mar 22 12:18:30 2016 +0000
@@ -19,7 +19,7 @@
-> term list
-> local_theory
-> ((thm (* goalstate *)
- * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
+ * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
) * local_theory)
end
@@ -330,21 +330,23 @@
val induct_thm = case induct_thms of
[thm] => thm
- |> Drule.gen_all (Variable.maxidx_of ctxt')
+ |> Variable.gen_all ctxt'
|> Thm.permute_prems 0 1
|> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm)
| thms => thms
- |> map (Drule.gen_all (Variable.maxidx_of ctxt'))
+ |> map (Variable.gen_all ctxt')
|> map (Rule_Cases.add_consumes 1)
|> snd o Rule_Cases.strict_mutual_rule ctxt'
|> atomize_concl ctxt'
fun tac ctxt thm =
- rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt
+ resolve_tac ctxt [Variable.gen_all ctxt thm]
+ THEN_ALL_NEW assume_tac ctxt
in
Goal.prove ctxt' (flat arg_namess) [] goal
(fn {context = ctxt'', ...} =>
- HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms)))
+ HEADGOAL (DETERM o (resolve_tac ctxt'' [induct_thm]) THEN'
+ RANGE (map (tac ctxt'') eqvts_thms)))
|> singleton (Proof_Context.export ctxt' ctxt)
|> split_conj_thm
|> map (fn th => th RS mp)
@@ -441,7 +443,7 @@
val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') =
Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy''
- val mutual_cont = mk_partial_rules_mutual lthy''' cont mutual'
+ fun mutual_cont ctxt = mk_partial_rules_mutual lthy''' (cont ctxt) mutual'
(* proof of equivalence between graph and auxiliary graph *)
val x = Var(("x", 0), ST)
@@ -474,22 +476,25 @@
val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms
val inj_thm = Goal.prove lthy''' [] [] goal_inj
- (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1)))
+ (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct]
+ THEN_ALL_NEW asm_simp_tac simpset1)))
fun aux_tac thm =
- rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW
+ resolve_tac lthy''' [Variable.gen_all lthy''' thm] THEN_ALL_NEW
asm_full_simp_tac (simpset1 addsimps [inj_thm])
val iff1_thm = Goal.prove lthy''' [] [] goal_iff1
- (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms))))
- |> Drule.gen_all (Variable.maxidx_of lthy''')
+ (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct]
+ THEN' RANGE (map aux_tac GIntro_thms))))
+ |> Variable.gen_all lthy'''
val iff2_thm = Goal.prove lthy''' [] [] goal_iff2
- (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE
+ (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_induct] THEN' RANGE
(map (aux_tac o simplify simpset0) GIntro_aux_thms))))
- |> Drule.gen_all (Variable.maxidx_of lthy''')
+ |> Variable.gen_all lthy'''
val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux)))
- (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm]))))
+ (K (HEADGOAL (EVERY' ((map (resolve_tac lthy''' o single) @{thms ext ext iffI}) @
+ [eresolve_tac lthy''' [iff2_thm], eresolve_tac lthy''' [iff1_thm]]))))
val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm]))
val goalstate' =
--- a/Nominal/nominal_permeq.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_permeq.ML Tue Mar 22 12:18:30 2016 +0000
@@ -141,7 +141,7 @@
val ty_insts = map SOME [b, a]
val term_insts = map SOME [p, f, x]
in
- Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
+ Thm.instantiate' ty_insts term_insts @{thm eqvt_apply}
end
| _ => Conv.no_conv ctrm
--- a/Nominal/nominal_thmdecls.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_thmdecls.ML Tue Mar 22 12:18:30 2016 +0000
@@ -183,8 +183,9 @@
in
REPEAT o FIRST'
[CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms),
- rtac (thm RS @{thm "trans"}),
- rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}]
+ resolve_tac ctxt [thm RS @{thm trans}],
+ resolve_tac ctxt @{thms trans[OF "permute_fun_def"]} THEN'
+ resolve_tac ctxt @{thms ext}]
end
in
@@ -213,8 +214,12 @@
let
val ss_thms = @{thms "permute_minus_cancel"(2)}
in
- EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt,
- rtac @{thm "permute_boolI"}, dtac thm',
+ EVERY' [resolve_tac ctxt @{thms iffI},
+ dresolve_tac ctxt @{thms permute_boolE},
+ resolve_tac ctxt [thm],
+ assume_tac ctxt,
+ resolve_tac ctxt @{thms permute_boolI},
+ dresolve_tac ctxt [thm'],
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)]
end
@@ -232,7 +237,7 @@
val p = concl |> dest_comb |> snd |> find_perm
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
- val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm
+ val thm' = infer_instantiate ctxt' [(#1 (dest_Var p), Thm.cterm_of ctxt' (mk_minus p'))] thm
in
Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1)
|> singleton (Proof_Context.export ctxt' ctxt)