# HG changeset patch
# User urbanc
# Date 1150137153 -7200
# Node ID d319e39a2e0e2f047803311cf0deb144acee4692
# Parent  a0c36e0fc89783966b3073ed7de93fa4cf7f137d
added lemma fresh_unit to Nominal.thy
made the fresh_guess tactic to solve more goals
adapted Iteration.thy to use the new tactic

diff -r a0c36e0fc897 -r d319e39a2e0e src/HOL/Nominal/Examples/Iteration.thy
--- a/src/HOL/Nominal/Examples/Iteration.thy	Mon Jun 12 18:17:21 2006 +0200
+++ b/src/HOL/Nominal/Examples/Iteration.thy	Mon Jun 12 20:32:33 2006 +0200
@@ -4,13 +4,12 @@
 imports "../Nominal"
 begin
 
-
 atom_decl name
 
 nominal_datatype lam = Var "name"
                      | App "lam" "lam"
                      | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
- 
+
 types 'a f1_ty  = "name\<Rightarrow>('a::pt_name)"
       'a f2_ty  = "'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
       'a f3_ty  = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
@@ -46,8 +45,7 @@
   assumes a: "finite ((supp (f1,f2,f3))::name set)"
   and     b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
   shows "\<exists>r. (t,r)\<in>it f1 f2 f3"
-apply(rule_tac lam.induct'[of "\<lambda>_. (supp (f1,f2,f3))::name set" 
-                              "\<lambda>z. \<lambda>t. \<exists>r. (t,r)\<in>it f1 f2 f3", simplified])
+apply(rule_tac lam.induct'[of "\<lambda>_. (supp (f1,f2,f3))" "\<lambda>z. \<lambda>t. \<exists>r. (t,r)\<in>it f1 f2 f3", simplified])
 apply(fold fresh_def)
 apply(auto intro: it.intros a)
 done
@@ -119,17 +117,9 @@
       apply(perm_simp add: calc_atm fresh_prod)
       done      
     have fs3: "c\<sharp>f3 a1 r1" using fresh it1 a
-      apply(rule_tac S="supp (f3,a1,r1)" in supports_fresh)
-      apply(supports_simp)
-      apply(simp add: supp_prod fs_name1 it_fin_supp[OF a])
-      apply(simp add: fresh_def[symmetric] fresh_prod fresh_atm)
-      done
+      by (fresh_guess add: supp_prod fs_name1 it_fin_supp[OF a] fresh_atm)
     have fs4: "c\<sharp>f3 a2 r2" using fresh it2 a
-      apply(rule_tac S="supp (f3,a2,r2)" in supports_fresh)
-      apply(supports_simp)
-      apply(simp add: supp_prod fs_name1 it_fin_supp[OF a])
-      apply(simp add: fresh_def[symmetric] fresh_prod fresh_atm)
-      done
+      by (fresh_guess add: supp_prod fs_name1 it_fin_supp[OF a] fresh_atm)
     have "f3 a1 r1 = [(a1,c)]\<bullet>(f3 a1 r1)" using fs1 fs3 by perm_simp
     also have "\<dots> = f3 c ([(a1,c)]\<bullet>r1)" using f1 fresh by (perm_simp add: calc_atm fresh_prod)
     also have "\<dots> = f3 c ([(a2,c)]\<bullet>r2)" using eq4 by simp
diff -r a0c36e0fc897 -r d319e39a2e0e src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Jun 12 18:17:21 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Jun 12 20:32:33 2006 +0200
@@ -235,6 +235,10 @@
   shows "a\<sharp>{x} = a\<sharp>x"
   by (simp add: fresh_def supp_singleton)
 
+lemma fresh_unit:
+  shows "a\<sharp>()"
+  by (simp add: fresh_def supp_unit)
+
 lemma fresh_prod:
   fixes a :: "'x"
   and   x :: "'a"
diff -r a0c36e0fc897 -r d319e39a2e0e src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Mon Jun 12 18:17:21 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Jun 12 20:32:33 2006 +0200
@@ -268,11 +268,16 @@
               Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
             val supports_fresh_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_fresh_rule'
+            val fresh_def   = thm "Nominal.fresh_def";
+	    val fresh_prod  = thm "Nominal.fresh_prod";
+            val fresh_unit  = thm "Nominal.fresh_unit";
+	    val simps       = [symmetric fresh_def,fresh_prod,fresh_unit]
           in
             (tactical ("guessing of the right set that supports the goal",
-                      EVERY [compose_tac (false, supports_fresh_rule'', 3) i(*,
-                             asm_full_simp_tac ss (i+1),
-                             supports_tac tactical ss i*)])) st
+                      EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
+                             asm_full_simp_tac (ss addsimps simps) (i+2),
+                             asm_full_simp_tac ss (i+1), 
+                             supports_tac tactical ss i])) st
           end
         | _ => Seq.empty
     end