1.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Apr 26 23:16:24 2009 +0200
1.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Apr 27 00:29:54 2009 +0200
1.3 @@ -3,10 +3,10 @@
1.4 This file introduces the infrastructure for the lemma
1.5 collection "eqvts".
1.6
1.7 - By attaching [eqvt], [eqvt_force] to a lemma, the lemma gets
1.8 + By attaching [eqvt] or [eqvt_force] to a lemma, it will get
1.9 stored in a data-slot in the context. Possible modifiers
1.10 - are [... add] and [... del] for adding and deleting, respectively
1.11 - the lemma from the data-slot.
1.12 + are [... add] and [... del] for adding and deleting,
1.13 + respectively, the lemma from the data-slot.
1.14 *)
1.15
1.16 signature NOMINAL_THMDECLS =
1.17 @@ -43,9 +43,6 @@
1.18 (* equality-lemma can be derived. *)
1.19 exception EQVT_FORM of string
1.20
1.21 -(* FIXME: should be a function in a library *)
1.22 -fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T))
1.23 -
1.24 val NOMINAL_EQVT_DEBUG = ref false
1.25
1.26 fun tactic (msg, tac) =
1.27 @@ -53,14 +50,14 @@
1.28 then tac THEN' (K (print_tac ("after " ^ msg)))
1.29 else tac
1.30
1.31 -fun tactic_eqvt ctx orig_thm pi pi' =
1.32 +fun prove_eqvt_tac ctxt orig_thm pi pi' =
1.33 let
1.34 - val mypi = Thm.cterm_of ctx pi
1.35 + val mypi = Thm.cterm_of ctxt pi
1.36 val T = fastype_of pi'
1.37 - val mypifree = Thm.cterm_of ctx (Const (@{const_name "List.rev"}, T --> T) $ pi')
1.38 - val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
1.39 + val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
1.40 + val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp"
1.41 in
1.42 - EVERY1 [tactic ("iffI applied",rtac @{thm iffI}),
1.43 + EVERY1 [tactic ("iffI applied", rtac @{thm iffI}),
1.44 tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
1.45 tactic ("solve with orig_thm", etac orig_thm),
1.46 tactic ("applies orig_thm instantiated with rev pi",
1.47 @@ -74,36 +71,38 @@
1.48 let
1.49 val thy = ProofContext.theory_of ctxt;
1.50 val pi' = Var (pi, typi);
1.51 - val lhs = Const (@{const_name "Nominal.perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
1.52 + val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
1.53 val ([goal_term, pi''], ctxt') = Variable.import_terms false
1.54 [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
1.55 val _ = Display.print_cterm (cterm_of thy goal_term)
1.56 in
1.57 Goal.prove ctxt' [] [] goal_term
1.58 - (fn _ => tactic_eqvt thy orig_thm pi' pi'') |>
1.59 + (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
1.60 singleton (ProofContext.export ctxt' ctxt)
1.61 end
1.62
1.63 -(* replaces every variable x in t with pi o x *)
1.64 +(* replaces in t every variable, say x, with pi o x *)
1.65 fun apply_pi trm (pi, typi) =
1.66 let
1.67 - fun only_vars t =
1.68 - (case t of
1.69 - Var (n, ty) =>
1.70 - (Const (@{const_name "Nominal.perm"}, typi --> ty --> ty)
1.71 - $ (Var (pi, typi)) $ (Var (n, ty)))
1.72 - | _ => t)
1.73 + fun replace n ty =
1.74 + let
1.75 + val c = Const (@{const_name "perm"}, typi --> ty --> ty)
1.76 + val v1 = Var (pi, typi)
1.77 + val v2 = Var (n, ty)
1.78 + in
1.79 + c $ v1 $ v2
1.80 + end
1.81 in
1.82 - map_aterms only_vars trm
1.83 -end;
1.84 + map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
1.85 +end
1.86
1.87 (* returns *the* pi which is in front of all variables, provided there *)
1.88 (* exists such a pi; otherwise raises EQVT_FORM *)
1.89 fun get_pi t thy =
1.90 let fun get_pi_aux s =
1.91 (case s of
1.92 - (Const (@{const_name "Nominal.perm"} ,typrm) $
1.93 - (Var (pi,typi as Type("List.list", [Type ("*", [Type (tyatm,[]),_])]))) $
1.94 + (Const (@{const_name "perm"} ,typrm) $
1.95 + (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $
1.96 (Var (n,ty))) =>
1.97 let
1.98 (* FIXME: this should be an operation the library *)
1.99 @@ -148,7 +147,7 @@
1.100 end
1.101 (* case: eqvt-lemma is of the equational form *)
1.102 | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
1.103 - (Const (@{const_name "Nominal.perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
1.104 + (Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
1.105 (if (apply_pi lhs (pi,typi)) = rhs
1.106 then [orig_thm]
1.107 else raise EQVT_FORM "Type Equality")
1.108 @@ -161,13 +160,11 @@
1.109 " does not comply with the form of an equivariance lemma (" ^ s ^").")
1.110
1.111
1.112 -fun eqvt_map f (r:Data.T) = f r;
1.113 +val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
1.114 +val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
1.115
1.116 -val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm));
1.117 -val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm));
1.118 -
1.119 -val eqvt_force_add = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm);
1.120 -val eqvt_force_del = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm);
1.121 +val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm);
1.122 +val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm);
1.123
1.124 val get_eqvt_thms = Context.Proof #> Data.get;
1.125