# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1338990647 -3600
# Node ID ae1defecd8c00f32a742e95e0605532af02a1e95
# Parent  313e6f2cdd8991a40c38d60ad23139e7ea11f5c9
a simproc for simplifying Fresh when there is a sufficiently fresh atom

diff -r 313e6f2cdd89 -r ae1defecd8c0 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jun 04 21:39:51 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jun 06 14:50:47 2012 +0100
@@ -1822,7 +1822,7 @@
 
 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ss => fn ctrm =>
   let 
-    val Const(@{const_name fresh}, _) $ _ $ f = term_of ctrm
+    val _ $ _ $ f = term_of ctrm
   in
     case (Term.add_frees f [], Term.add_vars f []) of
       ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]})
@@ -3140,6 +3140,14 @@
 setup {* Sign.add_const_constraint
   (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
 
+
+
+section {* Library functions for the nominal infrastructure *}
+
+use "nominal_library.ML"
+
+
+
 section {* The freshness lemma according to Andy Pitts *}
 
 lemma freshness_lemma:
@@ -3226,18 +3234,54 @@
   apply (auto simp add: fresh_Pair intro: a)
   done
 
+lemma "1 = 1 &&& 2 = 2"
+apply(tactic {* ALLGOALS (asm_full_simp_tac @{simpset}) *})
+done
+
+
+simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm =>
+  let
+     val ctxt = Simplifier.the_context ss
+     val _ $ h = term_of ctrm
+
+     val cfresh = @{const_name fresh}
+     val catom  = @{const_name atom}
+
+     val atoms = Simplifier.prems_of ss
+      |> map_filter (fn thm => case Thm.prop_of thm of                    
+           _ $ (Const (cfresh, _) $ (Const (catom, _) $ atm) $ _) => SOME (atm) | _ => NONE)
+      |> distinct (op=)
+     
+     fun get_thm atm = 
+       let
+         val goal1 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) h)
+         val goal2 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) (h $ atm))
+ 
+         val thm1 = Goal.prove ctxt [] [] goal1 (K (asm_simp_tac ss 1)) 
+         val thm2 = Goal.prove ctxt [] [] goal2 (K (asm_simp_tac ss 1)) 
+       in
+         SOME (@{thm Fresh_apply'} OF [thm1, thm2] RS eq_reflection)
+       end handle ERROR _ => NONE
+  in
+    get_first get_thm atoms
+  end
+*}
+
+
 lemma Fresh_eqvt:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
   shows "p \<bullet> (Fresh h) = Fresh (p \<bullet> h)"
-  using a
-  apply (clarsimp simp add: fresh_Pair)
-  apply (subst Fresh_apply', assumption+)
-  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
-  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
-  apply (simp only: atom_eqvt permute_fun_app_eq [where f=h])
-  apply (erule (1) Fresh_apply' [symmetric])
-  done
+proof -
+  from a obtain a::"'a::at" where fr: "atom a \<sharp> h" "atom a \<sharp> h a"
+    by (metis fresh_Pair)
+  then have fr_p: "atom (p \<bullet> a) \<sharp> (p \<bullet> h)" "atom (p \<bullet> a) \<sharp> (p \<bullet> h) (p \<bullet> a)"
+    by (metis atom_eqvt fresh_permute_iff eqvt_apply)+
+  have "p \<bullet> (Fresh h) = p \<bullet> (h a)" using fr by simp
+  also have "... = (p \<bullet> h) (p \<bullet> a)" by simp
+  also have "... = Fresh (p \<bullet> h)" using fr_p by simp
+  finally show "p \<bullet> (Fresh h) = Fresh (p \<bullet> h)" .
+qed
 
 lemma Fresh_supports:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
@@ -3256,15 +3300,8 @@
   shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
 proof -
   obtain a::'a where "atom a \<sharp> P" using P by (rule obtain_fresh')
-  show "(FRESH x. f (P x)) = f (FRESH x. P x)"
-    apply (subst Fresh_apply' [where a=a, OF _ pure_fresh])
-    apply (cut_tac `atom a \<sharp> P`)
-    apply (simp add: fresh_conv_MOST)
-    apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure fun_eq_iff)
-    apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
-    apply (rule refl)
-    done
+  then show "(FRESH x. f (P x)) = f (FRESH x. P x)"
+    by (simp add: pure_fresh)
 qed
 
 lemma FRESH_binop_iff:
@@ -3277,17 +3314,8 @@
 proof -
   from assms have "finite (supp (P, Q))" by (simp add: supp_Pair)
   then obtain a::'a where "atom a \<sharp> (P, Q)" by (rule obtain_fresh') 
-  then have "atom a \<sharp> P" and "atom a \<sharp> Q" by (simp_all add: fresh_Pair)
-  show ?thesis
-    apply (subst Fresh_apply' [where a=a, OF _ pure_fresh])
-    apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
-    apply (simp add: fresh_conv_MOST)
-    apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure fun_eq_iff)
-    apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
-    apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
-    apply (rule refl)
-    done
+  then show ?thesis
+    by (simp add: pure_fresh)
 qed
 
 lemma FRESH_conj_iff:
@@ -3302,12 +3330,6 @@
   shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
 using P Q by (rule FRESH_binop_iff)
 
-
-section {* Library functions for the nominal infrastructure *}
-
-use "nominal_library.ML"
-
-
 section {* Automation for creating concrete atom types *}
 
 text {* at the moment only single-sort concrete atoms are supported *}