--- a/src/HOL/Nominal/nominal_thmdecls.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon May 07 00:49:59 2007 +0200
@@ -1,13 +1,13 @@
(* ID: "$Id$"
Authors: Julien Narboux and Christian Urban
- This file introduces the infrastructure for the lemma
+ This file introduces the infrastructure for the lemma
declaration "eqvts" "bijs" and "freshs".
- By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
+ By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
in a data-slot in the theory context. Possible modifiers
are [attribute add] and [attribute del] for adding and deleting,
- respectively the lemma from the data-slot.
+ respectively the lemma from the data-slot.
*)
signature NOMINAL_THMDECLS =
@@ -21,7 +21,7 @@
val get_eqvt_thms: theory -> thm list
val get_fresh_thms: theory -> thm list
val get_bij_thms: theory -> thm list
-
+
val NOMINAL_EQVT_DEBUG : bool ref
end;
@@ -31,24 +31,12 @@
structure Data = GenericDataFun
(
- val name = "HOL/Nominal/eqvt";
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 = Drule.merge_rules (#eqvts r1, #eqvts r2),
- freshs = Drule.merge_rules (#freshs r1, #freshs r2),
+ fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2),
+ freshs = Drule.merge_rules (#freshs r1, #freshs r2),
bijs = Drule.merge_rules (#bijs r1, #bijs r2)}
- fun print context (data:T) =
- let
- fun print_aux msg thms =
- Pretty.writeln (Pretty.big_list msg
- (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
- in
- (print_aux "Equivariance lemmas: " (#eqvts data);
- print_aux "Freshness lemmas: " (#freshs data);
- print_aux "Bijection lemmas: " (#bijs data))
- end;
-
);
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
@@ -62,7 +50,19 @@
(* eqality-lemma can be derived. *)
exception EQVT_FORM of string;
-val print_data = Data.print o Context.Proof;
+fun print_data ctxt =
+ let
+ val data = Data.get (Context.Proof ctxt);
+ fun pretty_thms msg thms =
+ Pretty.big_list msg (map (ProofContext.pretty_thm ctxt) thms);
+ in
+ Pretty.writeln (Pretty.chunks
+ [pretty_thms "Equivariance lemmas:" (#eqvts data),
+ pretty_thms "Freshness lemmas:" (#freshs data),
+ pretty_thms "Bijection lemmas:" (#bijs data)])
+ end;
+
+
val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
val get_bij_thms = Context.Theory #> Data.get #> #bijs;
@@ -75,56 +75,56 @@
val NOMINAL_EQVT_DEBUG = ref false;
-fun tactic (msg,tac) =
- if !NOMINAL_EQVT_DEBUG
+fun tactic (msg,tac) =
+ if !NOMINAL_EQVT_DEBUG
then (EVERY [tac, print_tac ("after "^msg)])
- else tac
+ else tac
fun dynamic_thms thy name = PureThy.get_thms thy (Name name)
-fun tactic_eqvt ctx orig_thm pi typi =
- let
+fun tactic_eqvt ctx orig_thm pi typi =
+ let
val mypi = Thm.cterm_of ctx (Var (pi,typi))
val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
in
- EVERY [tactic ("iffI applied",rtac iffI 1),
- tactic ("simplifies with orig_thm and perm_bool",
- asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
+ EVERY [tactic ("iffI applied",rtac iffI 1),
+ tactic ("simplifies with orig_thm and perm_bool",
+ asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
tactic ("applies orig_thm instantiated with rev pi",
- dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
+ dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
tactic ("getting rid of all remaining perms",
- full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
+ full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
end;
fun get_derived_thm thy hyp concl orig_thm pi typi =
- let
+ let
val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
- val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
- val _ = Display.print_cterm (cterm_of thy goal_term)
+ val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
+ val _ = Display.print_cterm (cterm_of thy goal_term)
in
- Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
+ Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
end
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
(* the eqvt_thm_list to the user, we have to manually update the context and the *)
(* thm-list eqvt *)
fun update_context flag thms context =
- let
- val context' = fold (fn thm => Data.map (flag thm)) thms context
- in
+ let
+ val context' = fold (fn thm => Data.map (flag thm)) thms context
+ in
Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
end;
-(* replaces every variable x in t with pi o x *)
+(* replaces every variable x in t with pi o x *)
fun apply_pi trm (pi,typi) =
- let
+ 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
+ in
+ map_aterms only_vars trm
end;
(* returns *the* pi which is in front of all variables, provided there *)
@@ -132,69 +132,69 @@
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,[]),_])]))) $
- (Var (n,ty))) =>
+ (Const ("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 *)
- val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
- in
- if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
- then [(pi,typi)]
- else raise
- EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
- end
+ val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
+ in
+ if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
+ then [(pi,typi)]
+ else raise
+ EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
+ end
| Abs (_,_,t1) => get_pi_aux t1
| (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
- | _ => [])
- in
+ | _ => [])
+ in
(* collect first all pi's in front of variables in t and then use distinct *)
(* 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
+ (case (distinct (op =) (get_pi_aux t)) of
[(pi,typi)] => (pi,typi)
| _ => raise EQVT_FORM "All permutation should be the same")
end;
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
(* lemma list depending on flag. To be added the lemma has to satisfy a *)
-(* certain form. *)
+(* certain form. *)
fun eqvt_add_del_aux flag orig_thm context =
- let
+ let
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
- (* case: eqvt-lemma is of the implicational form *)
+ (* case: eqvt-lemma is of the implicational form *)
(Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
- let
+ let
val (pi,typi) = get_pi concl thy
in
if (apply_pi hyp (pi,typi) = concl)
- then
+ then
(warning ("equivariance lemma of the relational form");
[orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
else raise EQVT_FORM "Type Implication"
end
- (* case: eqvt-lemma is of the equational form *)
- | (Const ("Trueprop", _) $ (Const ("op =", _) $
+ (* case: eqvt-lemma is of the equational form *)
+ | (Const ("Trueprop", _) $ (Const ("op =", _) $
(Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
- (if (apply_pi lhs (pi,typi)) = rhs
+ (if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
else raise EQVT_FORM "Type Equality")
| _ => raise EQVT_FORM "Type unknown")
- in
+ in
update_context flag thms_to_be_added context
end
- handle EQVT_FORM s =>
+ handle EQVT_FORM s =>
error (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 *)
+(* data-slot *)
-fun simple_add_del_aux record_access name flag th context =
- let
+fun simple_add_del_aux record_access name flag th context =
+ let
val context' = Data.map (flag th) context
in
- Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
+ Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
end
fun bij_add_del_aux f = simple_add_del_aux #bijs "bijs" f
@@ -205,21 +205,20 @@
fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
-val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
-val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
-val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
-val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
+val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
+val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
+val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
+val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
-val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
+val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
-val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
+val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
val setup =
- Data.init #>
- Attrib.add_attributes
+ Attrib.add_attributes
[("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"),
("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
"equivariance theorem declaration (without checking the form of the lemma)"),
@@ -227,11 +226,3 @@
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")];
end;
-
-(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
-
-(* Drule.add_rule has type thm -> thm list -> thm list *)
-
-(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
-
-(* add_del_args is of type attribute -> attribute -> src -> attribute *)
\ No newline at end of file