simplified type attribute;
authorwenzelm
Sat Jan 21 23:02:20 2006 +0100 (2006-01-21)
changeset 18729216e31270509
parent 18728 6790126ab5f6
child 18730 843da46f89ac
simplified type attribute;
tuned;
src/HOL/Hyperreal/transfer.ML
src/HOL/Tools/reconstruction.ML
src/HOL/Tools/specification_package.ML
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Sat Jan 21 23:02:14 2006 +0100
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Sat Jan 21 23:02:20 2006 +0100
     1.3 @@ -2,20 +2,20 @@
     1.4      ID          : $Id$
     1.5      Author      : Brian Huffman
     1.6  
     1.7 -Transfer principle tactic for nonstandard analysis
     1.8 +Transfer principle tactic for nonstandard analysis.
     1.9  *)
    1.10  
    1.11 -signature TRANSFER_TAC =
    1.12 +signature TRANSFER =
    1.13  sig
    1.14 -  val transfer_tac: thm list -> int -> tactic
    1.15 +  val transfer_tac: Proof.context -> thm list -> int -> tactic
    1.16    val add_const: string -> theory -> theory
    1.17    val setup: theory -> theory
    1.18  end;
    1.19  
    1.20 -structure Transfer: TRANSFER_TAC =
    1.21 +structure Transfer: TRANSFER =
    1.22  struct
    1.23  
    1.24 -structure TransferData = TheoryDataFun
    1.25 +structure TransferData = GenericDataFun
    1.26  (struct
    1.27    val name = "HOL/transfer";
    1.28    type T = {
    1.29 @@ -25,7 +25,6 @@
    1.30      consts: string list
    1.31    };
    1.32    val empty = {intros = [], unfolds = [], refolds = [], consts = []};
    1.33 -  val copy = I;
    1.34    val extend = I;
    1.35    fun merge _
    1.36      ({intros = intros1, unfolds = unfolds1,
    1.37 @@ -59,29 +58,26 @@
    1.38  
    1.39  val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"]
    1.40  
    1.41 -fun transfer_thm_of thy ths t =
    1.42 +fun transfer_thm_of ctxt ths t =
    1.43    let
    1.44 -    val {intros,unfolds,refolds,consts} = TransferData.get thy
    1.45 +    val thy = ProofContext.theory_of ctxt;
    1.46 +    val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
    1.47      val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t))
    1.48      val u = unstar_term consts t'
    1.49 -    val tacs =
    1.50 -      [ rewrite_goals_tac (ths @ refolds @ unfolds)
    1.51 -      , rewrite_goals_tac atomizers
    1.52 -      , match_tac [transitive_thm] 1
    1.53 -      , resolve_tac [transfer_start] 1
    1.54 -      , REPEAT_ALL_NEW (resolve_tac intros) 1
    1.55 -      , match_tac [reflexive_thm] 1 ]
    1.56 -  in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (fn _ => EVERY tacs) end
    1.57 +    val tac =
    1.58 +      rewrite_goals_tac (ths @ refolds @ unfolds) THEN
    1.59 +      rewrite_goals_tac atomizers THEN
    1.60 +      match_tac [transitive_thm] 1 THEN
    1.61 +      resolve_tac [transfer_start] 1 THEN
    1.62 +      REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
    1.63 +      match_tac [reflexive_thm] 1
    1.64 +  in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (K tac) end
    1.65  
    1.66 -fun transfer_tac ths =
    1.67 +fun transfer_tac ctxt ths =
    1.68      SUBGOAL (fn (t,i) =>
    1.69          (fn th =>
    1.70 -            let val thy = theory_of_thm th
    1.71 -                val tr = transfer_thm_of thy ths t
    1.72 -            in rewrite_goals_tac [tr] th
    1.73 -            end
    1.74 -        )
    1.75 -    )
    1.76 +            let val tr = transfer_thm_of ctxt ths t
    1.77 +            in rewrite_goals_tac [tr] th end))
    1.78  
    1.79  local
    1.80  fun map_intros f = TransferData.map
    1.81 @@ -96,46 +92,32 @@
    1.82    (fn {intros,unfolds,refolds,consts} =>
    1.83      {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
    1.84  in
    1.85 -fun intro_add_global (thy, thm) = (map_intros (Drule.add_rule thm) thy, thm);
    1.86 -fun intro_del_global (thy, thm) = (map_intros (Drule.del_rule thm) thy, thm);
    1.87 +val intro_add = Thm.declaration_attribute (map_intros o Drule.add_rule);
    1.88 +val intro_del = Thm.declaration_attribute (map_intros o Drule.del_rule);
    1.89  
    1.90 -fun unfold_add_global (thy, thm) = (map_unfolds (Drule.add_rule thm) thy, thm);
    1.91 -fun unfold_del_global (thy, thm) = (map_unfolds (Drule.del_rule thm) thy, thm);
    1.92 +val unfold_add = Thm.declaration_attribute (map_unfolds o Drule.add_rule);
    1.93 +val unfold_del = Thm.declaration_attribute (map_unfolds o Drule.del_rule);
    1.94  
    1.95 -fun refold_add_global (thy, thm) = (map_refolds (Drule.add_rule thm) thy, thm);
    1.96 -fun refold_del_global (thy, thm) = (map_refolds (Drule.del_rule thm) thy, thm);
    1.97 +val refold_add = Thm.declaration_attribute (map_refolds o Drule.add_rule);
    1.98 +val refold_del = Thm.declaration_attribute (map_refolds o Drule.del_rule);
    1.99  end
   1.100  
   1.101 -fun add_const c = TransferData.map
   1.102 +fun add_const c = Context.theory_map (TransferData.map
   1.103    (fn {intros,unfolds,refolds,consts} =>
   1.104 -    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})
   1.105 +    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
   1.106  
   1.107 -local
   1.108 -  val undef_local =
   1.109 -    Attrib.add_del_args
   1.110 -      Attrib.undef_local_attribute
   1.111 -      Attrib.undef_local_attribute;
   1.112 -in
   1.113 -  val intro_attr =
   1.114 -   (Attrib.add_del_args intro_add_global intro_del_global, undef_local);
   1.115 -  val unfold_attr =
   1.116 -   (Attrib.add_del_args unfold_add_global unfold_del_global, undef_local);
   1.117 -  val refold_attr =
   1.118 -   (Attrib.add_del_args refold_add_global refold_del_global, undef_local);
   1.119 -end
   1.120 -
   1.121 -val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
   1.122 +val transfer_method = Method.thms_ctxt_args (fn ths => fn ctxt =>
   1.123 +  Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ctxt ths));
   1.124  
   1.125  val setup =
   1.126    TransferData.init #>
   1.127    Attrib.add_attributes
   1.128 -    [("transfer_intro", intro_attr,
   1.129 +    [("transfer_intro", Attrib.add_del_args intro_add intro_del,
   1.130        "declaration of transfer introduction rule"),
   1.131 -     ("transfer_unfold", unfold_attr,
   1.132 +     ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del,
   1.133        "declaration of transfer unfolding rule"),
   1.134 -     ("transfer_refold", refold_attr,
   1.135 +     ("transfer_refold", Attrib.add_del_args refold_add refold_del,
   1.136        "declaration of transfer refolding rule")] #>
   1.137 -  Method.add_method
   1.138 -    ("transfer", Method.thms_args transfer_method, "transfer principle");
   1.139 +  Method.add_method ("transfer", transfer_method, "transfer principle");
   1.140  
   1.141  end;
     2.1 --- a/src/HOL/Tools/reconstruction.ML	Sat Jan 21 23:02:14 2006 +0100
     2.2 +++ b/src/HOL/Tools/reconstruction.ML	Sat Jan 21 23:02:20 2006 +0100
     2.3 @@ -7,8 +7,6 @@
     2.4  (*Attributes for reconstructing external resolution proofs*)
     2.5  
     2.6  structure Reconstruction =
     2.7 -let open Attrib
     2.8 -in
     2.9  struct
    2.10  
    2.11  (**************************************************************)
    2.12 @@ -16,10 +14,10 @@
    2.13  (**************************************************************)
    2.14  
    2.15  fun mksubstlist [] sublist = sublist
    2.16 -  | mksubstlist ((a, (_, b)) :: rest) sublist = 
    2.17 +  | mksubstlist ((a, (_, b)) :: rest) sublist =
    2.18        let val vartype = type_of b
    2.19            val avar = Var(a,vartype)
    2.20 -          val newlist = ((avar,b)::sublist) 
    2.21 +          val newlist = ((avar,b)::sublist)
    2.22        in mksubstlist rest newlist end;
    2.23  
    2.24  
    2.25 @@ -31,21 +29,15 @@
    2.26       select_literal (lit1 + 1) cl1
    2.27       RSN ((lit2 + 1), cl2);
    2.28  
    2.29 -fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
    2.30 -
    2.31 -fun gen_binary thm = syntax
    2.32 -      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
    2.33 -val binary_global = gen_binary global_thm;
    2.34 -val binary_local = gen_binary local_thm;
    2.35 -
    2.36 -(*I have not done the MRR rule because it seems to be identifical to 
    2.37 -binary*)
    2.38 +val binary = Attrib.syntax
    2.39 +  (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    2.40 +    >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
    2.41  
    2.42  
    2.43  fun inst_single sign t1 t2 cl =
    2.44      let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
    2.45      in  hd (Seq.list_of(distinct_subgoals_tac
    2.46 -			    (cterm_instantiate [(ct1,ct2)] cl)))  
    2.47 +                            (cterm_instantiate [(ct1,ct2)] cl)))
    2.48      end;
    2.49  
    2.50  fun inst_subst sign substs cl =
    2.51 @@ -71,9 +63,8 @@
    2.52         inst_subst sign (mksubstlist envlist []) cl
    2.53      end;
    2.54  
    2.55 -fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
    2.56 -
    2.57 -fun factor x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
    2.58 +val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
    2.59 +  >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
    2.60  
    2.61  
    2.62  (** Paramodulation **)
    2.63 @@ -91,32 +82,24 @@
    2.64      in Meson.negated_asm_of_head newth' end;
    2.65  
    2.66  
    2.67 -fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
    2.68 -
    2.69 -fun gen_paramod thm = syntax
    2.70 -      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
    2.71 -val paramod_global = gen_paramod global_thm;
    2.72 -val paramod_local = gen_paramod local_thm;
    2.73 +val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    2.74 +  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
    2.75  
    2.76  
    2.77  (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
    2.78  
    2.79 -fun demod_rule ((cl1, lit1), (cl2 , lit2)) = 
    2.80 +fun demod_rule ((cl1, lit1), (cl2 , lit2)) =
    2.81      let  val eq_lit_th = select_literal (lit1+1) cl1
    2.82           val mod_lit_th = select_literal (lit2+1) cl2
    2.83 -	 val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
    2.84 +         val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
    2.85           val eqsubst = eq_lit_th RSN (2,rev_subst)
    2.86           val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
    2.87           val offset = #maxidx(rep_thm newth) + 1
    2.88 -	                  (*ensures "renaming apart" even when Vars are frozen*)
    2.89 +                          (*ensures "renaming apart" even when Vars are frozen*)
    2.90      in Meson.negated_asm_of_head (thaw offset newth) end;
    2.91  
    2.92 -fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j)));
    2.93 -
    2.94 -fun gen_demod thm = syntax
    2.95 -      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> demod_syntax);
    2.96 -val demod_global = gen_demod global_thm;
    2.97 -val demod_local = gen_demod local_thm;
    2.98 +val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    2.99 +  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j)))));
   2.100  
   2.101  
   2.102  (** Conversion of a theorem into clauses **)
   2.103 @@ -124,22 +107,18 @@
   2.104  (*For efficiency, we rely upon memo-izing in ResAxioms.*)
   2.105  fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
   2.106  
   2.107 -fun clausify_syntax i (x, th) = (x, clausify_rule (th,i));
   2.108 -
   2.109 -fun clausify x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
   2.110 +val clausify = Attrib.syntax (Scan.lift Args.nat
   2.111 +  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
   2.112  
   2.113  
   2.114  (** theory setup **)
   2.115  
   2.116  val setup =
   2.117    Attrib.add_attributes
   2.118 -    [("binary", (binary_global, binary_local), "binary resolution"),
   2.119 -     ("paramod", (paramod_global, paramod_local), "paramodulation"),
   2.120 -     ("demod", (demod_global, demod_local), "demodulation"),
   2.121 -     ("factor", (factor, factor), "factoring"),
   2.122 -     ("clausify", (clausify, clausify), "conversion to clauses")];
   2.123 +    [("binary", binary, "binary resolution"),
   2.124 +     ("paramod", paramod, "paramodulation"),
   2.125 +     ("demod", demod, "demodulation"),
   2.126 +     ("factor", factor, "factoring"),
   2.127 +     ("clausify", clausify, "conversion to clauses")];
   2.128  
   2.129  end
   2.130 -end
   2.131 -
   2.132 -
     3.1 --- a/src/HOL/Tools/specification_package.ML	Sat Jan 21 23:02:14 2006 +0100
     3.2 +++ b/src/HOL/Tools/specification_package.ML	Sat Jan 21 23:02:20 2006 +0100
     3.3 @@ -8,8 +8,8 @@
     3.4  signature SPECIFICATION_PACKAGE =
     3.5  sig
     3.6    val quiet_mode: bool ref
     3.7 -  val add_specification_i: string option -> (bstring * xstring * bool) list ->
     3.8 -    theory attribute
     3.9 +  val add_specification: string option -> (bstring * xstring * bool) list ->
    3.10 +    theory * thm -> theory * thm
    3.11  end
    3.12  
    3.13  structure SpecificationPackage: SPECIFICATION_PACKAGE =
    3.14 @@ -82,11 +82,15 @@
    3.15        | NONE => mk_definitional cos arg
    3.16  end
    3.17  
    3.18 -fun add_specification_i axiomatic cos arg =
    3.19 +fun add_specification axiomatic cos arg =
    3.20      arg |> apsnd freezeT
    3.21          |> proc_exprop axiomatic cos
    3.22          |> apsnd standard
    3.23  
    3.24 +fun add_spec x y (context, thm) =
    3.25 +  (Context.the_theory context, thm) |> add_specification x y |>> Context.Theory;
    3.26 +
    3.27 +
    3.28  (* Collect all intances of constants in term *)
    3.29  
    3.30  fun collect_consts (        t $ u,tms) = collect_consts (u,collect_consts (t,tms))
    3.31 @@ -200,7 +204,7 @@
    3.32                          args |> apsnd (remove_alls frees)
    3.33                               |> apsnd undo_imps
    3.34                               |> apsnd standard
    3.35 -                             |> Thm.apply_attributes (map (Attrib.global_attribute thy) atts)
    3.36 +                             |> Thm.theory_attributes (map (Attrib.attribute thy) atts)
    3.37                               |> add_final
    3.38                               |> Library.swap
    3.39                      end
    3.40 @@ -224,9 +228,11 @@
    3.41                  arg |> apsnd freezeT
    3.42                      |> process_all (zip3 alt_names rew_imps frees)
    3.43              end
    3.44 +            fun post_proc (context, th) =
    3.45 +                post_process (Context.theory_of context, th) |>> Context.Theory;
    3.46      in
    3.47        IsarThy.theorem_i Drule.internalK
    3.48 -        ("", [add_specification_i axiomatic (zip3 names cnames overloaded), post_process])
    3.49 +        ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
    3.50          (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
    3.51      end
    3.52