# HG changeset patch
# User urbanc
# Date 1141311666 -3600
# Node ID fee0e93efa782545f27341f33baee54ff078a2f0
# Parent  ad36a9b42cf39ef21d56363eed2d7680dd1871de
fixed the bugs itroduced by the previous commit

diff -r ad36a9b42cf3 -r fee0e93efa78 src/HOL/Nominal/Examples/CR.thy
--- 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