diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -45,21 +45,16 @@
 apply(simp_all add: fresh_atm)
 done
 
-consts
-  Beta :: "(lam\<times>lam) set"
-syntax 
-  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
-  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
-translations 
-  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
-  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
-inductive Beta
-  intros
+inductive2 Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+where
   b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
-  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
-  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
-  b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
+| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
+| b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
 
+abbreviation "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) where
+  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2 \<equiv> Beta\<^sup>*\<^sup>* t1 t2"
+ 
 lemma eqvt_beta: 
   fixes pi :: "name prm"
   and   t  :: "lam"
@@ -86,7 +81,7 @@
   next
     case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
   next
-    case (b3 a s1 s2)
+    case (b3 s1 s2 a)
     have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
     have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
     show ?case 
@@ -137,7 +132,7 @@
 
 
 lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
-apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
 apply(auto simp add: lam.distinct lam.inject)
 apply(auto simp add: alpha)
 apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
@@ -201,15 +196,10 @@
   "dom_ty []    = []"
   "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 
 
-consts
-  ctxts :: "((name\<times>ty) list) set" 
-  valid :: "(name\<times>ty) list \<Rightarrow> bool"
-translations
-  "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
-inductive ctxts
-intros
-v1[intro]: "valid []"
-v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
+inductive2 valid :: "(name\<times>ty) list \<Rightarrow> bool"
+where
+  v1[intro]: "valid []"
+| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
 
 lemma valid_eqvt:
   fixes   pi:: "name prm"
@@ -238,7 +228,7 @@
   and    a :: "name"
   and    \<tau> :: "ty"
   shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
-apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
+apply(ind_cases2 "valid ((a,\<tau>)#\<Gamma>)", simp)
 done
 
 lemma valid_unicity[rule_format]: 
@@ -251,18 +241,11 @@
 apply(auto dest!: valid_elim fresh_context)
 done
 
-consts
-  typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
-syntax
-  "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
-translations
-  "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
-
-inductive typing
-intros
-t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
-t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
-t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
+inductive2 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+where
+  t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
+| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
+| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
 
 lemma eqvt_typing: 
   fixes  \<Gamma> :: "(name\<times>ty) list"
@@ -273,14 +256,14 @@
   shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
 using a
 proof (induct)
-  case (t1 \<Gamma> \<tau> a)
+  case (t1 \<Gamma> a \<tau>)
   have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
   moreover
   have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
     using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
 next 
-  case (t3 \<Gamma> \<sigma> \<tau> a t)
+  case (t3 a \<Gamma> \<tau> t \<sigma>)
   moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
 qed (auto)
@@ -302,7 +285,7 @@
 proof -
   from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
   proof (induct)
-    case (t1 \<Gamma> \<tau> a)
+    case (t1 \<Gamma> a \<tau>)
     have j1: "valid \<Gamma>" by fact
     have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact
     from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
@@ -310,10 +293,10 @@
     hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
     show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp
   next
-    case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
+    case (t2 \<Gamma> t1 \<tau> \<sigma> t2)
     thus ?case using a2 by (simp, blast intro: eqvt_typing)
   next
-    case (t3 \<Gamma> \<sigma> \<tau> a t)
+    case (t3 a \<Gamma> \<tau> t \<sigma>)
     have k1: "a\<sharp>\<Gamma>" by fact
     have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
     have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
@@ -375,17 +358,17 @@
 done
 
 lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
-apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
+apply(ind_cases2 "\<Gamma> \<turnstile> Var a : \<tau>")
 apply(auto simp add: lam.inject lam.distinct)
 done
 
 lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
-apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
+apply(ind_cases2 "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
 apply(auto simp add: lam.inject lam.distinct)
 done
 
 lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
-apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
+apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
 apply(auto simp add: lam.distinct lam.inject alpha) 
 apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing)
 apply(simp)
@@ -534,7 +517,7 @@
 
 constdefs
   "SN" :: "lam \<Rightarrow> bool"
-  "SN t \<equiv> t\<in>termi Beta"
+  "SN t \<equiv> termi Beta t"
 
 lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
 apply(simp add: SN_def)
@@ -561,30 +544,24 @@
   "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
 
 (* a slight hack to get the first element of applications *)
-consts
-  FST :: "(lam\<times>lam) set"
-syntax 
-  "FST_judge"   :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
-translations 
-  "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
-inductive FST
-  intros
+inductive2 FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
+where
 fst[intro!]:  "(App t s) \<guillemotright> t"
 
 lemma fst_elim[elim!]: 
   shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
-apply(ind_cases "App t s \<guillemotright> t'")
+apply(ind_cases2 "App t s \<guillemotright> t'")
 apply(simp add: lam.inject)
 done
 
 lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
 apply(simp add: SN_def)
-apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
+apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> termi Beta z")(*A*)
 apply(force)
 (*A*)
 apply(erule acc_induct)
 apply(clarify)
-apply(ind_cases "x \<guillemotright> z")
+apply(ind_cases2 "x \<guillemotright> z" for x z)
 apply(clarify)
 apply(rule accI)
 apply(auto intro: b1)
@@ -626,7 +603,7 @@
 apply(force simp only: NEUT_def)
 apply(simp (no_asm) add: CR3_RED_def)
 apply(clarify)
-apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "App t x \<longrightarrow>\<^isub>\<beta> t'" for x t t')
 apply(simp_all add: lam.inject)
 apply(simp only:  CR3_RED_def)
 apply(drule_tac x="s2" in spec)
@@ -701,21 +678,21 @@
 qed
     
 lemma double_acc_aux:
-  assumes a_acc: "a \<in> acc r"
-  and b_acc: "b \<in> acc r"
+  assumes a_acc: "acc r a"
+  and b_acc: "acc r b"
   and hyp: "\<And>x z.
-    (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
-    (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
-    (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
-    (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
+    (\<And>y. r y x \<Longrightarrow> acc r y) \<Longrightarrow>
+    (\<And>y. r y x \<Longrightarrow> P y z) \<Longrightarrow>
+    (\<And>u. r u z \<Longrightarrow> acc r u) \<Longrightarrow>
+    (\<And>u. r u z \<Longrightarrow> P x u) \<Longrightarrow> P x z"
   shows "P a b"
 proof -
   from a_acc
-  have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
+  have r: "\<And>b. acc r b \<Longrightarrow> P a b"
   proof (induct a rule: acc.induct)
     case (accI x)
     note accI' = accI
-    have "b \<in> acc r" .
+    have "acc r b" .
     thus ?case
     proof (induct b rule: acc.induct)
       case (accI y)
@@ -734,7 +711,7 @@
 qed
 
 lemma double_acc:
-  "\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"
+  "\<lbrakk>acc r a; acc r b; \<forall>x z. ((\<forall>y. r y x \<longrightarrow> P y z) \<and> (\<forall>u. r u z \<longrightarrow> P x u)) \<longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
 apply(rule_tac r="r" in double_acc_aux)
 apply(assumption)+
 apply(blast)
@@ -743,7 +720,7 @@
 lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
 apply(simp)
 apply(clarify)
-apply(subgoal_tac "t\<in>termi Beta")(*1*)
+apply(subgoal_tac "termi Beta t")(*1*)
 apply(erule rev_mp)
 apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
 apply(erule rev_mp)
@@ -764,7 +741,7 @@
 apply(force simp add: NEUT_def)
 apply(simp add: CR3_RED_def)
 apply(clarify)
-apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'" for xa z t')
 apply(auto simp add: lam.inject lam.distinct)
 apply(drule beta_abs)
 apply(auto)
@@ -813,7 +790,7 @@
 apply(force simp add: NEUT_def)
 apply(simp add: NORMAL_def)
 apply(clarify)
-apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "Var x \<longrightarrow>\<^isub>\<beta> t'" for t')
 apply(auto simp add: lam.inject lam.distinct)
 apply(force simp add: RED_props)
 apply(simp add: id_subs)