# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1338462073 -3600
# Node ID 5335c0ea743aec641a3686669ed18a7a72079cc3
# Parent  ca162f0a7957f93146e2144f05e8c4707ecaaf86# Parent  9eeea01bdbc0eecf92ea7923dd8bc983c2decd40
merged

diff -r ca162f0a7957 -r 5335c0ea743a Nominal/Nominal2_Base_Exec.thy
--- a/Nominal/Nominal2_Base_Exec.thy	Thu May 31 12:01:01 2012 +0100
+++ b/Nominal/Nominal2_Base_Exec.thy	Thu May 31 12:01:13 2012 +0100
@@ -1015,9 +1015,6 @@
 unfolding finite_def
 by (perm_simp) (rule refl)
 
-lemma Let_eqvt [eqvt]:
-  "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
-  unfolding Let_def permute_fun_app_eq ..
 
 subsubsection {* Equivariance for product operations *}
 
@@ -1678,6 +1675,13 @@
   unfolding supp_def 
   by simp
 
+lemma fresh_fun_eqvt:
+  assumes a: "eqvt f"
+  shows "a \<sharp> f"
+  using a
+  unfolding fresh_def
+  by (simp add: supp_fun_eqvt)
+
 lemma fresh_fun_eqvt_app:
   assumes a: "eqvt f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
@@ -1726,6 +1730,27 @@
 using supp_eqvt_at[OF asm fin]
 by auto
 
+text {* for handling of freshness of functions *}
+
+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
+  in
+    case (Term.add_frees f [], Term.add_vars f []) of
+      ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]})
+    | (x::_, []) => let
+         val thy = Proof_Context.theory_of (Simplifier.the_context ss)        
+         val argx = Free x
+         val absf = absfree x f
+         val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))]
+         val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)] 
+         val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+      in
+        SOME(thm RS @{thm Eq_TrueI}) 
+      end  
+    | (_, _) => NONE
+  end
+*}
 
 subsection {* helper functions for nominal_functions *}
 
@@ -3080,16 +3105,16 @@
 text {* packaging the freshness lemma into a function *}
 
 definition
-  fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
+  Fresh :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
 where
-  "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
-
-lemma fresh_fun_apply:
+  "Fresh h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
+
+lemma Fresh_apply:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
   assumes b: "atom a \<sharp> h"
-  shows "fresh_fun h = h a"
-unfolding fresh_fun_def
+  shows "Fresh h = h a"
+unfolding Fresh_def
 proof (rule the_equality)
   show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
   proof (intro strip)
@@ -3104,36 +3129,36 @@
   with b show "fr = h a" by auto
 qed
 
-lemma fresh_fun_apply':
+lemma Fresh_apply':
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
   assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
-  shows "fresh_fun h = h a"
-  apply (rule fresh_fun_apply)
+  shows "Fresh h = h a"
+  apply (rule Fresh_apply)
   apply (auto simp add: fresh_Pair intro: a)
   done
 
-lemma fresh_fun_eqvt:
+lemma Fresh_eqvt:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-  shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
+  shows "p \<bullet> (Fresh h) = Fresh (p \<bullet> h)"
   using a
   apply (clarsimp simp add: fresh_Pair)
-  apply (subst fresh_fun_apply', assumption+)
+  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_fun_apply' [symmetric])
+  apply (erule (1) Fresh_apply' [symmetric])
   done
 
-lemma fresh_fun_supports:
+lemma Fresh_supports:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-  shows "(supp h) supports (fresh_fun h)"
+  shows "(supp h) supports (Fresh h)"
   apply (simp add: supports_def fresh_def [symmetric])
-  apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
+  apply (simp add: Fresh_eqvt [OF a] swap_fresh_fresh)
   done
 
-notation fresh_fun (binder "FRESH " 10)
+notation Fresh (binder "FRESH " 10)
 
 lemma FRESH_f_iff:
   fixes P :: "'a::at \<Rightarrow> 'b::pure"
@@ -3143,12 +3168,12 @@
 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_fun_apply' [where a=a, OF _ pure_fresh])
+    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_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+    apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
     apply (rule refl)
     done
 qed
@@ -3165,13 +3190,13 @@
   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_fun_apply' [where a=a, OF _ pure_fresh])
+    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_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
-    apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
+    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
 qed