--- a/Nominal/Ex/AuxNoFCB.thy Fri Mar 30 13:39:15 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy Fri Mar 30 13:56:36 2012 +0200
@@ -36,22 +36,14 @@
lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False"
apply (simp add: eqvt_def lam2_rec_graph_def)
apply (rule, perm_simp, rule, rule)
- defer
- apply (simp_all)[53]
- apply clarify
- apply metis
- apply simp
apply (case_tac x)
apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust)
apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
- apply simp_all[3]
- apply (metis, metis, metis)
+ apply simp_all[3] apply (metis, metis, metis)
apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
- apply simp_all[3]
- apply (metis, metis, metis)
+ apply simp_all[3] apply (metis, metis, metis)
apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust)
- apply simp_all[2]
- apply (metis, metis)
+ apply simp_all[2] apply (metis, metis)
apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P")
apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P")
apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P")
@@ -68,6 +60,7 @@
apply (drule_tac x="lam" in meta_spec)+
apply (drule_tac x="b" in meta_spec)+
apply (drule_tac x="a" in meta_spec)+
+ unfolding fresh_star_def
apply (case_tac "
(\<forall>x' y' t' s'.
atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
@@ -76,7 +69,7 @@
Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')
")
apply clarify
- apply (simp add: fresh_star_def)
+ apply (simp)
apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and>
atom namea \<sharp> (name, c, Lam [name]. lam) \<and>
(\<forall>x' y' t' s'.
@@ -86,7 +79,11 @@
Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s');
x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk>
\<Longrightarrow> P")
- apply (simp add: fresh_star_def)
+ apply (simp)
+ apply (simp_all)[53]
+ apply clarify
+ apply metis
+ apply simp
done
termination (eqvt) by lexicographic_order
@@ -109,7 +106,7 @@
fll name lam namea lama = fll x' t' y' s')")
apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
- using Abs1_eq_iff lam.eq_iff apply metis
+ apply metis
apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
apply rule
@@ -222,36 +219,6 @@
apply lexicographic_order
done
-lemma foldr_eqvt[eqvt]:
- "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
- apply (induct b)
- apply simp_all
- apply (perm_simp)
- apply simp
- done
-
-nominal_primrec
- subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90)
-where
- "(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)
- apply(rule TrueI)
- apply(auto)
- apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
- apply(blast)+
- apply(simp_all add: fresh_star_def fresh_Pair_elim)
- apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
- apply(simp_all add: Abs_fresh_iff)
- apply(simp add: fresh_star_def fresh_Pair)
- apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
- apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-done
-
-termination (eqvt) by lexicographic_order
-
nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
"swapequal l r [] \<longleftrightarrow> l = r"
| "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow>
@@ -310,6 +277,7 @@
apply (subgoal_tac "ab \<noteq> (b \<leftrightarrow> aba) \<bullet> m")
apply simp
by (metis (lifting) permute_flip_at)
+
lemma var_neq_swapequal2: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs"
apply (induct xs arbitrary: m)
apply simp
@@ -326,7 +294,6 @@
apply simp
by (metis (lifting) permute_flip_at)
-
lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs"
apply (induct xs arbitrary: m n)
apply simp
@@ -358,8 +325,6 @@
apply (subst swapequal.simps)
apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1]
apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t")
- prefer 2
- apply (simp add: flip_at_base_simps fresh_at_base flip_def)
apply (subst swapequal.simps)
apply (simp add: fresh_Pair fresh_Cons fresh_permute_left)
apply rule apply assumption
@@ -372,15 +337,15 @@
apply (subst swapequal.simps)
apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left)
apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t")
- prefer 2
+ apply rule apply assumption
apply (simp add: flip_at_base_simps fresh_at_base flip_def)
- apply rule apply assumption
apply (simp add: flip_at_base_simps fresh_at_base flip_def)
apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t")
apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s")
apply simp
apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
+ apply (simp add: flip_at_base_simps fresh_at_base flip_def)
done
lemma swapequal_lambda:
@@ -482,7 +447,7 @@
apply simp
done
-lemma
+lemma aux_is_alpha:
"aux x y [] \<longleftrightarrow> (x = y)"
by (simp_all add: supp_Nil aux_alphaish)