--- a/src/HOL/Nominal/Examples/CR.thy Thu Mar 02 15:43:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy Thu Mar 02 16:01:06 2006 +0100
@@ -249,79 +249,6 @@
thus ?thesis by simp
qed
-lemma beta_induct_aux:
- fixes P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool"
- and t :: "lam"
- and s :: "lam"
- and x :: "'a::fs_name"
- assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
- and a1: "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App s1 t) (App s2 t)"
- and a2: "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App t s1) (App t s2)"
- and a3: "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
- and a4: "\<And>a t1 s1 x. a\<sharp>(x,s1) \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
- and eq: "\<And>(pi::name prm) x t s. P x t s \<Longrightarrow> P (pi\<bullet>x) (pi\<bullet>t) (pi\<bullet>s)"
- shows "P x t s"
-using a
-proof (induct fixing: x)
- case b1 thus ?case using a1 by blast
- next
- case b2 thus ?case using a2 by blast
- next
- case (b3 a s1 s2)
- have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
- have j2: "\<And>x. P x s1 s2" by fact
- show ?case
- proof -
- have f: "\<exists>c::name. c\<sharp>(a,s1,s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
- then obtain c::"name"
- where f1: "c\<noteq>a" and f2: "c\<sharp>x" and f3: "c\<sharp>s1" and f4: "c\<sharp>s2"
- by (force simp add: fresh_prod fresh_atm)
- have x1: "([(c,a)]\<bullet>s1) \<longrightarrow>\<^isub>\<beta> ([(c,a)]\<bullet>s2)" using j1 by (rule eqvt_beta)
- have x2: "\<And>x. P x ([(c,a)]\<bullet>s1) ([(c,a)]\<bullet>s2)" using j2 eq
- apply -
- apply(drule_tac x="[(c,a)]\<bullet>x" in meta_spec)
- apply(drule_tac x="[(c,a)]\<bullet>x" in meta_spec)
- apply(drule_tac x="s1" in meta_spec)
- apply(drule_tac x="s2" in meta_spec)
- apply(drule_tac x="[(c,a)]" in meta_spec)
- apply(simp add: perm_swap)
- done
- have x: "P x (Lam [c].([(c,a)]\<bullet>s1)) (Lam [c].([(c,a)]\<bullet>s2))"
- using a3 f2 x1 x2 by blast
- have alpha1: "(Lam [c].([(c,a)]\<bullet>s1)) = (Lam [a].s1)" using f1 f3
- by (simp add: lam.inject alpha)
- have alpha2: "(Lam [c].([(c,a)]\<bullet>s2)) = (Lam [a].s2)" using f1 f3
- by (simp add: lam.inject alpha)
- show " P x (Lam [a].s1) (Lam [a].s2)"
- using x alpha1 alpha2 by (simp only: pt_name2)
- qed
- next
- case (b4 a s1 s2)
- show ?case
- proof -
- have f: "\<exists>c::name. c\<sharp>(a,s1,s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
- then obtain c::"name"
- where f1: "c\<noteq>a" and f2: "c\<sharp>x" and f3: "c\<sharp>s1" and f4: "c\<sharp>s2" and f5: "c\<sharp>(x,s2)"
- by (force simp add: fresh_prod fresh_atm)
- have x: "P x (App (Lam [c].([(c,a)]\<bullet>s1)) s2) (([(c,a)]\<bullet>s1)[c::=s2])"
- using a4 f5
- (* HERE *)
-
- by (blast intro!: eqvt_beta)
- have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
- by (simp add: lam.inject alpha)
- have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
- using f3 by (simp only: subst_rename[symmetric] pt_name2)
- show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
- using x alpha1 alpha2 by (simp only: pt_name2)
- qed
- qed
- hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast
- thus ?thesis by simp
-qed
-
section {* One-Reduction *}
consts