--- a/Nominal-General/nominal_thmdecls.ML Sat Sep 11 05:56:49 2010 +0800
+++ b/Nominal-General/nominal_thmdecls.ML Sun Sep 12 22:46:40 2010 +0800
@@ -118,85 +118,85 @@
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..."
+ 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
+ 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
+ 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
+ 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 "op ="}, _) $
- (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."
+ 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 |> eqvt_transform_eq ctxt
+ | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
(** attributes **)