# HG changeset patch
# User urbanc
# Date 1141836951 -3600
# Node ID 5caacd449ea49749a0b6c98f97e71de37fa06db0
# Parent  a45baf1ac094e3f5ec29c238fd7673f03e725415
tuned some proofs

diff -r a45baf1ac094 -r 5caacd449ea4 src/HOL/Nominal/Examples/Iteration.thy
--- a/src/HOL/Nominal/Examples/Iteration.thy	Wed Mar 08 17:54:55 2006 +0100
+++ b/src/HOL/Nominal/Examples/Iteration.thy	Wed Mar 08 17:55:51 2006 +0100
@@ -142,7 +142,6 @@
   case (it3 c r t)
   have ih: "finite ((supp r)::name set)" by fact
   let ?g' = "\<lambda>pi a'. f3 a' (r (pi@[(c,a')]))"     --"helper function"
-  --"two facts used by fresh_fun_equiv"
   have fact1: "\<forall>pi. finite ((supp (?g' pi))::name set)" using f ih
     by (rule_tac allI, finite_guess add: perm_append supp_prod fs_name1)
   have fact2: "\<forall>pi. \<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" 
@@ -152,8 +151,7 @@
       by (rule_tac f3_freshness_conditions_simple, simp_all add: supp_prod)
   qed
   show ?case using fact1 fact2 ih f
-    by (finite_guess add: fresh_fun_equiv[OF pt_name_inst, OF at_name_inst] 
-                          perm_append supp_prod fs_name1)
+    by (finite_guess add: fresh_fun_eqvt perm_append supp_prod fs_name1)
 qed 
 
 lemma it_trans: 
@@ -218,8 +216,8 @@
   and     a: "(pi\<bullet>t,y) \<in> it f1 f2 f3"
   shows "(t, \<lambda>pi2. y (pi2@(rev pi))) \<in> it f1 f2 f3"
 proof - 
-  from a have "((rev pi)\<bullet>(pi\<bullet>t),\<lambda>pi2. y (pi2@(rev pi))) \<in> it f1 f2 f3" using f c
-    by (simp add: it_perm_aux)
+  from a have "((rev pi)\<bullet>(pi\<bullet>t),\<lambda>pi2. y (pi2@(rev pi))) \<in> it f1 f2 f3" 
+    using f c by (simp add: it_perm_aux)
   thus ?thesis by perm_simp
 qed
 
@@ -314,8 +312,7 @@
   and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
   and     a: "(t,r) \<in> it f1 f2 f3"
   shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
-using a
-proof(induct)
+using a proof(induct)
   case it1 show ?case by (perm_simp add: it.intros)
 next
   case it2 thus ?case by (perm_simp add: it.intros)
@@ -350,8 +347,7 @@
   and     c: "b y = a"
   shows "(THE r. P r) y = a"
 apply(simp add: c[symmetric])
-apply(rule fun_cong[OF the1_equality])
-apply(rule a, rule b)
+apply(rule fun_cong[OF the1_equality, OF a, OF b])
 done
 
 lemma itfun'_prm:
@@ -426,7 +422,6 @@
   and     a: "b\<sharp>(a,t,f1,f2,f3)"
   shows "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = f3 b (itfun f1 f2 f3 ([(a,b)]\<bullet>t))"
 proof -
-  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
   have eq1: "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = itfun f1 f2 f3 (Lam [a].t)"
   proof -
     have "Lam [b].([(b,a)]\<bullet>t) = Lam [a].t" using a
@@ -438,7 +433,7 @@
     using f by (finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
   have fr_g: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" using f c 
     by (rule_tac f3_freshness_conditions_simple, auto simp add: supp_prod, 
-	finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
+        finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
   have fresh_b: "b\<sharp>?g" 
   proof -
     have "finite ((supp (a,t,f1,f2,f3))::name set)" using f
@@ -449,7 +444,6 @@
     ultimately show ?thesis using a
       by (auto intro!: supports_fresh, simp add: fresh_def)
   qed
-  (* main proof *)
   have "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = itfun f1 f2 f3 (Lam [a].t)" by (simp add: eq1)
   also have "\<dots> = fresh_fun ?g" by (rule itfun_Lam_aux1[OF f, OF c])
   also have "\<dots> = ?g b" using fresh_b fin_g fr_g