# HG changeset patch
# User urbanc
# Date 1199435651 -3600
# Node ID 7711d60a5293d5312080b349302e7512d5490de7
# Parent  8fbc7d38d6cf9f9eebf4850eef5971cd29acb78a
adapted to new inversion rules

diff -r 8fbc7d38d6cf -r 7711d60a5293 src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Fri Jan 04 09:34:11 2008 +0100
@@ -265,66 +265,29 @@
    (auto simp add: calc_atm fresh_atm abs_fresh)
 
 lemma one_abs: 
-  fixes    t :: "lam"
-  and      t':: "lam"
-  and      a :: "name"
-  assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
+  assumes a: "Lam [a].t\<longrightarrow>\<^isub>1t'"
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
-  using a
-  apply -
-  apply(ind_cases "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
-  apply(auto simp add: lam.inject alpha)
-  apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
-  apply(rule conjI)
-  apply(perm_simp)
-  apply(simp add: fresh_left calc_atm)
-  apply(simp add: One.eqvt)
-  apply(simp add: one_fresh_preserv)
-done  
-
+proof -
+  have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
+  with a have "a\<sharp>t'" by (simp add: one_fresh_preserv)
+  with a show ?thesis
+    by (cases rule: One.strong_cases[where a="a" and aa="a"])
+       (auto simp add: lam.inject abs_fresh alpha)
+qed
 
 lemma one_app: 
   assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
   shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
-         (\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
-  using a
-  apply -
-  apply(ind_cases "App t1 t2 \<longrightarrow>\<^isub>1 t'")
-  apply(auto simp add: lam.distinct lam.inject)
-  done
+         (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2 \<and> a\<sharp>(t2,s2))"
+using a by (erule_tac One.cases) (auto simp add: lam.inject)
 
 lemma one_red: 
-  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M"
+  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M" "a\<sharp>(t2,M)"
   shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
          (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
-  using a
-  apply -
-  apply(ind_cases "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
-  apply(simp_all add: lam.inject)
-  apply(force)
-  apply(erule conjE)
-  apply(drule sym[of "Lam [a].t1"])
-  apply(simp)
-  apply(drule one_abs)
-  apply(erule exE)
-  apply(simp)
-  apply(force simp add: alpha)
-  apply(erule conjE)
-  apply(simp add: lam.inject alpha)
-  apply(erule disjE)
-  apply(simp)
-  apply(force)
-  apply(simp)
-  apply(rule disjI2)
-  apply(rule_tac x="[(a,aa)]\<bullet>t2a" in exI)
-  apply(rule_tac x="s2" in exI)
-  apply(auto)
-  apply(subgoal_tac "a\<sharp>t2a")(*A*)
-  apply(simp add: subst_rename)
-  (*A*)
-  apply(force intro: one_fresh_preserv)
-  apply(force intro: One.eqvt)
-  done
+using a
+by (cases rule: One.strong_cases [where a="a" and aa="a"])
+   (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod)
 
 text {* first case in Lemma 3.2.4*}
 
@@ -347,9 +310,8 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-apply(nominal_induct M avoiding: x N N' rule: lam.induct)
-apply(auto simp add: fresh_prod fresh_atm)
-done
+by (nominal_induct M avoiding: x N N' rule: lam.induct)
+   (auto simp add: fresh_prod fresh_atm)
 
 lemma one_subst: 
   assumes a: "M\<longrightarrow>\<^isub>1M'"
@@ -385,9 +347,8 @@
   and     b: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
 using a b
-apply(nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
-apply(auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
-done
+by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
+   (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
 
 lemma diamond[rule_format]:
   fixes    M :: "lam"
@@ -401,12 +362,12 @@
   thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and>  M2\<longrightarrow>\<^isub>1M3" by blast
 next
   case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
-  have vc: "x\<sharp>Q" "x\<sharp>Q'" by fact+
+  have vc: "x\<sharp>Q" "x\<sharp>Q'" "x\<sharp>M2" by fact+
   have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact
   hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q') \<or> 
-         (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" by (simp add: one_red)
+         (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" using vc by (simp add: one_red)
   moreover (* subcase 2.1 *)
   { assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
     then obtain P'' and Q'' where 
@@ -446,7 +407,7 @@
   have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
   assume "App P Q \<longrightarrow>\<^isub>1 M2"
   hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q'') \<or> 
-         (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> x\<sharp>(Q,Q') \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q')" 
+         (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q' \<and> x\<sharp>(Q,Q'))" 
     by (simp add: one_app[simplified])
   moreover (* subcase 3.1 *)
   { assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
@@ -463,11 +424,11 @@
     hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
   }
   moreover (* subcase 3.2 *)
-  { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> x\<sharp>(Q,Q'') \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+  { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q'' \<and> x\<sharp>(Q,Q'')"
     then obtain x P1 P1'' Q'' where
       b0: "P = Lam [x].P1" and b1: "M2 = P1''[x::=Q'']" and 
       b2: "P1\<longrightarrow>\<^isub>1P1''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" and vc: "x\<sharp>(Q,Q'')" by blast
-    from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)
+    from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)      
     then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by blast 
     from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp
     then obtain P1''' where
diff -r 8fbc7d38d6cf -r 7711d60a5293 src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Jan 04 09:34:11 2008 +0100
@@ -63,6 +63,7 @@
 using a by (nominal_induct t avoiding: x y s u rule: lam.induct)
            (auto simp add: fresh_fact forget)
 
+
 lemma subst_rename: 
   assumes a: "y\<sharp>t"
   shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]"
@@ -124,48 +125,31 @@
   finally show "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2[x::=s2]" by simp
 qed
 
-lemma One_preserves_fresh:
-  fixes x :: "name"
-  assumes a: "t \<longrightarrow>\<^isub>1 s" 
-  shows "x\<sharp>t \<Longrightarrow> x\<sharp>s"
-using a by (nominal_induct t s avoiding: x rule: One.strong_induct)
-           (auto simp add: abs_fresh fresh_atm fresh_fact)
-
 lemma One_Var:
   assumes a: "Var x \<longrightarrow>\<^isub>1 M"
   shows "M = Var x"
 using a by (erule_tac One.cases) (simp_all) 
 
 lemma One_Lam: 
-  assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s"
+  assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s" "x\<sharp>s"
   shows "\<exists>t'. s = Lam [x].t' \<and> t \<longrightarrow>\<^isub>1 t'"
 using a
-  apply(erule_tac One.cases)
-  apply(auto simp add: lam.inject alpha)
-  apply(rule_tac x="[(x,xa)]\<bullet>t2" in exI)
-  apply(perm_simp add: fresh_left calc_atm One.eqvt One_preserves_fresh)
-done  
+by (cases rule: One.strong_cases[where x="x" and xa="x"])
+   (auto simp add: lam.inject abs_fresh alpha)
 
 lemma One_App: 
   assumes a: "App t s \<longrightarrow>\<^isub>1 r"
   shows "(\<exists>t' s'. r = App t' s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> 
          (\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^isub>1 p' \<and> s \<longrightarrow>\<^isub>1 s' \<and> x\<sharp>(s,s'))" 
-using a by (erule_tac One.cases) 
-           (auto simp add: lam.inject)
+using a by (erule_tac One.cases) (auto simp add: lam.inject)
 
 lemma One_Redex: 
-  assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r"
+  assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r" "x\<sharp>(s,r)"
   shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> 
          (\<exists>t' s'. r = t'[x::=s'] \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s')" 
 using a
-apply(erule_tac One.cases, simp_all)
-apply(auto dest: One_Lam simp add: lam.inject)[1] 
-apply(rule disjI2)
-apply(auto simp add: lam.inject alpha)
-apply(rule_tac x="[(x,xa)]\<bullet>t2" in exI)
-apply(rule_tac x="s2" in exI)
-apply(simp add: subst_rename One_preserves_fresh One.eqvt)
-done
+by (cases rule: One.strong_cases [where x="x" and xa="x"])
+   (auto dest: One_Lam simp add: lam.inject abs_fresh alpha fresh_prod)
 
 section {* Transitive Closure of One *}
 
@@ -186,11 +170,9 @@
 | d3[intro]: "\<lbrakk>\<not>(\<exists>y t'. t1 = Lam [y].t'); t1 \<longrightarrow>\<^isub>d t2; s1 \<longrightarrow>\<^isub>d s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>\<^isub>d App t2 s2"
 | d4[intro]: "\<lbrakk>x\<sharp>(s1,s2); t1 \<longrightarrow>\<^isub>d t2; s1 \<longrightarrow>\<^isub>d s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>\<^isub>d t2[x::=s2]"
 
-(* FIXME: needs to be in nominal_inductive *)
-declare perm_pi_simp[eqvt_force]
-
 equivariance Dev
-nominal_inductive Dev by (simp_all add: abs_fresh fresh_fact')
+nominal_inductive Dev 
+  by (simp_all add: abs_fresh fresh_fact')
 
 lemma better_d4_intro:
   assumes a: "t1 \<longrightarrow>\<^isub>d t2" "s1 \<longrightarrow>\<^isub>d s2"
@@ -208,17 +190,19 @@
   fixes x::"name"
   assumes a: "M\<longrightarrow>\<^isub>d N"  
   shows "x\<sharp>M \<Longrightarrow> x\<sharp>N"
-using a by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
+using a 
+by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
 
 lemma Dev_Lam:
-  assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N"
+  assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N" 
   shows "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>\<^isub>d N'"
-using a
-apply(erule_tac Dev.cases)
-apply(auto simp add: lam.inject alpha)
-apply(rule_tac x="[(x,xa)]\<bullet>s" in exI)
-apply(perm_simp add: fresh_left Dev.eqvt Dev_preserves_fresh)
-done
+proof -
+  from a have "x\<sharp>Lam [x].M" by (simp add: abs_fresh)
+  with a have "x\<sharp>N" by (simp add: Dev_preserves_fresh)
+  with a show ?thesis
+    by (cases rule: Dev.strong_cases [where x="x" and xa="x"])
+       (auto simp add: lam.inject abs_fresh alpha)
+qed
 
 lemma Development_existence:
   shows "\<exists>M'. M \<longrightarrow>\<^isub>d M'"
@@ -228,9 +212,13 @@
 lemma Triangle:
   assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2"
   shows "t2 \<longrightarrow>\<^isub>1 t1"
-using a by (nominal_induct avoiding: t2 rule: Dev.strong_induct)
-                   (auto dest!: One_Var One_App One_Redex One_Lam intro: One_subst)
-(* Remark: we could here get away with a normal induction and appealing to One_preserves_fresh *)
+using a 
+apply(nominal_induct avoiding: t2 rule: Dev.strong_induct)
+apply(auto dest!: One_Var)[1]
+apply(auto dest!: One_Lam)[1]
+apply(auto dest!: One_App)[1]
+apply(auto dest!: One_Redex intro: One_subst)[1]
+done
 
 lemma Diamond_for_One:
   assumes a: "t \<longrightarrow>\<^isub>1 t1" "t \<longrightarrow>\<^isub>1 t2"
diff -r 8fbc7d38d6cf -r 7711d60a5293 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Fri Jan 04 09:34:11 2008 +0100
@@ -71,33 +71,25 @@
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
-lemma supp_beta: 
+lemma beta_preserves_fresh: 
+  fixes a::"name"
   assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
-  shows "(supp s)\<subseteq>((supp t)::name set)"
+  shows "a\<sharp>t \<Longrightarrow> a\<sharp>s"
 using a
-by (induct)
-   (auto intro!: simp add: abs_supp lam.supp subst_supp)
+apply(nominal_induct t s avoiding: a rule: Beta.strong_induct)
+apply(auto simp add: abs_fresh fresh_fact fresh_atm)
+done
 
 lemma beta_abs: 
-  assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'"
+  assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'" 
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
-using a
-apply -
-apply(ind_cases "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)
-apply(rule conjI)
-apply(rule sym)
-apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
-apply(simp)
-apply(rule pt_name3)
-apply(simp add: at_ds5[OF at_name_inst])
-apply(rule conjI)
-apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
-apply(force dest!: supp_beta simp add: fresh_def)
-apply(force intro!: eqvts)
-done
+proof -
+  have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
+  with a have "a\<sharp>t'" by (simp add: beta_preserves_fresh)
+  with a show ?thesis
+    by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
+       (auto simp add: lam.inject abs_fresh alpha)
+qed
 
 lemma beta_subst: 
   assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"