# HG changeset patch # User wenzelm # Date 964954536 -7200 # Node ID 8058d285b1cdd2d18539d4613a7a5b746d987c30 # Parent 9adbcf6375c165d784fa2aad876301085975b1ea export RANGE, hard_asm_tac, soft_asm_tac; export is_chain, assert_forward_or_chain; added the_fact; updated ProofContext.export_wrt; diff -r 9adbcf6375c1 -r 8058d285b1cd src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sun Jul 30 12:54:07 2000 +0200 +++ b/src/Pure/Isar/proof.ML Sun Jul 30 12:55:36 2000 +0200 @@ -8,6 +8,7 @@ signature BASIC_PROOF = sig + val RANGE: (int -> tactic) list -> int -> tactic val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq end; @@ -26,11 +27,14 @@ val warn_extra_tfrees: state -> state -> state val reset_thms: string -> state -> state val the_facts: state -> thm list + val the_fact: state -> thm val get_goal: state -> term * (thm list * thm) val goal_facts: (state -> thm list) -> state -> state val use_facts: state -> state val reset_facts: state -> state + val is_chain: state -> bool val assert_forward: state -> state + val assert_forward_or_chain: state -> state val assert_backward: state -> state val assert_no_chain: state -> state val enter_forward: state -> state @@ -57,10 +61,12 @@ (thm list * context attribute list) list) list -> state -> state val fix: (string list * string option) list -> state -> state val fix_i: (string list * typ option) list -> state -> state - val assm: (int -> tactic) * (int -> tactic) + val hard_asm_tac: int -> tactic + val soft_asm_tac: int -> tactic + val assm: ProofContext.exporter -> (string * context attribute list * (string * (string list * string list)) list) list -> state -> state - val assm_i: (int -> tactic) * (int -> tactic) + val assm_i: ProofContext.exporter -> (string * context attribute list * (term * (term list * term list)) list) list -> state -> state val assume: (string * context attribute list * (string * (string list * string list)) list) list @@ -207,6 +213,11 @@ fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts | the_facts state = raise STATE ("No current facts available", state); +fun the_fact state = + (case the_facts state of + [thm] => thm + | _ => raise STATE ("Single fact expected", state)); + fun assert_facts state = (the_facts state; state); fun get_facts (State (Node {facts, ...}, _)) = facts; @@ -380,7 +391,7 @@ end; -(* export results *) +(* tacticals *) fun RANGE [] _ = all_tac | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; @@ -391,19 +402,23 @@ fun HEADGOAL tac = tac 1; + +(* export results *) + fun export_goal print_rule raw_rule inner state = let val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state; - val (exp, tacs) = ProofContext.export_wrt inner (Some outer); - val rule = exp raw_rule; - val _ = print_rule rule; - val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm; - in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; - + val (exp_tac, tacs) = ProofContext.export_wrt true inner (Some outer); + fun exp_rule rule = + let + val _ = print_rule rule; + val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE tacs) thm; + in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; + in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end; fun export_thm inner thm = - let val (exp, tacs) = ProofContext.export_wrt inner None in - (case Seq.chop (2, RANGE (map #2 tacs) 1 (exp thm)) of + let val (exp_tac, tacs) = ProofContext.export_wrt false inner None in + (case Seq.chop (2, (exp_tac THEN RANGE tacs 1) thm) of ([thm'], _) => thm' | ([], _) => raise THM ("export: failed", 0, [thm]) | _ => raise THM ("export: more than one result", 0, [thm])) @@ -414,9 +429,9 @@ None => Seq.single (reset_facts state) | Some thms => let - val (exp, tacs) = - ProofContext.export_wrt (context_of inner_state) (Some (context_of state)); - val thmqs = map (RANGE (map #2 tacs) 1 o exp) thms; + val (exp_tac, tacs) = + ProofContext.export_wrt false (context_of inner_state) (Some (context_of state)); + val thmqs = map (exp_tac THEN RANGE tacs 1) thms; in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end); @@ -436,7 +451,7 @@ val {hyps, prop, sign, ...} = Thm.rep_thm thm; val tsig = Sign.tsig_of sign; - val casms = map #1 (assumptions state); + val casms = flat (map #1 (assumptions state)); val bad_hyps = Library.gen_rems Term.aconv (hyps, map (Thm.term_of o Drule.mk_cgoal) casms); in if not (null bad_hyps) then @@ -497,26 +512,30 @@ local -fun gen_assume f tac args state = +fun gen_assume f exp args state = state |> assert_forward - |> map_context_result (f tac args) + |> map_context_result (f exp args) |> (fn (st, (factss, prems)) => these_factss (st, factss) |> put_thms ("prems", prems)); -val hard_asm_tac = Tactic.etac Drule.triv_goal; -val soft_asm_tac = Tactic.rtac Drule.triv_goal - THEN' Tactic.rtac asm_rl; (* FIXME hack to norm goal *) +fun simple_exporter tac1 tac2 = + (Seq.single oo Drule.implies_intr_list, + fn is_goal => fn n => replicate n (if is_goal then tac1 else tac2)); in +val hard_asm_tac = Tactic.etac Drule.triv_goal; +val soft_asm_tac = Tactic.rtac Drule.triv_goal; + (* THEN' Tactic.rtac asm_rl FIXME hack to norm goal *) + val assm = gen_assume ProofContext.assume; val assm_i = gen_assume ProofContext.assume_i; -val assume = assm (hard_asm_tac, soft_asm_tac); -val assume_i = assm_i (hard_asm_tac, soft_asm_tac); -val presume = assm (soft_asm_tac, soft_asm_tac); -val presume_i = assm_i (soft_asm_tac, soft_asm_tac); +val assume = assm (simple_exporter hard_asm_tac soft_asm_tac); +val assume_i = assm_i (simple_exporter hard_asm_tac soft_asm_tac); +val presume = assm (simple_exporter soft_asm_tac soft_asm_tac); +val presume_i = assm_i (simple_exporter soft_asm_tac soft_asm_tac); end; @@ -638,6 +657,8 @@ val outer_ctxt = context_of outer_state; val result = prep_result state t raw_thm; + val resultq = #1 (ProofContext.export_wrt false goal_ctxt (Some outer_ctxt)) result; + val (atts, opt_solve) = (case kind of Goal atts => (atts, export_goal print_rule result goal_ctxt) @@ -647,9 +668,9 @@ print_result {kind = kind_name kind, name = name, thm = result}; outer_state |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t] - |> have_thmss [((name, atts), [Thm.no_attributes - [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]])] - |> opt_solve + |> (fn st => Seq.map (fn res => + have_thmss [((name, atts), [Thm.no_attributes [res]])] st) resultq) + |> (Seq.flat o Seq.map opt_solve) |> (Seq.flat o Seq.map after_qed) end;