# HG changeset patch # User wenzelm # Date 1130531275 -7200 # Node ID 09ab79d4e8e17266a50d1beb82dab332e74ac3b5 # Parent ccf2972f6f897917e12f71eaa72087296c60729d renamed Goal constant to prop, more general protect/unprotect interfaces; renamed norm_hhf_rule to norm_hhf; added comp_hhf, compose_hhf_tac, based on Drule.lift_all; diff -r ccf2972f6f89 -r 09ab79d4e8e1 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Oct 28 22:27:54 2005 +0200 +++ b/src/Pure/goal.ML Fri Oct 28 22:27:55 2005 +0200 @@ -2,8 +2,7 @@ ID: $Id$ Author: Makarius and Lawrence C Paulson -Internal goals. NB: by attaching the Goal constant the conclusion of -a goal state is guaranteed to be atomic. +Tactical goal state. *) signature BASIC_GOAL = @@ -15,13 +14,16 @@ sig include BASIC_GOAL val init: cterm -> thm + val protect: thm -> thm val conclude: thm -> thm val finish: thm -> thm - val norm_hhf_rule: thm -> thm - val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm + val norm_hhf: thm -> thm + val comp_hhf: thm -> thm -> thm + val compose_hhf_tac: thm list -> int -> tactic val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm val prove_multi: theory -> string list -> term list -> term list -> (thm list -> tactic) -> thm list + val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm (* FIXME remove *) val norm_hhf_plain: thm -> thm @@ -33,29 +35,36 @@ structure Goal: GOAL = struct -(* managing goal states *) +(** goals **) + +(* + -------- (init) + C ==> #C +*) +fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI; (* - ------------ (init) - C ==> Goal C + A ==> ... ==> C + ------------------ (protect) + #(A ==> ... ==> C) *) -fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI; +fun protect th = th COMP Drule.incr_indexes th Drule.protectI; (* - A ==> ... ==> Goal C - -------------------- (conclude) + A ==> ... ==> #C + ---------------- (conclude) A ==> ... ==> C *) fun conclude th = (case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1) - (Drule.incr_indexes_wrt [] [] [] [th] Drule.goalD) of + (Drule.incr_indexes th Drule.protectD) of SOME th' => th' | NONE => raise THM ("Failed to conclude goal", 0, [th])); (* - Goal C - ------ (finish) - C + #C + --- (finish) + C *) fun finish th = (case Thm.nprems_of th of @@ -65,24 +74,39 @@ ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); -(* prove_raw -- minimal result checks, no normalization *) + +(** results **) + +(* HHF normal form *) val norm_hhf_plain = (* FIXME remove *) (not o Drule.is_norm_hhf o Thm.prop_of) ? MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq]; -val norm_hhf_rule = +val norm_hhf = norm_hhf_plain #> Thm.adjust_maxidx_thm #> Drule.gen_all; -fun prove_raw casms cprop tac = - (case SINGLE (tac (map (norm_hhf_rule o Thm.assume) casms)) (init cprop) of - SOME th => Drule.implies_intr_list casms (finish th) - | NONE => raise ERROR_MESSAGE "Tactic failed."); + +(* composition of normal results *) + +fun compose_hhf tha i thb = + Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb; + +fun comp_hhf tha thb = + (case Seq.pull (compose_hhf tha 1 thb) of + SOME (th, _) => th + | NONE => raise THM ("comp_hhf", 1, [tha, thb])); + +fun compose_hhf_tac [] _ = no_tac + | compose_hhf_tac (th :: ths) i = PRIMSEQ (compose_hhf th i) APPEND compose_hhf_tac ths i; -(* tactical proving *) + +(** tactical theorem proving **) + +(* prove *) local @@ -107,7 +131,7 @@ val cparams = map (cert_safe o Free) params; val casms = map cert_safe asms; - val prems = map (norm_hhf_rule o Thm.assume) casms; + val prems = map (norm_hhf o Thm.assume) casms; val goal = init (cert_safe prop); val goal' = (case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed."); @@ -128,7 +152,7 @@ fun prove_multi thy xs asms prop tac = gen_prove (fn fixed_tfrees => Drule.zero_var_indexes o - (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule) + (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf) thy xs asms prop tac; fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac); @@ -139,6 +163,14 @@ end; +(* prove_raw -- no checks, no normalization of result! *) + +fun prove_raw casms cprop tac = + (case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of + SOME th => Drule.implies_intr_list casms (finish th) + | NONE => raise ERROR_MESSAGE "Tactic failed."); + + (* SELECT_GOAL *) (*Tactical for restricting the effect of a tactic to subgoal i. Works