# HG changeset patch
# User urbanc
# Date 1133695557 -3600
# Node ID 18568b35035a839c2b5421c58647a4d616658d21
# Parent  c9be8266325f01971242de20b5d1f39fa86fe0e2
tuned

diff -r c9be8266325f -r 18568b35035a src/HOL/Nominal/Examples/Lam_substs.thy
--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Sun Dec 04 12:14:40 2005 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Sun Dec 04 12:25:57 2005 +0100
@@ -16,48 +16,37 @@
 
 section {* Strong induction principles for lam *}
 
-lemma lam_induct_aux:
+lemma lam_induct'[case_names Fin Var App Lam]:
   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>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)
-  have ih: "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by fact
-  show "\<And>(pi::name prm) x. P x (pi\<bullet>(Lam [a].t))"
-  proof (simp add: abs_perm)
-    fix x::"'a" and pi::"name prm"
-    have "\<exists>c::name. c\<sharp>(f x,pi\<bullet>a,pi\<bullet>t)"
-      by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 fs)
-    then obtain c::"name" 
-      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(f x)" and f3: "c\<sharp>(pi\<bullet>t)" 
-      by (force simp add: fresh_prod fresh_atm)
-    have "Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" using f1 f3
-      by (simp add: lam.inject alpha)
-    moreover
-    from ih have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>t)" by force
-    hence "\<And>x. P x ([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))" by (simp add: pt_name2[symmetric])
-    hence "P x (Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)))" using h3 f2
-      by (auto simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs])
-    ultimately show "P x (Lam [(pi\<bullet>a)].(pi\<bullet>t))" by simp
-  qed
-qed (auto intro: h1 h2)
-
-lemma lam_induct'[case_names Fin Var App Lam]: 
-  fixes P :: "'a \<Rightarrow> lam \<Rightarrow> bool"
-  and   x :: "'a"
-  and   t :: "lam"
-  and   f :: "'a \<Rightarrow> 'a"
-  assumes fs: "\<And>x. finite ((supp (f x))::name set)"
-  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)
+  shows "P x t"
+proof -
+  have "\<And>(pi::name prm) x. P x (pi\<bullet>t)"
+  proof (induct rule: lam.induct_weak)
+    case (Lam a t)
+    have ih: "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by fact
+    show "\<And>(pi::name prm) x. P x (pi\<bullet>(Lam [a].t))"
+    proof (simp add: abs_perm)
+      fix x::"'a" and pi::"name prm"
+      have "\<exists>c::name. c\<sharp>(f x,pi\<bullet>a,pi\<bullet>t)"
+	by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 fs)
+      then obtain c::"name" 
+	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(f x)" and f3: "c\<sharp>(pi\<bullet>t)" 
+	by (force simp add: fresh_prod fresh_atm)
+      have "Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" using f1 f3
+	by (simp add: lam.inject alpha)
+      moreover
+      from ih have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>t)" by force
+      hence "\<And>x. P x ([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))" by (simp add: pt_name2[symmetric])
+      hence "P x (Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)))" using h3 f2
+	by (auto simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs])
+      ultimately show "P x (Lam [(pi\<bullet>a)].(pi\<bullet>t))" by simp
+    qed
+  qed (auto intro: h1 h2)
   hence "P x (([]::name prm)\<bullet>t)" by blast
   thus "P x t" by simp
 qed
@@ -1373,7 +1362,7 @@
   and   t2:: "lam"
   and   a :: "name"
   shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
-apply(nominal_induct t1 fresh: b t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: b t2 rule: lam_induct)
 apply(auto simp add: perm_bij fresh_prod fresh_atm)
 apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*)
 apply(simp) 
@@ -1381,7 +1370,7 @@
 done
 
 lemma subst_supp: "supp(t1[a::=t2])\<subseteq>(((supp(t1)-{a})\<union>supp(t2))::name set)"
-apply(nominal_induct t1 fresh: a t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: a t2 rule: lam_induct)
 apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
 apply(blast)
 apply(blast)