1.1 --- a/src/Pure/goal.ML	Fri Oct 28 22:27:54 2005 +0200
     1.2 +++ b/src/Pure/goal.ML	Fri Oct 28 22:27:55 2005 +0200
     1.3 @@ -2,8 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius and Lawrence C Paulson
     1.6  
     1.7 -Internal goals.  NB: by attaching the Goal constant the conclusion of
     1.8 -a goal state is guaranteed to be atomic.
     1.9 +Tactical goal state.
    1.10  *)
    1.11  
    1.12  signature BASIC_GOAL =
    1.13 @@ -15,13 +14,16 @@
    1.14  sig
    1.15    include BASIC_GOAL
    1.16    val init: cterm -> thm
    1.17 +  val protect: thm -> thm
    1.18    val conclude: thm -> thm
    1.19    val finish: thm -> thm
    1.20 -  val norm_hhf_rule: thm -> thm
    1.21 -  val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.22 +  val norm_hhf: thm -> thm
    1.23 +  val comp_hhf: thm -> thm -> thm
    1.24 +  val compose_hhf_tac: thm list -> int -> tactic
    1.25    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.26    val prove_multi: theory -> string list -> term list -> term list ->
    1.27      (thm list -> tactic) -> thm list
    1.28 +  val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.29  
    1.30    (* FIXME remove *)
    1.31    val norm_hhf_plain: thm -> thm
    1.32 @@ -33,29 +35,36 @@
    1.33  structure Goal: GOAL =
    1.34  struct
    1.35  
    1.36 -(* managing goal states *)
    1.37 +(** goals **)
    1.38  
    1.39  (*
    1.40 -  ------------ (init)
    1.41 -  C ==> Goal C
    1.42 +  -------- (init)
    1.43 +  C ==> #C
    1.44  *)
    1.45 -fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI;
    1.46 +fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI;
    1.47  
    1.48  (*
    1.49 -  A ==> ... ==> Goal C
    1.50 -  -------------------- (conclude)
    1.51 +    A ==> ... ==> C
    1.52 +  ------------------ (protect)
    1.53 +  #(A ==> ... ==> C)
    1.54 +*)
    1.55 +fun protect th = th COMP Drule.incr_indexes th Drule.protectI;
    1.56 +
    1.57 +(*
    1.58 +  A ==> ... ==> #C
    1.59 +  ---------------- (conclude)
    1.60    A ==> ... ==> C
    1.61  *)
    1.62  fun conclude th =
    1.63    (case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1)
    1.64 -      (Drule.incr_indexes_wrt [] [] [] [th] Drule.goalD) of
    1.65 +      (Drule.incr_indexes th Drule.protectD) of
    1.66      SOME th' => th'
    1.67    | NONE => raise THM ("Failed to conclude goal", 0, [th]));
    1.68  
    1.69  (*
    1.70 -  Goal C
    1.71 -  ------ (finish)
    1.72 -    C
    1.73 +  #C
    1.74 +  --- (finish)
    1.75 +   C
    1.76  *)
    1.77  fun finish th =
    1.78    (case Thm.nprems_of th of
    1.79 @@ -65,24 +74,39 @@
    1.80        ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
    1.81  
    1.82  
    1.83 -(* prove_raw -- minimal result checks, no normalization *)
    1.84 +
    1.85 +(** results **)
    1.86 +
    1.87 +(* HHF normal form *)
    1.88  
    1.89  val norm_hhf_plain =  (* FIXME remove *)
    1.90    (not o Drule.is_norm_hhf o Thm.prop_of) ?
    1.91      MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq];
    1.92  
    1.93 -val norm_hhf_rule =
    1.94 +val norm_hhf =
    1.95    norm_hhf_plain
    1.96    #> Thm.adjust_maxidx_thm
    1.97    #> Drule.gen_all;
    1.98  
    1.99 -fun prove_raw casms cprop tac =
   1.100 -  (case SINGLE (tac (map (norm_hhf_rule o Thm.assume) casms)) (init cprop) of
   1.101 -    SOME th => Drule.implies_intr_list casms (finish th)
   1.102 -  | NONE => raise ERROR_MESSAGE "Tactic failed.");
   1.103  
   1.104 +(* composition of normal results *)
   1.105  
   1.106 -(* tactical proving *)
   1.107 +fun compose_hhf tha i thb =
   1.108 +  Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb;
   1.109 +
   1.110 +fun comp_hhf tha thb =
   1.111 +  (case Seq.pull (compose_hhf tha 1 thb) of
   1.112 +    SOME (th, _) => th
   1.113 +  | NONE => raise THM ("comp_hhf", 1, [tha, thb]));
   1.114 +
   1.115 +fun compose_hhf_tac [] _ = no_tac
   1.116 +  | compose_hhf_tac (th :: ths) i = PRIMSEQ (compose_hhf th i) APPEND compose_hhf_tac ths i;
   1.117 +
   1.118 +
   1.119 +
   1.120 +(** tactical theorem proving **)
   1.121 +
   1.122 +(* prove *)
   1.123  
   1.124  local
   1.125  
   1.126 @@ -107,7 +131,7 @@
   1.127  
   1.128      val cparams = map (cert_safe o Free) params;
   1.129      val casms = map cert_safe asms;
   1.130 -    val prems = map (norm_hhf_rule o Thm.assume) casms;
   1.131 +    val prems = map (norm_hhf o Thm.assume) casms;
   1.132  
   1.133      val goal = init (cert_safe prop);
   1.134      val goal' = (case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.");
   1.135 @@ -128,7 +152,7 @@
   1.136  
   1.137  fun prove_multi thy xs asms prop tac =
   1.138    gen_prove (fn fixed_tfrees => Drule.zero_var_indexes o
   1.139 -      (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
   1.140 +      (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf)
   1.141      thy xs asms prop tac;
   1.142  
   1.143  fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
   1.144 @@ -139,6 +163,14 @@
   1.145  end;
   1.146  
   1.147  
   1.148 +(* prove_raw -- no checks, no normalization of result! *)
   1.149 +
   1.150 +fun prove_raw casms cprop tac =
   1.151 +  (case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of
   1.152 +    SOME th => Drule.implies_intr_list casms (finish th)
   1.153 +  | NONE => raise ERROR_MESSAGE "Tactic failed.");
   1.154 +
   1.155 +
   1.156  (* SELECT_GOAL *)
   1.157  
   1.158  (*Tactical for restricting the effect of a tactic to subgoal i.  Works