# HG changeset patch
# User urbanc
# Date 1133359395 -3600
# Node ID f7899cb24c7949bb1e1318211fab551bd05401b3
# Parent  116fe71fad515c0033e7752644b42ee18d490d4f
changed induction principle and everything to conform with the
new nominal_induct

diff -r 116fe71fad51 -r f7899cb24c79 src/HOL/Nominal/Examples/Lam_substs.thy
--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Nov 30 14:27:50 2005 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Nov 30 15:03:15 2005 +0100
@@ -20,9 +20,9 @@
   fixes P :: "'a \<Rightarrow> lam \<Rightarrow> bool"
   and   f :: "'a \<Rightarrow> 'a"
   assumes fs: "\<And>x. finite ((supp (f x))::name set)"
-      and h1: "\<And>x a. P x (Var  a)"  
-      and h2: "\<And>x t1 t2. (\<And>z. P z t1) \<Longrightarrow> (\<And>z. P z t2) \<Longrightarrow> P x (App t1 t2)" 
-      and h3: "\<And>x a t. a\<sharp>f x \<Longrightarrow> (\<And>z. P z t) \<Longrightarrow> P x (Lam [a].t)"
+      and h1: "\<And>a x. P x (Var  a)"  
+      and h2: "\<And>t1 t2 x. (\<And>z. P z t1) \<Longrightarrow> (\<And>z. P z t2) \<Longrightarrow> P x (App t1 t2)" 
+      and h3: "\<And>a t x. a\<sharp>f x \<Longrightarrow> (\<And>z. P z t) \<Longrightarrow> P x (Lam [a].t)"
   shows "\<And>(pi::name prm) x. P x (pi\<bullet>t)"
 proof (induct rule: lam.induct_weak)
   case (Lam a t)
@@ -52,9 +52,9 @@
   and   t :: "lam"
   and   f :: "'a \<Rightarrow> 'a"
   assumes fs: "\<And>x. finite ((supp (f x))::name set)"
-  and     h1: "\<And>x a. P x (Var  a)" 
-  and     h2: "\<And>x t1 t2. (\<And>z. P z t1)\<Longrightarrow>(\<And>z. P z t2)\<Longrightarrow>P x (App t1 t2)" 
-  and     h3: "\<And>x a t. a\<sharp>f x \<Longrightarrow> (\<And>z. P z t)\<Longrightarrow> P x (Lam [a].t)"
+  and     h1: "\<And>a x. P x (Var  a)" 
+  and     h2: "\<And>t1 t2 x. (\<And>z. P z t1)\<Longrightarrow>(\<And>z. P z t2)\<Longrightarrow>P x (App t1 t2)" 
+  and     h3: "\<And>a t x. a\<sharp>f x \<Longrightarrow> (\<And>z. P z t)\<Longrightarrow> P x (Lam [a].t)"
   shows  "P x t"
 proof - 
   from fs h1 h2 h3 have "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by (rule lam_induct_aux, auto)
@@ -66,9 +66,9 @@
   fixes P :: "('a::fs_name) \<Rightarrow> lam \<Rightarrow> bool"
   and   x :: "'a::fs_name"
   and   t :: "lam"
-  assumes h1: "\<And>x a. P x (Var  a)" 
-  and     h2: "\<And>x t1 t2. (\<And>z. P z t1)\<Longrightarrow>(\<And>z. P z t2)\<Longrightarrow>P x (App t1 t2)" 
-  and     h3: "\<And>x a t. a\<sharp>x \<Longrightarrow> (\<And>z. P z t)\<Longrightarrow> P x (Lam [a].t)"
+  assumes h1: "\<And>a x. P x (Var  a)" 
+  and     h2: "\<And>t1 t2 x. (\<And>z. P z t1)\<Longrightarrow>(\<And>z. P z t2)\<Longrightarrow>P x (App t1 t2)" 
+  and     h3: "\<And>a t x. a\<sharp>x \<Longrightarrow> (\<And>z. P z t)\<Longrightarrow> P x (Lam [a].t)"
   shows  "P x t"
 apply(rule lam_induct'[of "\<lambda>x. x" "P"])
 apply(simp add: fs_name1)
@@ -231,7 +231,7 @@
   and   f3 ::"('a::pt_name) f3_ty"
   and   t  ::"lam"
   and   y  ::"name prm \<Rightarrow> ('a::pt_name)"
-  shows "(t,y)\<in>rec f1 f2 f3 \<Longrightarrow> (\<forall>(pi1::name prm) (pi2::name prm). pi1 \<sim> pi2 \<longrightarrow> (y pi1 = y pi2))"
+  shows "(t,y)\<in>rec f1 f2 f3 \<Longrightarrow> (\<forall>(pi1::name prm) (pi2::name prm). pi1 \<triangleq> pi2 \<longrightarrow> (y pi1 = y pi2))"
 apply(erule rec.induct)
 apply(auto simp add: pt3[OF pt_name_inst])
 apply(rule_tac f="fresh_fun" in arg_cong)
@@ -385,7 +385,7 @@
 	fix a'::"name"
 	have "(y ((pi@[(pi1\<bullet>c,a')])@pi1)) =  (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" 
 	  proof -
-	    have "((pi@[(pi1\<bullet>c,a')])@pi1) \<sim> ((pi@pi1)@[(c,(rev pi1)\<bullet>a')])"
+	    have "((pi@[(pi1\<bullet>c,a')])@pi1) \<triangleq> ((pi@pi1)@[(c,(rev pi1)\<bullet>a')])"
 	    by (force simp add: prm_eq_def at_append[OF at_name_inst] 
                    at_calc[OF at_name_inst] at_bij[OF at_name_inst] 
                    at_pi_rev[OF at_name_inst] at_rev_pi[OF at_name_inst])
@@ -543,7 +543,7 @@
 	  by (simp only: rec_perm_rev[OF f, OF c])
 	hence g2: "(t, \<lambda>pi2. y'' (pi2@([(a,d)]@[(a,c)])))\<in>rec f1 f2 f3" by simp
 	have "distinct [a,c,d]" using i9 f4 f5 by force
-	hence g3: "(pi@[(c,d)]@[(a,d)]@[(a,c)]) \<sim> (pi@[(a,d)])"
+	hence g3: "(pi@[(c,d)]@[(a,d)]@[(a,c)]) \<triangleq> (pi@[(a,d)])"
 	  by (force simp add: prm_eq_def at_calc[OF at_name_inst] at_append[OF at_name_inst])
 	have "fresh_fun ?g = ?g d" using r1 c1 f1
 	  by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
@@ -926,7 +926,6 @@
   and     a2: "\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)" 
   and     a3: "\<forall>a t. a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)"
   shows "fun t = rfun f1 f2 f3 t"
-(*apply(nominal_induct t rule: lam_induct')*)
 apply (rule lam_induct'[of "\<lambda>_. (f1,f2,f3)" "\<lambda>_ t. fun t = rfun f1 f2 f3 t"])
 (* finite support *)
 apply(rule f)
@@ -1167,13 +1166,6 @@
 apply(simp add: rfun_gen_def)
 done
 
-(* FIXME: this should be automatically proved in nominal_atoms *)
-
-instance nat :: pt_name
-apply(intro_classes)
-apply(simp_all add: perm_nat_def)
-done
-
 constdefs 
   depth_Var :: "name \<Rightarrow> nat"
   "depth_Var \<equiv> \<lambda>(a::name). 1"
@@ -1372,17 +1364,15 @@
   and   t2:: "lam"
   and   a :: "name"
   shows "pi\<bullet>(t1[a::=t2]) = (pi\<bullet>t1)[(pi\<bullet>a)::=(pi\<bullet>t2)]"
-thm lam_induct
-apply(nominal_induct t1 rule: lam_induct)
-apply(auto)
+apply(nominal_induct t1 fresh: a t2 rule: lam_induct)
 apply(auto simp add: perm_bij fresh_prod fresh_atm)
-apply(subgoal_tac "(aa\<bullet>ab)\<sharp>(aa\<bullet>a,aa\<bullet>b)")(*A*)
+apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>ba)")(*A*)
 apply(simp) 
 apply(simp add: perm_bij fresh_prod fresh_atm pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) 
 done
 
 lemma subst_supp: "supp(t1[a::=t2])\<subseteq>(((supp(t1)-{a})\<union>supp(t2))::name set)"
-apply(nominal_induct t1 rule: lam_induct)
+apply(nominal_induct t1 fresh: a t2 rule: lam_induct)
 apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
 apply(blast)
 apply(blast)