--- 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
--- 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])
--- 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",
--- 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
--- 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
*}