export compose_hhf;
authorwenzelm
Tue Nov 08 10:43:10 2005 +0100 (2005-11-08)
changeset 1811963901a9b99dc
parent 18118 38316c575328
child 18120 41328805d4db
export compose_hhf;
removed obsolete norm_hhf_plain;
tuned;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Tue Nov 08 10:43:09 2005 +0100
     1.2 +++ b/src/Pure/goal.ML	Tue Nov 08 10:43:10 2005 +0100
     1.3 @@ -18,18 +18,13 @@
     1.4    val conclude: thm -> thm
     1.5    val finish: thm -> thm
     1.6    val norm_hhf: thm -> thm
     1.7 +  val compose_hhf: thm -> int -> thm -> thm Seq.seq
     1.8 +  val compose_hhf_tac: thm -> int -> tactic
     1.9    val comp_hhf: thm -> thm -> thm
    1.10 -  val compose_hhf_tac: thm list -> int -> tactic
    1.11    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.12    val prove_multi: theory -> string list -> term list -> term list ->
    1.13      (thm list -> tactic) -> thm list
    1.14    val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.15 -
    1.16 -  (* FIXME remove *)
    1.17 -  val norm_hhf_plain: thm -> thm
    1.18 -  val prove_multi_plain: theory -> string list -> term list -> term list ->
    1.19 -    (thm list -> tactic) -> thm list
    1.20 -  val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.21  end;
    1.22  
    1.23  structure Goal: GOAL =
    1.24 @@ -44,9 +39,9 @@
    1.25  fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI;
    1.26  
    1.27  (*
    1.28 -    A ==> ... ==> C
    1.29 -  ------------------ (protect)
    1.30 -  #(A ==> ... ==> C)
    1.31 +   C
    1.32 +  --- (protect)
    1.33 +  #C
    1.34  *)
    1.35  fun protect th = th COMP Drule.incr_indexes th Drule.protectI;
    1.36  
    1.37 @@ -79,12 +74,9 @@
    1.38  
    1.39  (* HHF normal form *)
    1.40  
    1.41 -val norm_hhf_plain =  (* FIXME remove *)
    1.42 +val norm_hhf =
    1.43    (not o Drule.is_norm_hhf o Thm.prop_of) ?
    1.44 -    MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq];
    1.45 -
    1.46 -val norm_hhf =
    1.47 -  norm_hhf_plain
    1.48 +    MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq]
    1.49    #> Thm.adjust_maxidx_thm
    1.50    #> Drule.gen_all;
    1.51  
    1.52 @@ -94,23 +86,21 @@
    1.53  fun compose_hhf tha i thb =
    1.54    Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb;
    1.55  
    1.56 +fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
    1.57 +
    1.58  fun comp_hhf tha thb =
    1.59 -  (case Seq.pull (compose_hhf tha 1 thb) of
    1.60 -    SOME (th, _) => th
    1.61 -  | NONE => raise THM ("comp_hhf", 1, [tha, thb]));
    1.62 -
    1.63 -fun compose_hhf_tac [] _ = no_tac
    1.64 -  | compose_hhf_tac (th :: ths) i = PRIMSEQ (compose_hhf th i) APPEND compose_hhf_tac ths i;
    1.65 +  (case Seq.chop (2, compose_hhf tha 1 thb) of
    1.66 +    ([th], _) => th
    1.67 +  | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
    1.68 +  | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
    1.69  
    1.70  
    1.71  
    1.72  (** tactical theorem proving **)
    1.73  
    1.74 -(* prove *)
    1.75 +(* prove_multi *)
    1.76  
    1.77 -local
    1.78 -
    1.79 -fun gen_prove finish_thm thy xs asms props tac =
    1.80 +fun prove_multi thy xs asms props tac =
    1.81    let
    1.82      val prop = Logic.mk_conjunction_list props;
    1.83      val statement = Logic.list_implies (asms, prop);
    1.84 @@ -134,7 +124,7 @@
    1.85      val prems = map (norm_hhf o Thm.assume) casms;
    1.86  
    1.87      val goal = init (cert_safe prop);
    1.88 -    val goal' = (case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.");
    1.89 +    val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.";
    1.90      val raw_result = finish goal' handle THM (msg, _, _) => err msg;
    1.91  
    1.92      val prop' = Thm.prop_of raw_result;
    1.93 @@ -145,23 +135,16 @@
    1.94      |> map
    1.95        (Drule.implies_intr_list casms
    1.96          #> Drule.forall_intr_list cparams
    1.97 -        #> finish_thm fixed_tfrees)
    1.98 +        #> norm_hhf
    1.99 +        #> (#1 o Thm.varifyT' fixed_tfrees)
   1.100 +        #> Drule.zero_var_indexes)
   1.101    end;
   1.102  
   1.103 -in
   1.104  
   1.105 -fun prove_multi thy xs asms prop tac =
   1.106 -  gen_prove (fn fixed_tfrees => Drule.zero_var_indexes o
   1.107 -      (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf)
   1.108 -    thy xs asms prop tac;
   1.109 +(* prove *)
   1.110  
   1.111  fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
   1.112  
   1.113 -fun prove_multi_plain thy xs asms prop tac = gen_prove (K norm_hhf_plain) thy xs asms prop tac;
   1.114 -fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac);
   1.115 -
   1.116 -end;
   1.117 -
   1.118  
   1.119  (* prove_raw -- no checks, no normalization of result! *)
   1.120