--- a/Nominal-General/nominal_thmdecls.ML Sun Nov 14 12:09:14 2010 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,237 +0,0 @@
-(* Title: nominal_thmdecls.ML
- Author: Christian Urban
-
- Infrastructure for the lemma collection "eqvts".
-
- 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
-
- p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1)
-
- or
-
- c x1 x2 ... ==> c (p o x1) (p o x2) ... (2)
-
- and it is stored in the form
-
- p o c == c
-
- The [eqvt_raw] attribute just adds the theorem to eqvts_raw.
-
- TODO: In case of the form in (2) one should also
- add the equational form to eqvts
-*)
-
-signature NOMINAL_THMDECLS =
-sig
- val eqvt_add: attribute
- val eqvt_del: attribute
- val eqvt_raw_add: attribute
- val eqvt_raw_del: attribute
- 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
- val is_eqvt: Proof.context -> term -> bool
-end;
-
-structure Nominal_ThmDecls: NOMINAL_THMDECLS =
-struct
-
-structure EqvtData = Generic_Data
-( type T = thm Item_Net.T;
- val empty = Thm.full_rules;
- val extend = I;
- val merge = Item_Net.merge);
-
-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;
-
-val add_thm = EqvtData.map o Item_Net.update;
-val del_thm = EqvtData.map o Item_Net.remove;
-
-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
- | _ => raise TERM ("Term must be a constsnt.", [trm])
-
-
-
-(** transformation of eqvt 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
- | _ => []
-
-fun put_perm p trm =
- case trm of
- Bound _ => trm
- | Const _ => trm
- | t $ u => put_perm p t $ put_perm p u
- | Abs (x, ty, t) => Abs (x, ty, put_perm p t)
- | _ => mk_perm p trm
-
-(* 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
-
-
-(* 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
- 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 "
- 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 (put_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 (ProofContext.export ctxt' ctxt)
- |> safe_mk_equiv
- |> zero_var_indexes
- end
- end
-
-(* 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 ctxt p p' thm =
- let
- val thy = ProofContext.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 "
- 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 (put_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 (ProofContext.export ctxt' ctxt)
- end
- end
-
-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."
-
-
-(** 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_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",
- "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"]) #>
- Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
- Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);
-
-
-end;