src/Pure/goal.ML
changeset 23237 ac9d126456e1
parent 22902 ac833b4bb7ee
child 23356 dbe3731241c3
     1.1 --- a/src/Pure/goal.ML	Mon Jun 04 15:43:32 2007 +0200
     1.2 +++ b/src/Pure/goal.ML	Mon Jun 04 21:04:19 2007 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    val compose_hhf: thm -> int -> thm -> thm Seq.seq
     1.5    val compose_hhf_tac: thm -> int -> tactic
     1.6    val comp_hhf: thm -> thm -> thm
     1.7 +  val assume_rule_tac: Proof.context -> int -> tactic
     1.8  end;
     1.9  
    1.10  structure Goal: GOAL =
    1.11 @@ -236,6 +237,18 @@
    1.12    | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
    1.13    | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
    1.14  
    1.15 +
    1.16 +(* non-atomic goal assumptions *)
    1.17 +
    1.18 +fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
    1.19 +  let
    1.20 +    val ((_, goal'), ctxt') = Variable.focus goal ctxt;
    1.21 +    val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
    1.22 +    val Rs = filter_out (Logic.is_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
    1.23 +    val tacs = Rs |> map (fn R =>
    1.24 +      Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
    1.25 +  in fold_rev (curry op APPEND') tacs (K no_tac) i end);
    1.26 +
    1.27  end;
    1.28  
    1.29  structure BasicGoal: BASIC_GOAL = Goal;