--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Tue Aug 07 18:54:52 2012 +0100
@@ -10,8 +10,8 @@
| "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))"
| "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
(M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))"
-unfolding eqvt_def CPS_graph_def
-apply (rule, perm_simp, rule, rule)
+unfolding eqvt_def CPS_graph_aux_def
+apply (simp)
using [[simproc del: alpha_lst]]
apply (simp_all add: fresh_Pair_elim)
apply (rule_tac y="x" in lt.exhaust)
@@ -80,8 +80,9 @@
"(Var x)+ = Var x"
| "(Lam x M)+ = Lam x (M*)"
| "(M $$ N)+ = M $$ N"
- unfolding convert_graph_def eqvt_def
- apply (rule, perm_simp, rule, rule)
+ unfolding convert_graph_aux_def eqvt_def
+ apply (simp)
+ apply(rule TrueI)
apply (erule lt.exhaust)
using [[simproc del: alpha_lst]]
apply (simp_all)
@@ -114,8 +115,8 @@
Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))"
| "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
Kapply (M $$ N) K = M; (Lam m (N* $$ (Lam n (Var m $$ Var n $$ K))))"
- unfolding Kapply_graph_def eqvt_def
- apply (rule, perm_simp, rule, rule)
+ unfolding Kapply_graph_aux_def eqvt_def
+ apply (simp)
using [[simproc del: alpha_lst]]
apply (simp_all)
apply (case_tac x)
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Tue Aug 07 18:54:52 2012 +0100
@@ -16,8 +16,8 @@
| fill_fun : "(CFun C N)<M> = (C<M>) $$ N"
| fill_arg : "(CArg N C)<M> = N $$ (C<M>)"
| fill_abs : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
- unfolding eqvt_def fill_graph_def
- apply perm_simp
+ unfolding eqvt_def fill_graph_aux_def
+ apply simp
using [[simproc del: alpha_lst]]
apply auto
apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
@@ -41,8 +41,8 @@
| "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"
| "ccomp (CArg N C) C' = CArg N (ccomp C C')"
| "ccomp (CFun C N) C' = CFun (ccomp C C') N"
- unfolding eqvt_def ccomp_graph_def
- apply perm_simp
+ unfolding eqvt_def ccomp_graph_aux_def
+ apply simp
using [[simproc del: alpha_lst]]
apply auto
apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Tue Aug 07 18:54:52 2012 +0100
@@ -13,8 +13,7 @@
| "(x~)^l = l $$ (x~)"
| "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
- apply (simp only: eqvt_def CPS1_CPS2_graph_def)
- apply (rule, perm_simp, rule)
+ apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)
using [[simproc del: alpha_lst]]
apply auto
apply (case_tac x)
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Tue Aug 07 18:54:52 2012 +0100
@@ -15,8 +15,7 @@
| "(x~)^l = l $$ (x~)"
| "(M $$ N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
- apply (simp only: eqvt_def CPS1_CPS2_graph_def)
- apply (rule, perm_simp, rule)
+ apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)
apply (auto simp only:)
apply (case_tac x)
apply (case_tac a)
--- a/Nominal/Ex/CPS/Lt.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy Tue Aug 07 18:54:52 2012 +0100
@@ -16,7 +16,7 @@
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
- unfolding eqvt_def subst_graph_def
+ unfolding eqvt_def subst_graph_aux_def
apply (simp)
apply(rule TrueI)
using [[simproc del: alpha_lst]]
@@ -51,8 +51,8 @@
"isValue (Var x) = True"
| "isValue (Lam y N) = True"
| "isValue (A $$ B) = False"
- unfolding eqvt_def isValue_graph_def
- by (perm_simp, auto)
+ unfolding eqvt_def isValue_graph_aux_def
+ by (auto)
(erule lt.exhaust, auto)
termination (eqvt)
--- a/Nominal/Ex/Classical.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Classical.thy Tue Aug 07 18:54:52 2012 +0100
@@ -67,7 +67,7 @@
(if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
| "atom a \<sharp> (d, e) \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
apply(simp only: eqvt_def)
- apply(simp only: crename_graph_def)
+ apply(simp only: crename_graph_aux_def)
apply (rule, perm_simp, rule)
apply(rule TrueI)
-- "covered all cases"
@@ -272,7 +272,7 @@
| "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] =
(if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
apply(simp only: eqvt_def)
- apply(simp only: nrename_graph_def)
+ apply(simp only: nrename_graph_aux_def)
apply (rule, perm_simp, rule)
apply(rule TrueI)
-- "covered all cases"
@@ -474,7 +474,7 @@
(if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z'
else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
apply(simp only: eqvt_def)
- apply(simp only: substn_graph_def)
+ apply(simp only: substn_graph_aux_def)
apply (rule, perm_simp, rule)
apply(rule TrueI)
-- "covered all cases"
--- a/Nominal/Ex/Lambda.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Lambda.thy Tue Aug 07 18:54:52 2012 +0100
@@ -7,7 +7,6 @@
atom_decl name
-
ML {* trace := true *}
nominal_datatype lam =
@@ -39,7 +38,7 @@
"is_app (Var x) = False"
| "is_app (App t1 t2) = True"
| "is_app (Lam [x]. t) = False"
-apply(simp add: eqvt_def is_app_graph_def)
+apply(simp add: eqvt_def is_app_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
apply(auto)[3]
@@ -59,7 +58,7 @@
"rator (Var x) = None"
| "rator (App t1 t2) = Some t1"
| "rator (Lam [x]. t) = None"
-apply(simp add: eqvt_def rator_graph_def)
+apply(simp add: eqvt_def rator_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
apply(auto)[3]
@@ -74,7 +73,7 @@
"rand (Var x) = None"
| "rand (App t1 t2) = Some t2"
| "rand (Lam [x]. t) = None"
-apply(simp add: eqvt_def rand_graph_def)
+apply(simp add: eqvt_def rand_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
apply(auto)[3]
@@ -90,7 +89,7 @@
| "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
| "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and>
((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
-apply(simp add: eqvt_def is_eta_nf_graph_def)
+apply(simp add: eqvt_def is_eta_nf_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
apply(auto)[3]
@@ -120,7 +119,7 @@
"var_pos y (Var x) = (if y = x then {[]} else {})"
| "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
| "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
-apply(simp add: eqvt_def var_pos_graph_def)
+apply(simp add: eqvt_def var_pos_graph_aux_def)
apply(rule TrueI)
apply(case_tac x)
apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
@@ -166,7 +165,7 @@
"(Var x)[y ::== s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
- apply(simp add: eqvt_def subst'_graph_def)
+ apply(simp add: eqvt_def subst'_graph_aux_def)
apply(rule TrueI)
apply(case_tac x)
apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
@@ -200,9 +199,7 @@
"frees_lst (Var x) = [atom x]"
| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
- unfolding eqvt_def
- unfolding frees_lst_graph_def
-apply(simp)
+apply(simp add: eqvt_def frees_lst_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
using [[simproc del: alpha_lst]]
@@ -228,7 +225,7 @@
"frees_set (Var x) = {atom x}"
| "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
| "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
- apply(simp add: eqvt_def frees_set_graph_def)
+ apply(simp add: eqvt_def frees_set_graph_aux_def)
apply(erule frees_set_graph.induct)
apply(auto)[9]
apply(rule_tac y="x" in lam.exhaust)
@@ -256,7 +253,7 @@
"height (Var x) = 1"
| "height (App t1 t2) = max (height t1) (height t2) + 1"
| "height (Lam [x].t) = height t + 1"
- apply(simp add: eqvt_def height_graph_def)
+ apply(simp add: eqvt_def height_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
using [[simproc del: alpha_lst]]
@@ -279,8 +276,7 @@
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
- unfolding eqvt_def subst_graph_def
- apply(simp)
+ apply(simp add: eqvt_def subst_graph_aux_def)
apply(rule TrueI)
using [[simproc del: alpha_lst]]
apply(auto)
@@ -468,7 +464,7 @@
"trans (Var x) xs = lookup xs 0 x"
| "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
| "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
- apply (simp add: eqvt_def trans_graph_def)
+ apply (simp add: eqvt_def trans_graph_aux_def)
apply (erule trans_graph.induct)
apply (auto simp add: ln.fresh)[3]
apply (simp add: supp_lookup_fresh)
@@ -503,7 +499,7 @@
"cntlams (Var x) = 0"
| "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
| "cntlams (Lam [x]. t) = Suc (cntlams t)"
- apply(simp add: eqvt_def cntlams_graph_def)
+ apply(simp add: eqvt_def cntlams_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
apply(auto)[3]
@@ -530,7 +526,7 @@
"cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
| "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
| "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
- apply(simp add: eqvt_def cntbvs_graph_def)
+ apply(simp add: eqvt_def cntbvs_graph_aux_def)
apply(rule TrueI)
apply(case_tac x)
apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -589,8 +585,7 @@
| "transdb (App t1 t2) xs =
Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
- unfolding eqvt_def transdb_graph_def
- apply(simp)
+ apply(simp add: eqvt_def transdb_graph_aux_def)
apply(rule TrueI)
apply (case_tac x)
apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -651,7 +646,7 @@
| "apply_subst (Var x) t2 = App (Var x) t2"
| "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
| "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
- apply(simp add: eval_apply_subst_graph_def eqvt_def)
+ apply(simp add: eval_apply_subst_graph_aux_def eqvt_def)
apply(rule TrueI)
apply (case_tac x)
apply (case_tac a rule: lam.exhaust)
@@ -703,8 +698,7 @@
"atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
| "q (Var x) N = Var x"
| "q (App l r) N = App l r"
-unfolding eqvt_def q_graph_def
-apply (simp)
+apply(simp add: eqvt_def q_graph_aux_def)
apply (rule TrueI)
apply (case_tac x)
apply (rule_tac y="a" in lam.exhaust)
@@ -732,7 +726,7 @@
| "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
| "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
| "\<not>eqvt f \<Longrightarrow> map_term f t = t"
- apply (simp add: eqvt_def map_term_graph_def)
+ apply (simp add: eqvt_def map_term_graph_aux_def)
apply(rule TrueI)
apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
using [[simproc del: alpha_lst]]
@@ -812,7 +806,7 @@
where
"Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
| "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
-unfolding eqvt_def Z_graph_def
+apply(simp add: eqvt_def Z_graph_aux_def)
apply (rule, perm_simp, rule)
oops
@@ -852,7 +846,7 @@
| "aux (Lam [x].t) (App t1 t2) xs = False"
| "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow>
aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
- apply (simp add: eqvt_def aux_graph_def)
+ apply (simp add: eqvt_def aux_graph_aux_def)
apply(erule aux_graph.induct)
apply(simp_all add: fresh_star_def pure_fresh)[9]
apply(case_tac x)
@@ -899,8 +893,8 @@
| "aux2 (Lam [x].t) (Var y) = False"
| "aux2 (Lam [x].t) (App t1 t2) = False"
| "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
- apply(simp add: eqvt_def aux2_graph_def)
- apply(simp)
+ apply(simp add: eqvt_def aux2_graph_aux_def)
+ apply(rule TrueI)
apply(case_tac x)
apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
apply(rule_tac y="b" in lam.exhaust)
--- a/Nominal/Ex/Let.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Let.thy Tue Aug 07 18:54:52 2012 +0100
@@ -115,7 +115,7 @@
| "height_trm (App l r) = max (height_trm l) (height_trm r)"
| "height_trm (Lam v b) = 1 + (height_trm b)"
| "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)"
- apply (simp only: eqvt_def height_trm_graph_def)
+ apply (simp only: eqvt_def height_trm_graph_aux_def)
apply (rule, perm_simp, rule, rule TrueI)
apply (case_tac x rule: trm_assn.exhaust(1))
apply (auto)[4]
@@ -169,7 +169,7 @@
| "subst s t (App l r) = App (subst s t l) (subst s t r)"
| "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)"
| "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (apply_assn2 (subst s t) as) (subst s t b)"
- apply (simp only: eqvt_def subst_graph_def)
+ apply (simp only: eqvt_def subst_graph_aux_def)
apply (rule, perm_simp, rule)
apply (rule TrueI)
apply (case_tac x)
--- a/Nominal/Ex/LetRec.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/LetRec.thy Tue Aug 07 18:54:52 2012 +0100
@@ -37,8 +37,8 @@
| "height_trm (Lam v b) = 1 + (height_trm b)"
| "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
| "height_bp (Bp v t) = height_trm t"
- apply (simp only: eqvt_def height_trm_height_bp_graph_def)
- apply (rule, perm_simp, rule, rule TrueI)
+ apply (simp add: eqvt_def height_trm_height_bp_graph_aux_def)
+ apply(rule TrueI)
using [[simproc del: alpha_set]]
apply auto
apply (case_tac x)
--- a/Nominal/Ex/Pi.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Pi.thy Tue Aug 07 18:54:52 2012 +0100
@@ -32,29 +32,9 @@
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(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)")
- unfolding eqvt_def
- apply(simp only: permute_fun_def)
- apply(rule allI)
- apply(rule ext)
- apply(rule ext)
- apply(simp only: permute_bool_def)
- apply(rule iffI)
- apply(drule_tac x="p" in meta_spec)
- apply(drule_tac x="- p \<bullet> x" in meta_spec)
- apply(drule_tac x="- p \<bullet> xa" in meta_spec)
- apply(simp)
- apply(drule_tac x="-p" in meta_spec)
- apply(drule_tac x="x" in meta_spec)
- apply(drule_tac x="xa" in meta_spec)
- apply(simp)
- apply(erule subst_name_list_graph.induct)
- apply(perm_simp)
- apply(rule subst_name_list_graph.intros)
- apply(perm_simp)
- apply(rule subst_name_list_graph.intros)
- apply(simp)
apply(rule_tac y="b" in list.exhaust)
by(auto)
@@ -181,97 +161,7 @@
| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
using [[simproc del: alpha_lst]]
apply(auto simp add: piMix_distinct piMix_eq_iff)
- apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")
- unfolding eqvt_def
- apply(rule allI)
- apply(simp only: permute_fun_def)
- apply(rule ext)
- apply(rule ext)
- apply(simp only: permute_bool_def)
- apply(rule iffI)
- apply(drule_tac x="p" in meta_spec)
- apply(drule_tac x="- p \<bullet> x" in meta_spec)
- apply(drule_tac x="- p \<bullet> xa" in meta_spec)
- apply(simp)
- apply(drule_tac x="-p" in meta_spec)
- apply(drule_tac x="x" in meta_spec)
- apply(drule_tac x="xa" in meta_spec)
- apply(simp)
- --"Equivariance"
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.induct)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testrr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(simp)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testrr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
- apply(simp)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testrr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(simp)
- apply(simp (no_asm_use) only: eqvts)
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testl)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(subst testlr)
- apply(rotate_tac 2)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(perm_simp)
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(blast)
- apply(blast)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testrr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
- apply(simp)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testrr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(subst testrr)
- apply(rotate_tac 2)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(perm_simp)
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(blast)
- apply(blast)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testrr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(blast)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testlr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(blast)
- apply(simp (no_asm_use) only: eqvts)
- apply(subst testrr)
- apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
- apply(blast)+
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
- apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
- apply(blast)
- apply(perm_simp)
- apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
+ apply(simp add: eqvt_def subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
--"Covered all cases"
apply(case_tac x)
apply(simp)
@@ -398,6 +288,99 @@
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
termination (eqvt)
--- a/Nominal/Ex/TypeSchemes1.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy Tue Aug 07 18:54:52 2012 +0100
@@ -80,8 +80,7 @@
where
"\<theta><Var X> = lookup \<theta> X"
| "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
- unfolding eqvt_def subst_graph_def
- apply (rule, perm_simp, rule)
+ apply(simp add: eqvt_def subst_graph_aux_def)
apply(rule TrueI)
apply(case_tac x)
apply(rule_tac y="b" in ty.exhaust)
@@ -119,8 +118,7 @@
substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
where
"fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
- unfolding eqvt_def substs_graph_def
- apply (rule, perm_simp, rule)
+ apply(simp add: eqvt_def substs_graph_aux_def)
apply auto[2]
apply (rule_tac y="b" and c="a" in tys.strong_exhaust)
apply auto[1]
@@ -279,10 +277,7 @@
where
"atom ` (fset Xs) \<sharp>* T \<Longrightarrow>
T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')"
-unfolding generalises_graph_def
-unfolding eqvt_def
-apply(perm_simp)
-apply(simp)
+apply(simp add: generalises_graph_aux_def eqvt_def)
apply(rule TrueI)
apply(case_tac x)
apply(simp)
@@ -409,8 +404,7 @@
where
"ftv (Var X) = {|X|}"
| "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)"
- unfolding eqvt_def ftv_graph_def
- apply (rule, perm_simp, rule)
+ apply(simp add: eqvt_def ftv_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in ty.exhaust)
apply(blast)
--- a/Nominal/Ex/TypeSchemes2.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy Tue Aug 07 18:54:52 2012 +0100
@@ -80,117 +80,7 @@
"subst \<theta> (Var X) = lookup \<theta> X"
| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
-(*unfolding subst_substs_graph_def eqvt_def
-apply rule
-apply perm_simp
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply rule*)
-thm subst_substs_graph.intros
-apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
-apply(simp add: eqvt_def)
-apply(rule allI)
-apply(simp add: permute_fun_def permute_bool_def)
-apply(rule ext)
-apply(rule ext)
-apply(rule iffI)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply(simp)
-apply(drule_tac x="-p" in meta_spec)
-apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="xa" in meta_spec)
-apply(simp)
---"Eqvt One way"
-apply(erule subst_substs_graph.induct)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp only: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp only: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp)
---"Eqvt done"
+apply(simp add: subst_substs_graph_aux_def eqvt_def)
apply(rule TrueI)
apply (case_tac x)
apply simp apply clarify
--- a/Nominal/Nominal2_Base.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Nominal2_Base.thy Tue Aug 07 18:54:52 2012 +0100
@@ -2099,7 +2099,7 @@
subsection {* Type @{typ "'a multiset"} is finitely supported *}
-lemma set_of_eqvt[eqvt]:
+lemma set_of_eqvt [eqvt]:
shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
by (induct M) (simp_all add: insert_eqvt empty_eqvt)
@@ -2886,7 +2886,7 @@
assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
-declare atom_eqvt[eqvt]
+declare atom_eqvt [eqvt]
class at = at_base +
assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
--- a/Nominal/nominal_function_core.ML Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/nominal_function_core.ML Tue Aug 07 18:54:52 2012 +0100
@@ -18,10 +18,15 @@
-> ((bstring * typ) list * term list * term * term) list (* specification *)
-> local_theory
-> (term (* f *)
+ * term (* G(raph) *)
+ * thm list (* GIntros *)
+ * thm (* Ginduct *)
* thm (* goalstate *)
* (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
) * local_theory
+ val inductive_def : (binding * typ) * mixfix -> term list -> local_theory
+ -> (term * thm list * thm * thm) * local_theory
end
structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE =
@@ -586,7 +591,7 @@
(* wrapper -- restores quantifiers in rule specifications *)
fun inductive_def (binding as ((R, T), _)) intrs lthy =
- let
+ let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
lthy
|> Local_Theory.conceal
@@ -1083,7 +1088,7 @@
termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]}
end
in
- ((f, goalstate, mk_partial_rules), lthy)
+ ((f, G, GIntro_thms, G_induct, goalstate, mk_partial_rules), lthy)
end
--- a/Nominal/nominal_mutual.ML Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/nominal_mutual.ML Tue Aug 07 18:54:52 2012 +0100
@@ -4,6 +4,8 @@
heavily based on the code of Alexander Krauss
(code forked on 14 January 2011)
+ Joachim Breitner helped with the auxiliary graph
+ definitions (7 August 2012)
Mutual recursive nominal function definitions.
*)
@@ -384,19 +386,114 @@
end
(* nominal *)
+fun subst_all s (Q $ Abs(_, _, t)) =
+ let
+ val vs = map Free (Term.add_frees s [])
+ in
+ fold Logic.all vs (subst_bound (s, t))
+ end
+
+fun mk_comp_dummy t s = Const (@{const_name comp}, dummyT) $ t $ s
+
+fun all v t =
+ let
+ val T = Term.fastype_of v
+ in
+ Logic.all_const T $ absdummy T (abstract_over (v, t))
+ end
+
+(* nominal *)
fun prepare_nominal_function_mutual config defname fixes eqss lthy =
let
val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =
analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
- val ((fsum, goalstate, cont), lthy') =
+ val ((fsum, G, GIntro_thms, G_induct, goalstate, cont), lthy') =
Nominal_Function_Core.prepare_nominal_function config defname [((n, T), NoSyn)] qglrs lthy
- val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
+ val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy'
val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
+
+ (* XXX *)
+
+ (* defining the auxiliary graph *)
+ fun mk_cases (MutualPart {i', fvar as (n, T), ...}) =
+ let
+ val (tys, ty) = strip_type T
+ val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty)
+ val inj_fun = absdummy dummyT (SumTree.mk_inj RST n' i' (Bound 0))
+ in
+ Syntax.check_term lthy'' (mk_comp_dummy inj_fun fun_var)
+ end
+
+ val sum_case_exp = map mk_cases parts
+ |> SumTree.mk_sumcases RST
+
+ val (G_name, G_type) = dest_Free G
+ val G_name_aux = G_name ^ "_aux"
+ val subst = [(G, Free (G_name_aux, G_type))]
+ val GIntros_aux = GIntro_thms
+ |> map prop_of
+ |> map (Term.subst_free subst)
+ |> map (subst_all sum_case_exp)
+
+ 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''
+
+ (* proof of equivalence between graph and auxiliary graph *)
+ val x = Var(("x", 0), ST)
+ val y = Var(("y", 1), RST)
+ val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y)
+ val G_prem = HOLogic.mk_Trueprop (G $ x $ y)
+
+ fun mk_inj_goal (MutualPart {i', ...}) =
+ let
+ val injs = SumTree.mk_inj ST n' i' (Bound 0)
+ val projs = y
+ |> SumTree.mk_proj RST n' i'
+ |> SumTree.mk_inj RST n' i'
+ in
+ Const (@{const_name "All"}, dummyT) $ absdummy dummyT
+ (HOLogic.mk_imp (HOLogic.mk_eq(x, injs), HOLogic.mk_eq(projs, y)))
+ end
+
+ val goal_inj = Logic.mk_implies (G_aux_prem,
+ HOLogic.mk_Trueprop (fold_conj (map mk_inj_goal parts)))
+ |> all x |> all y
+ |> Syntax.check_term lthy'''
+ val goal_iff1 = Logic.mk_implies (G_aux_prem, G_prem)
+ |> all x |> all y
+ val goal_iff2 = Logic.mk_implies (G_prem, G_aux_prem)
+ |> all x |> all y
+
+ val simp_thms = @{thms Projl.simps Projr.simps sum.inject sum.cases sum.distinct o_apply}
+ val ss0 = HOL_basic_ss addsimps simp_thms
+ val ss1 = HOL_ss 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 ss1)))
+
+ fun aux_tac thm =
+ rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (ss1 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
+ val iff2_thm = Goal.prove lthy''' [] [] goal_iff2
+ (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE (map (aux_tac o simplify ss0) GIntro_aux_thms))))
+ |> Drule.gen_all
+
+ 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]))))
+
+ val tac = HEADGOAL (simp_tac (HOL_basic_ss addsimps [iff_thm]))
+ val goalstate' =
+ case (SINGLE tac) goalstate of
+ NONE => error "auxiliary equivalence proof failed"
+ | SOME st => st
in
- ((goalstate, mutual_cont), lthy'')
+ ((goalstate', mutual_cont), lthy''')
end
end
--- a/Tutorial/Lambda.thy Tue Aug 07 18:53:50 2012 +0100
+++ b/Tutorial/Lambda.thy Tue Aug 07 18:54:52 2012 +0100
@@ -38,7 +38,7 @@
"height (Var x) = 1"
| "height (App t1 t2) = max (height t1) (height t2) + 1"
| "height (Lam [x].t) = height t + 1"
-apply(simp add: eqvt_def height_graph_def)
+apply(simp add: eqvt_def height_graph_aux_def)
apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
using [[simproc del: alpha_lst]]
@@ -59,8 +59,8 @@
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
- unfolding eqvt_def subst_graph_def
- apply(rule, perm_simp, rule)
+ unfolding eqvt_def subst_graph_aux_def
+ apply(simp)
apply(rule TrueI)
using [[simproc del: alpha_lst]]
apply(auto)