equal
deleted
inserted
replaced
37 val pretty_state: int -> state -> Pretty.T list |
37 val pretty_state: int -> state -> Pretty.T list |
38 val pretty_goals: bool -> state -> Pretty.T list |
38 val pretty_goals: bool -> state -> Pretty.T list |
39 val refine: Method.text -> state -> state Seq.seq |
39 val refine: Method.text -> state -> state Seq.seq |
40 val refine_end: Method.text -> state -> state Seq.seq |
40 val refine_end: Method.text -> state -> state Seq.seq |
41 val refine_insert: thm list -> state -> state |
41 val refine_insert: thm list -> state -> state |
|
42 val goal_tac: thm -> int -> tactic |
42 val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq |
43 val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq |
43 val match_bind: (string list * string) list -> state -> state |
44 val match_bind: (string list * string) list -> state -> state |
44 val match_bind_i: (term list * term) list -> state -> state |
45 val match_bind_i: (term list * term) list -> state -> state |
45 val let_bind: (string list * string) list -> state -> state |
46 val let_bind: (string list * string) list -> state -> state |
46 val let_bind_i: (term list * term) list -> state -> state |
47 val let_bind_i: (term list * term) list -> state -> state |
442 end; |
443 end; |
443 |
444 |
444 |
445 |
445 (* refine via sub-proof *) |
446 (* refine via sub-proof *) |
446 |
447 |
447 local |
448 fun goal_tac rule = |
448 |
|
449 fun refine_tac rule = |
|
450 Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW |
449 Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW |
451 (Tactic.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) => |
450 (Tactic.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) => |
452 if can Logic.unprotect (Logic.strip_assums_concl goal) then |
451 if can Logic.unprotect (Logic.strip_assums_concl goal) then |
453 Tactic.etac Drule.protectI i |
452 Tactic.etac Drule.protectI i |
454 else all_tac))); |
453 else all_tac))); |
455 |
454 |
456 in |
|
457 |
|
458 fun refine_goals print_rule inner raw_rules state = |
455 fun refine_goals print_rule inner raw_rules state = |
459 let |
456 let |
460 val (outer, (_, goal)) = get_goal state; |
457 val (outer, (_, goal)) = get_goal state; |
461 fun refine rule st = (print_rule outer rule; FINDGOAL (refine_tac rule) st); |
458 fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st); |
462 in |
459 in |
463 raw_rules |
460 raw_rules |
464 |> ProofContext.goal_exports inner outer |
461 |> ProofContext.goal_exports inner outer |
465 |> Seq.maps (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state) |
462 |> Seq.maps (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state) |
466 end; |
463 end; |
467 |
|
468 end; |
|
469 |
464 |
470 |
465 |
471 (* conclude_goal *) |
466 (* conclude_goal *) |
472 |
467 |
473 fun conclude_goal state goal propss = |
468 fun conclude_goal state goal propss = |