src/Pure/goal.ML
changeset 52223 5bb6ae8acb87
parent 52104 250cd2a9308d
child 52456 960202346d0c
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
    54   val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    54   val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    55   val conjunction_tac: int -> tactic
    55   val conjunction_tac: int -> tactic
    56   val precise_conjunction_tac: int -> int -> tactic
    56   val precise_conjunction_tac: int -> int -> tactic
    57   val recover_conjunction_tac: tactic
    57   val recover_conjunction_tac: tactic
    58   val norm_hhf_tac: int -> tactic
    58   val norm_hhf_tac: int -> tactic
    59   val compose_hhf_tac: thm -> int -> tactic
       
    60   val assume_rule_tac: Proof.context -> int -> tactic
    59   val assume_rule_tac: Proof.context -> int -> tactic
    61 end;
    60 end;
    62 
    61 
    63 structure Goal: GOAL =
    62 structure Goal: GOAL =
    64 struct
    63 struct
   357   |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
   356   |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
   358 
   357 
   359 fun retrofit i n st' st =
   358 fun retrofit i n st' st =
   360   (if n = 1 then st
   359   (if n = 1 then st
   361    else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
   360    else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
   362   |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
   361   |> Thm.bicompose {flatten = false, match = false, incremented = false}
       
   362       (false, conclude st', Thm.nprems_of st') i;
   363 
   363 
   364 fun SELECT_GOAL tac i st =
   364 fun SELECT_GOAL tac i st =
   365   if Thm.nprems_of st = 1 andalso i = 1 then tac st
   365   if Thm.nprems_of st = 1 andalso i = 1 then tac st
   366   else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
   366   else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
   367 
   367 
   400 val norm_hhf_tac =
   400 val norm_hhf_tac =
   401   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   401   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   402   THEN' SUBGOAL (fn (t, i) =>
   402   THEN' SUBGOAL (fn (t, i) =>
   403     if Drule.is_norm_hhf t then all_tac
   403     if Drule.is_norm_hhf t then all_tac
   404     else rewrite_goal_tac Drule.norm_hhf_eqs i);
   404     else rewrite_goal_tac Drule.norm_hhf_eqs i);
   405 
       
   406 fun compose_hhf_tac th i st =
       
   407   PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
       
   408 
   405 
   409 
   406 
   410 (* non-atomic goal assumptions *)
   407 (* non-atomic goal assumptions *)
   411 
   408 
   412 fun non_atomic (Const ("==>", _) $ _ $ _) = true
   409 fun non_atomic (Const ("==>", _) $ _ $ _) = true