--- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Apr 25 23:42:30 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Apr 26 00:42:59 2009 +0200
@@ -1,12 +1,12 @@
(* Authors: Julien Narboux and Christian Urban
This file introduces the infrastructure for the lemma
- declaration "eqvts" "bijs" and "freshs".
+ collection "eqvts".
- By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
- in a data-slot in the context. Possible modifiers
- are [attribute add] and [attribute del] for adding and deleting,
- respectively the lemma from the data-slot.
+ By attaching [eqvt], [eqvt_force] to a lemma, the lemma gets
+ stored in a data-slot in the context. Possible modifiers
+ are [... add] and [... del] for adding and deleting, respectively
+ the lemma from the data-slot.
*)
signature NOMINAL_THMDECLS =
@@ -17,9 +17,6 @@
val eqvt_force_del: attribute
val setup: theory -> theory
val get_eqvt_thms: Proof.context -> thm list
- val get_fresh_thms: Proof.context -> thm list
- val get_bij_thms: Proof.context -> thm list
-
val NOMINAL_EQVT_DEBUG : bool ref
end;
@@ -29,13 +26,11 @@
structure Data = GenericDataFun
(
- type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
- val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
- val extend = I;
- fun merge _ (r1:T,r2:T) = {eqvts = Thm.merge_thms (#eqvts r1, #eqvts r2),
- freshs = Thm.merge_thms (#freshs r1, #freshs r2),
- bijs = Thm.merge_thms (#bijs r1, #bijs r2)}
-);
+ type T = thm list
+ val empty = []:T
+ val extend = I
+ fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
+)
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
(* There are two forms: one is an implication (for relations) and the other is an *)
@@ -46,45 +41,40 @@
(* the implicational case it is also checked that the variables and permutation fit *)
(* together, i.e. are of the right "pt_class", so that a stronger version of the *)
(* equality-lemma can be derived. *)
-exception EQVT_FORM of string;
-
-val get_eqvt_thms = Context.Proof #> Data.get #> #eqvts;
-val get_fresh_thms = Context.Proof #> Data.get #> #freshs;
-val get_bij_thms = Context.Proof #> Data.get #> #bijs;
+exception EQVT_FORM of string
(* FIXME: should be a function in a library *)
-fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
+fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T))
-val NOMINAL_EQVT_DEBUG = ref false;
+val NOMINAL_EQVT_DEBUG = ref false
-fun tactic (msg,tac) =
- if !NOMINAL_EQVT_DEBUG
- then tac THEN print_tac ("after "^msg)
- else tac
+fun tactic (msg, tac) =
+ if !NOMINAL_EQVT_DEBUG
+ then tac THEN' (K (print_tac ("after " ^ msg)))
+ else tac
fun tactic_eqvt ctx orig_thm pi pi' =
- let
- val mypi = Thm.cterm_of ctx pi
- val T = fastype_of pi'
- val mypifree = Thm.cterm_of ctx (Const ("List.rev", T --> T) $ pi')
- val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
- in
- EVERY [tactic ("iffI applied",rtac iffI 1),
- tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)),
- tactic ("solve with orig_thm", (etac orig_thm 1)),
- tactic ("applies orig_thm instantiated with rev pi",
- dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
- tactic ("getting rid of the pi on the right",
- (rtac @{thm perm_boolI} 1)),
- tactic ("getting rid of all remaining perms",
- full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)]
- end;
+let
+ val mypi = Thm.cterm_of ctx pi
+ val T = fastype_of pi'
+ val mypifree = Thm.cterm_of ctx (Const (@{const_name "List.rev"}, T --> T) $ pi')
+ val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
+in
+ EVERY1 [tactic ("iffI applied",rtac @{thm iffI}),
+ tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
+ tactic ("solve with orig_thm", etac orig_thm),
+ tactic ("applies orig_thm instantiated with rev pi",
+ dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
+ tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
+ tactic ("getting rid of all remaining perms",
+ full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
+end;
fun get_derived_thm ctxt hyp concl orig_thm pi typi =
let
val thy = ProofContext.theory_of ctxt;
val pi' = Var (pi, typi);
- val lhs = Const ("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
+ val lhs = Const (@{const_name "Nominal.perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
val ([goal_term, pi''], ctxt') = Variable.import_terms false
[HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
val _ = Display.print_cterm (cterm_of thy goal_term)
@@ -95,23 +85,25 @@
end
(* replaces every variable x in t with pi o x *)
-fun apply_pi trm (pi,typi) =
- let
- fun only_vars t =
- (case t of
- Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
- | _ => t)
- in
- map_aterms only_vars trm
- end;
+fun apply_pi trm (pi, typi) =
+let
+ fun only_vars t =
+ (case t of
+ Var (n, ty) =>
+ (Const (@{const_name "Nominal.perm"}, typi --> ty --> ty)
+ $ (Var (pi, typi)) $ (Var (n, ty)))
+ | _ => t)
+in
+ map_aterms only_vars trm
+end;
(* returns *the* pi which is in front of all variables, provided there *)
(* exists such a pi; otherwise raises EQVT_FORM *)
fun get_pi t thy =
let fun get_pi_aux s =
(case s of
- (Const ("Nominal.perm",typrm) $
- (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
+ (Const (@{const_name "Nominal.perm"} ,typrm) $
+ (Var (pi,typi as Type("List.list", [Type ("*", [Type (tyatm,[]),_])]))) $
(Var (n,ty))) =>
let
(* FIXME: this should be an operation the library *)
@@ -130,7 +122,7 @@
(* to ensure that all pi's must have been the same, i.e. distinct returns *)
(* a singleton-list *)
(case (distinct (op =) (get_pi_aux t)) of
- [(pi,typi)] => (pi,typi)
+ [(pi,typi)] => (pi, typi)
| _ => raise EQVT_FORM "All permutation should be the same")
end;
@@ -155,8 +147,8 @@
else raise EQVT_FORM "Type Implication"
end
(* case: eqvt-lemma is of the equational form *)
- | (Const ("Trueprop", _) $ (Const ("op =", _) $
- (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
+ | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
+ (Const (@{const_name "Nominal.perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
else raise EQVT_FORM "Type Equality")
@@ -165,38 +157,26 @@
fold (fn thm => Data.map (flag thm)) thms_to_be_added context
end
handle EQVT_FORM s =>
- error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
+ error (Display.string_of_thm orig_thm ^
+ " does not comply with the form of an equivariance lemma (" ^ s ^").")
-(* in cases of bij- and freshness, we just add the lemmas to the *)
-(* data-slot *)
-fun eqvt_map f (r:Data.T) = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r};
-fun fresh_map f (r:Data.T) = {eqvts = #eqvts r, freshs = f (#freshs r), bijs = #bijs r};
-fun bij_map f (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = f (#bijs r)};
+fun eqvt_map f (r:Data.T) = f r;
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm));
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm));
val eqvt_force_add = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm);
val eqvt_force_del = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm);
-val bij_add = Thm.declaration_attribute (Data.map o bij_map o Thm.add_thm);
-val bij_del = Thm.declaration_attribute (Data.map o bij_map o Thm.del_thm);
-val fresh_add = Thm.declaration_attribute (Data.map o fresh_map o Thm.add_thm);
-val fresh_del = Thm.declaration_attribute (Data.map o fresh_map o Thm.del_thm);
-
+val get_eqvt_thms = Context.Proof #> Data.get;
val setup =
- Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
- "equivariance theorem declaration" #>
- Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
- "equivariance theorem declaration (without checking the form of the lemma)" #>
- Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del)
- "freshness theorem declaration" #>
- Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del)
- "bijection theorem declaration" #>
- PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
- PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
- PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
+ Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
+ "equivariance theorem declaration"
+ #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
+ "equivariance theorem declaration (without checking the form of the lemma)"
+ #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get)
+
end;