--- a/Nominal/nominal_thmdecls.ML Tue Mar 26 16:41:31 2013 +0100
+++ b/Nominal/nominal_thmdecls.ML Wed Mar 27 16:08:30 2013 +0100
@@ -1,27 +1,59 @@
(* Title: nominal_thmdecls.ML
Author: Christian Urban
+ Author: Tjark Weber
- Infrastructure for the lemma collection "eqvts".
+ Infrastructure for the lemma collections "eqvts", "eqvts_raw".
Provides the attributes [eqvt] and [eqvt_raw], and the theorem
- lists eqvts and eqvts_raw. The first attribute will store the
- theorem in the eqvts list and also in the eqvts_raw list. For
- the latter the theorem is expected to be of the form
+ lists "eqvts" and "eqvts_raw".
+
+ The [eqvt] attribute expects a theorem of the form
+
+ ?p \<bullet> (c ?x1 ?x2 ...) = c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ... (1)
+
+ or, if c is a relation with arity >= 1, of the form
+
+ c ?x1 ?x2 ... ==> c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ... (2)
- p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1)
+ [eqvt] will store this theorem in the form (1) or, if c
+ is a relation with arity >= 1, in the form
+
+ c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ... = c ?x1 ?x2 ... (3)
- or
+ in "eqvts". (The orientation of (3) was chosen because
+ Isabelle's simplifier uses equations from left to right.)
+ [eqvt] will also derive and store the theorem
+
+ ?p \<bullet> c == c (4)
+
+ in "eqvts_raw".
- c x1 x2 ... ==> c (p o x1) (p o x2) ... (2)
+ (1)-(4) are all logically equivalent. We consider (1) and (2)
+ to be more end-user friendly, i.e., slightly more natural to
+ understand and prove, while (3) and (4) make the rewriting
+ system for equivariance more predictable and less prone to
+ looping in Isabelle.
- and it is stored in the form
+ The [eqvt_raw] attribute expects a theorem of the form (4),
+ and merely stores it in "eqvts_raw".
- p o c == c
+ [eqvt_raw] is provided because certain equivariance theorems
+ would lead to looping when used for simplification in the form
+ (1): notably, equivariance of permute (infix \<bullet>), i.e.,
+ ?p \<bullet> (?q \<bullet> ?x) = (?p \<bullet> ?q) \<bullet> (?p \<bullet> ?x).
- The [eqvt_raw] attribute just adds the theorem to eqvts_raw.
+ To support binders such as All/Ex/Ball/Bex etc., which are
+ typically applied to abstractions, argument terms ?xi (as well
+ as permuted arguments ?p \<bullet> ?xi) in (1)-(3) need not be eta-
+ contracted, i.e., they may be of the form "%z. ?xi z" or
+ "%z. (?p \<bullet> ?x) z", respectively.
- TODO: In case of the form in (2) one should also
- add the equational form to eqvts
+ For convenience, argument terms ?xi (as well as permuted
+ arguments ?p \<bullet> ?xi) in (1)-(3) may actually be tuples, e.g.,
+ "(?xi, ?xj)" or "(?p \<bullet> ?xi, ?p \<bullet> ?xj)", respectively.
+
+ In (1)-(4), "c" is either a (global) constant or a locally
+ fixed parameter, e.g., of a locale or type class.
*)
signature NOMINAL_THMDECLS =
@@ -46,206 +78,246 @@
val extend = I;
val merge = Item_Net.merge);
+(* EqvtRawData is implemented with a Termtab (rather than an
+ Item_Net) so that we can efficiently decide whether a given
+ constant has a corresponding equivariance theorem stored, cf.
+ the function is_eqvt. *)
structure EqvtRawData = Generic_Data
( type T = thm Termtab.table;
val empty = Termtab.empty;
val extend = I;
val merge = Termtab.merge (K true));
-val eqvts = Item_Net.content o EqvtData.get;
-val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get;
-
-val get_eqvts_thms = eqvts o Context.Proof;
-val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
-
-fun checked_update key net =
- (if Item_Net.member net key then
- warning "Theorem already declared as equivariant."
- else ();
- Item_Net.update key net)
-
-val add_thm = EqvtData.map o checked_update;
-val del_thm = EqvtData.map o Item_Net.remove;
+val eqvts = Item_Net.content o EqvtData.get
+val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get
-fun add_raw_thm thm =
- case prop_of thm of
- Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm))
- | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm])
-
-fun del_raw_thm thm =
- case prop_of thm of
- Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c)
- | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm])
-
-fun is_eqvt ctxt trm =
- case trm of
- (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c
- | _ => false (* raise TERM ("Term must be a constant.", [trm]) *)
-
+val get_eqvts_thms = eqvts o Context.Proof
+val get_eqvts_raw_thms = eqvts_raw o Context.Proof
-(** transformation of eqvt lemmas **)
+(** raw equivariance lemmas **)
-fun get_perms trm =
- case trm of
- Const (@{const_name permute}, _) $ _ $ (Bound _) =>
- raise TERM ("get_perms called on bound", [trm])
- | Const (@{const_name permute}, _) $ p $ _ => [p]
- | t $ u => get_perms t @ get_perms u
- | Abs (_, _, t) => get_perms t
- | _ => []
+(* Returns true iff an equivariance lemma exists in "eqvts_raw"
+ for a given term. *)
+val is_eqvt =
+ Termtab.defined o EqvtRawData.get o Context.Proof
-fun add_perm p trm =
+(* Returns c if thm is of the form (4), raises an error
+ otherwise. *)
+fun key_of_raw_thm context thm =
let
- fun aux trm =
- case trm of
- Bound _ => trm
- | Const _ => trm
- | t $ u => aux t $ aux u
- | Abs (x, ty, t) => Abs (x, ty, aux t)
- | _ => mk_perm p trm
+ fun error_msg () =
+ error
+ ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^
+ Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+ in
+ case prop_of thm of
+ Const ("==", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
+ if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
+ c
+ else
+ error_msg ()
+ | _ => error_msg ()
+ end
+
+fun add_raw_thm thm context =
+ let
+ val c = key_of_raw_thm context thm
in
- strip_comb trm
- ||> map aux
- |> list_comb
- end
+ if Termtab.defined (EqvtRawData.get context) c then
+ warning ("Replacing existing raw equivariance theorem for \"" ^
+ Syntax.string_of_term (Context.proof_of context) c ^ "\".")
+ else ();
+ EqvtRawData.map (Termtab.update (c, thm)) context
+ end
+
+fun del_raw_thm thm context =
+ let
+ val c = key_of_raw_thm context thm
+ in
+ if Termtab.defined (EqvtRawData.get context) c then
+ EqvtRawData.map (Termtab.delete c) context
+ else (
+ warning ("Cannot delete non-existing raw equivariance theorem for \"" ^
+ Syntax.string_of_term (Context.proof_of context) c ^ "\".");
+ context
+ )
+ end
-(* tests whether there is a disagreement between the permutations,
- and that there is at least one permutation *)
-fun is_bad_list [] = true
- | is_bad_list [_] = false
- | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
+(** adding/deleting lemmas to/from "eqvts" **)
+
+fun add_thm thm context =
+ (
+ if Item_Net.member (EqvtData.get context) thm then
+ warning ("Theorem already declared as equivariant:\n" ^
+ Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+ else ();
+ EqvtData.map (Item_Net.update thm) context
+ )
+
+fun del_thm thm context =
+ (
+ if Item_Net.member (EqvtData.get context) thm then
+ EqvtData.map (Item_Net.remove thm) context
+ else (
+ warning ("Cannot delete non-existing equivariance theorem:\n" ^
+ Syntax.string_of_term (Context.proof_of context) (prop_of thm));
+ context
+ )
+ )
-(* transforms equations into the "p o c == c"-form
- from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)
+(** transformation of equivariance lemmas **)
+
+(* Transforms a theorem of the form (1) into the form (4). *)
+local
-fun eqvt_transform_eq_tac thm =
-let
- val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}
+fun tac thm =
+ let
+ val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"}
+ in
+ REPEAT o FIRST'
+ [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),
+ rtac (thm RS @{thm "trans"}),
+ rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}]
+ end
+
in
- REPEAT o FIRST'
- [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),
- rtac (thm RS @{thm trans}),
- rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
-end
-
-fun eqvt_transform_eq ctxt thm =
- let
- val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))
- handle TERM _ => error "Equivariance lemma must be an equality."
- val (p, t) = dest_perm lhs
- handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..."
- val ps = get_perms rhs handle TERM _ => []
- val (c, c') = (head_of t, head_of rhs)
- val msg = "Equivariance lemma is not of the right form "
+fun thm_4_of_1 ctxt thm =
+ let
+ val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt)
+ 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
- if c <> c'
- then error (msg ^ "(constants do not agree).")
- else if is_bad_list (p :: ps)
- then error (msg ^ "(permutations do not agree).")
- else if not (rhs aconv (add_perm p t))
- then error (msg ^ "(arguments do not agree).")
- else if is_Const t
- 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 _ => eqvt_transform_eq_tac thm 1)
- |> singleton (Proof_Context.export ctxt' ctxt)
- |> safe_mk_equiv
- |> zero_var_indexes
- end
+ Goal.prove ctxt [] [] goal' (fn _ => tac thm 1)
+ |> singleton (Proof_Context.export ctxt' ctxt)
+ |> (fn th => th RS @{thm "eq_reflection"})
+ |> zero_var_indexes
+ end
+ handle TERM _ =>
+ raise THM ("thm_4_of_1", 0, [thm])
+
+end (* local *)
+
+(* Transforms a theorem of the form (2) into the form (1). *)
+local
+
+fun tac thm thm' =
+ let
+ val ss_thms = @{thms "permute_minus_cancel"(2)}
+ in
+ EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac,
+ rtac @{thm "permute_boolI"}, dtac thm', full_simp_tac (HOL_basic_ss addsimps ss_thms)]
end
-(* transforms equations into the "p o c == c"-form
- from R x1 ...xn ==> R (p o x1) ... (p o xn) *)
+in
-fun eqvt_transform_imp_tac ctxt p p' thm =
+fun thm_1_of_2 ctxt thm =
let
- val thy = Proof_Context.theory_of ctxt
- val cp = Thm.cterm_of thy p
- val cp' = Thm.cterm_of thy (mk_minus p')
- val thm' = Drule.cterm_instantiate [(cp, cp')] thm
- val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)}
- in
- EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac,
- rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]
- end
-
-fun eqvt_transform_imp ctxt thm =
- let
- val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))
- val (c, c') = (head_of prem, head_of concl)
- val ps = get_perms concl handle TERM _ => []
- val p = try hd ps
- val msg = "Equivariance lemma is not of the right form "
+ val (prem, concl) = thm |> prop_of |> Logic.dest_implies |> pairself HOLogic.dest_Trueprop
+ (* since argument terms "?p \<bullet> ?x1" may actually be eta-expanded
+ or tuples, we need the following function to find ?p *)
+ fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p
+ | find_perm (Const (@{const_name "Pair"}, _) $ x $ _) = find_perm x
+ | find_perm (Abs (_, _, body)) = find_perm body
+ | find_perm _ = raise THM ("thm_3_of_2", 0, [thm])
+ val p = concl |> dest_comb |> snd |> find_perm
+ val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
+ val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
+ val certify = cterm_of (theory_of_thm thm)
+ val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm
in
- if c <> c'
- then error (msg ^ "(constants do not agree).")
- else if is_bad_list ps
- then error (msg ^ "(permutations do not agree).")
- else if not (concl aconv (add_perm (the p) prem))
- then error (msg ^ "(arguments do not agree).")
- else
- let
- val prem' = mk_perm (the p) prem
- val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl))
- val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
- in
- Goal.prove ctxt' [] [] goal'
- (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1)
- |> singleton (Proof_Context.export ctxt' ctxt)
- end
- end
+ Goal.prove ctxt' [] [] goal' (fn _ => tac thm thm' 1)
+ |> singleton (Proof_Context.export ctxt' ctxt)
+ end
+ handle TERM _ =>
+ raise THM ("thm_1_of_2", 0, [thm])
+
+end (* local *)
+
+(* Transforms a theorem of the form (1) into the form (3). *)
+fun thm_3_of_1 _ thm =
+ (thm RS (@{thm "permute_bool_def"} RS @{thm "sym"} RS @{thm "trans"}) RS @{thm "sym"})
+ |> zero_var_indexes
+
+local
+ val msg = cat_lines
+ ["Equivariance theorem must be of the form",
+ " ?p \<bullet> (c ?x1 ?x2 ...) = c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ...",
+ "or, if c is a relation with arity >= 1, of the form",
+ " c ?x1 ?x2 ... ==> c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ..."]
+in
-fun eqvt_transform ctxt thm =
- case (prop_of thm) of
- @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $
- (Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>
- eqvt_transform_eq ctxt thm
- | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) =>
- eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt
- | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
-
+(* Transforms a theorem of the form (1) or (2) into the form (4). *)
+fun eqvt_transform ctxt thm =
+ (case prop_of thm of @{const "Trueprop"} $ _ =>
+ thm_4_of_1 ctxt thm
+ | @{const "==>"} $ _ $ _ =>
+ thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
+ | _ =>
+ error msg)
+ handle THM _ =>
+ error msg
+
+(* Transforms a theorem of the form (1) into theorems of the
+ form (1) (or, if c is a relation with arity >= 1, of the form
+ (3)) and (4); transforms a theorem of the form (2) into
+ theorems of the form (3) and (4). *)
+fun eqvt_and_raw_transform ctxt thm =
+ (case prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) =>
+ let
+ val th' =
+ if fastype_of c_args = @{typ "bool"}
+ andalso (not o null) (snd (fixed_nonfixed_args ctxt c_args)) then
+ thm_3_of_1 ctxt thm
+ else
+ thm
+ in
+ (th', thm_4_of_1 ctxt thm)
+ end
+ | @{const "==>"} $ _ $ _ =>
+ let
+ val th1 = thm_1_of_2 ctxt thm
+ in
+ (thm_3_of_1 ctxt th1, thm_4_of_1 ctxt th1)
+ end
+ | _ =>
+ error msg)
+ handle THM _ =>
+ error msg
+
+end (* local *)
+
(** attributes **)
-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_raw_add = Thm.declaration_attribute add_raw_thm
+val eqvt_raw_del = Thm.declaration_attribute del_raw_thm
-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)
+fun eqvt_add_or_del eqvt_fn raw_fn =
+ Thm.declaration_attribute
+ (fn thm => fn context =>
+ let
+ val (eqvt, raw) = eqvt_and_raw_transform (Context.proof_of context) thm
+ in
+ context |> eqvt_fn eqvt |> raw_fn raw
+ end)
-val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
-val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;
+val eqvt_add = eqvt_add_or_del add_thm add_raw_thm
+val eqvt_del = eqvt_add_or_del del_thm 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",
- "brought into the form p o c == c"]) #>
- Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
- (cat_lines ["Declaration of equivariance lemmas - no",
- "transformation is performed"]) #>
+ Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
+ "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #>
+ Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
+ "Declaration of raw equivariance lemmas - no transformation is performed" #>
Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
- Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);
-
+ Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw)
end;