tuned
authorChristian Urban <urbanc@in.tum.de>
Mon Apr 27 00:29:54 2009 +0200 (2009-04-27)
changeset 30991c814a34f687e
parent 30990 4872eef36167
child 30995 e46639644fcd
tuned
src/HOL/Nominal/nominal_thmdecls.ML
     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