src/Pure/goal.ML
changeset 19423 51eeee99bd8f
parent 19221 aab0c0399e91
child 19482 9f11af8f7ef9
equal deleted inserted replaced
19422:bba26da0f227 19423:51eeee99bd8f
   145 
   145 
   146     val prop' = Thm.prop_of raw_result;
   146     val prop' = Thm.prop_of raw_result;
   147     val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
   147     val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
   148       err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   148       err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   149   in
   149   in
   150     hd (Drule.conj_elim_precise [length props] raw_result)
   150     hd (Conjunction.elim_precise [length props] raw_result)
   151     |> map
   151     |> map
   152       (Drule.implies_intr_list casms
   152       (Drule.implies_intr_list casms
   153         #> Drule.forall_intr_list cparams
   153         #> Drule.forall_intr_list cparams
   154         #> norm_hhf
   154         #> norm_hhf
   155         #> Thm.varifyT' fixed_tfrees
   155         #> Thm.varifyT' fixed_tfrees
   174 (** local goal states **)
   174 (** local goal states **)
   175 
   175 
   176 fun extract i n st =
   176 fun extract i n st =
   177   (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
   177   (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
   178    else if n = 1 then Seq.single (Thm.cprem_of st i)
   178    else if n = 1 then Seq.single (Thm.cprem_of st i)
   179    else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
   179    else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
   180   |> Seq.map (Thm.adjust_maxidx #> init);
   180   |> Seq.map (Thm.adjust_maxidx #> init);
   181 
   181 
   182 fun retrofit i n st' st =
   182 fun retrofit i n st' st =
   183   (if n = 1 then st
   183   (if n = 1 then st
   184    else st |> Drule.rotate_prems (i - 1) |> Drule.conj_uncurry n |> Drule.rotate_prems (1 - i))
   184    else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
   185   |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
   185   |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
   186 
   186 
   187 fun SELECT_GOAL tac i st =
   187 fun SELECT_GOAL tac i st =
   188   if Thm.nprems_of st = 1 andalso i = 1 then tac st
   188   if Thm.nprems_of st = 1 andalso i = 1 then tac st
   189   else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
   189   else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;