# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271661955 -7200
# Node ID cfda1ec86a9e62d4310437947c6cff279586de07
# Parent  a08eaea622d125357303b78dc560b0dfa23d5ed9# Parent  c7cdea70eacdcc30446f46201f30546d02ac1e00
merge

diff -r a08eaea622d1 -r cfda1ec86a9e Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 19 09:25:43 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 19 09:25:55 2010 +0200
@@ -2,8 +2,8 @@
     Author:     Brian Huffman, 
     Author:     Christian Urban
 
-    Equivariance, Supp and Fresh Lemmas for Operators. 
-    (Contains many, but not all such lemmas.)
+    Equivariance, supp and freshness lemmas for various operators 
+    (contains many, but not all such lemmas).
 *)
 theory Nominal2_Eqvt
 imports Nominal2_Base Nominal2_Atoms
@@ -12,7 +12,6 @@
      ("nominal_eqvt.ML")
 begin
 
-
 section {* Logical Operators *}
 
 lemma eq_eqvt:
@@ -238,7 +237,7 @@
 
 section {* Equivariance automation *}
 
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
 
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
@@ -289,14 +288,21 @@
 use "nominal_permeq.ML"
 setup Nominal_Permeq.setup
 
+ML {*
+val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
+val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
+  (Scan.repeat (Args.const true))) []
+*}
+
 method_setup perm_simp =
- {* Attrib.thms >> 
-    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}
+ {* test1 -- test2 >> 
+    (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
  {* pushes permutations inside *}
 
 method_setup perm_strict_simp =
- {* Attrib.thms >> 
-    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *}
+ {* test1 -- test2 >> 
+    (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL 
+       (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *}
  {* pushes permutations inside, raises an error if it cannot solve all permutations *}
 
 declare [[trace_eqvt = true]]
@@ -369,9 +375,8 @@
 
 text {* Problem: there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
-apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*})
-apply(perm_simp)
-(* apply(perm_strict_simp) *)
+apply(perm_strict_simp exclude: The)
+apply(perm_simp exclude: The)
 oops
 
 (* automatic equivariance procedure for 
diff -r a08eaea622d1 -r cfda1ec86a9e Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Mon Apr 19 09:25:43 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Mon Apr 19 09:25:55 2010 +0200
@@ -7,6 +7,7 @@
 signature NOMINAL_LIBRARY =
 sig
   val mk_minus: term -> term
+  val mk_perm_ty: typ -> term -> term -> term
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
 
@@ -21,12 +22,10 @@
 fun mk_minus p = 
  Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
 
-fun mk_perm p trm =
-let
-  val ty = fastype_of trm
-in
+fun mk_perm_ty ty p trm =
   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
-end
+
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t])
diff -r a08eaea622d1 -r cfda1ec86a9e Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Mon Apr 19 09:25:43 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Mon Apr 19 09:25:55 2010 +0200
@@ -33,6 +33,7 @@
   val setup: theory -> theory
   val get_eqvts_thms: Proof.context -> thm list
   val get_eqvts_raw_thms: Proof.context -> thm list
+  val eqvt_transform: Proof.context -> thm -> thm
 
   (* TEMPORARY FIX *)
   val add_thm: thm -> Context.generic -> Context.generic
@@ -87,12 +88,20 @@
 
 fun add_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
+    Const ("==", _) $ _ $ _ => 
+      EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
   | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
-fun eq_transform_tac thm = 
+
+(** transformation of eqvt lemmas **)
+
+
+(* transforms equations into the "p o c = c"-form 
+   from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)
+
+fun eqvt_transform_eq_tac thm = 
 let
   val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}
 in
@@ -102,8 +111,7 @@
      rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
 end
 
-(* transform equations into the "p o c = c"-form *)
-fun transform_eq ctxt thm = 
+fun eqvt_transform_eq ctxt thm = 
 let
   val ((p, t), rhs) = apfst dest_perm 
     (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))
@@ -118,18 +126,22 @@
   else if not (rhs aconv (put_p p t))
     then error "Eqvt lemma is not of the right form (arguments do not agree)"
   else if is_Const t 
-    then thm
+    then safe_mk_equiv thm
   else 
     let 
       val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
       val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
     in
-      Goal.prove ctxt [] [] goal' (fn _ => eq_transform_tac thm 1)
+      Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
       |> singleton (ProofContext.export ctxt' ctxt)
+      |> safe_mk_equiv
     end
 end
 
-fun imp_transform_tac thy p p' thm = 
+(* transforms equations into the "p o c = c"-form 
+   from R x1 ...xn ==> R (p o x1) ... (p o xn) *)
+
+fun eqvt_transform_imp_tac thy p p' thm = 
 let
   val cp = Thm.cterm_of thy p
   val cp' = Thm.cterm_of thy (mk_minus p')
@@ -140,7 +152,7 @@
     rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]
 end
 
-fun transform_imp ctxt thm =
+fun eqvt_transform_imp ctxt thm =
 let
   val thy = ProofContext.theory_of ctxt
   val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))
@@ -161,31 +173,46 @@
       val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
     in
       Goal.prove ctxt' [] [] goal'
-        (fn _ => imp_transform_tac thy (the p) p' thm 1) 
+        (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) 
       |> singleton (ProofContext.export ctxt' ctxt)
-      |> transform_eq ctxt
+      |> eqvt_transform_eq ctxt
     end
 end     
 
-fun transform addel_fun thm context = 
-let
-  val ctxt = Context.proof_of context
-in
-  case (prop_of thm) of
-    @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ 
-      (Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>
-        addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context
-  | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => 
-        addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context
-  | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
-end 
+fun eqvt_transform ctxt thm = 
+ case (prop_of thm) of
+   @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ 
+     (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => 
+       eqvt_transform_eq ctxt thm
+ | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => 
+     eqvt_transform_imp ctxt thm
+ | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
+ 
+
+(** attributes **)
 
-val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));
-val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm));
+val eqvt_add = Thm.declaration_attribute 
+  (fn thm => fn context =>
+   let
+     val thm' = eqvt_transform (Context.proof_of context) thm
+   in
+     context |> add_thm thm |> add_raw_thm thm'
+   end)
+
+val eqvt_del = Thm.declaration_attribute
+  (fn thm => fn context =>
+   let
+     val thm' = eqvt_transform (Context.proof_of context) thm
+   in
+     context |> del_thm thm |> del_raw_thm thm'
+   end)
 
 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;
 
+
+(** setup function **)
+
 val setup =
   Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) 
     (cat_lines ["Declaration of equivariance lemmas - they will automtically be",  
diff -r a08eaea622d1 -r cfda1ec86a9e Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Mon Apr 19 09:25:43 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Mon Apr 19 09:25:55 2010 +0200
@@ -5,8 +5,8 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
-(* this should not be a raw equivariant rule *)
-(* we force it to be                         *)
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be       *)
 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
 thm eqvts
 (*declare permute_pure[eqvt]*)
@@ -679,5 +679,18 @@
   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 qed
 
+section {* test about equivariance for alpha *}
+
+thm eqvts
+thm eqvts_raw
+
+declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_tkind_raw
+
+thm eqvts
+thm eqvts_raw
+
 end
 
diff -r a08eaea622d1 -r cfda1ec86a9e Nominal/Perm.thy
--- a/Nominal/Perm.thy	Mon Apr 19 09:25:43 2010 +0200
+++ b/Nominal/Perm.thy	Mon Apr 19 09:25:55 2010 +0200
@@ -4,8 +4,7 @@
 
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
-  fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
-  val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
+  open Nominal_Library; 
 *}
 
 ML {*
@@ -94,10 +93,10 @@
             in list_abs (map (pair "x") Us,
               Free (nth perm_names_types' (body_index dt)) $ pi $
                 list_comb (x, map (fn (i, U) =>
-                  (permute U) $ (minus_perm $ pi) $ Bound i)
+                  (mk_perm_ty U (mk_minus pi) (Bound i)))
                   ((length Us - 1 downto 0) ~~ Us)))
             end
-          else (permute T) $ pi $ x
+          else (mk_perm_ty T pi x)
         end;
     in
       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -125,7 +124,8 @@
   lthy'
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
   |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
-  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
+  |> Class_Target.prove_instantiation_exit_result morphism tac 
+      (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
   end
 
 *}