# HG changeset patch # User wenzelm # Date 1121263655 -7200 # Node ID 67140ae50e77b41546fb086033b08556144fe21c # Parent c7d38e7147683f997b9a6aef8ab9d18d713af16f removed ad-hoc atp_hook, cal_atp; removed depth_of; tuned; diff -r c7d38e714768 -r 67140ae50e77 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Jul 13 16:07:34 2005 +0200 +++ b/src/Pure/Isar/proof.ML Wed Jul 13 16:07:35 2005 +0200 @@ -5,9 +5,6 @@ The Isar/VM proof language interpreter. *) - -(*Jia Meng: added in atp_hook and modified enter_forward. *) - signature BASIC_PROOF = sig val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq @@ -32,6 +29,7 @@ val reset_thms: string -> state -> state val the_facts: state -> thm list val the_fact: state -> thm + val thisN: string val get_goal: state -> context * (thm list * thm) val goal_facts: (state -> thm list) -> state -> state val get_mode: state -> mode @@ -40,11 +38,9 @@ val assert_forward_or_chain: state -> state val assert_backward: state -> state val assert_no_chain: state -> state - val atp_hook: (context * thm -> unit) ref val enter_forward: state -> state val show_main_goal: bool ref val verbose: bool ref - val depth_of: state -> int val pretty_state: int -> state -> Pretty.T list val pretty_goals: bool -> state -> Pretty.T list val level: state -> int @@ -123,23 +119,18 @@ val global_qed: (state -> state Seq.seq) -> state -> (theory * ((string * string) * (string * thm list) list)) Seq.seq val begin_block: state -> state + val next_block: state -> state val end_block: state -> state Seq.seq - val next_block: state -> state - val thisN: string - val call_atp: bool ref; end; structure Proof: PROOF = struct -(*Jia Meng: by default, no ATP is called. *) -val call_atp = ref false; +type context = ProofContext.context; + (** proof state **) -type context = ProofContext.context; - - (* type goal *) datatype kind = @@ -276,28 +267,6 @@ let val (ctxt, (_, ((_, x), _))) = find_goal state in (ctxt, x) end; - -(* -(* Jia: added here: get all goals from the state 10/01/05 *) -fun find_all i (state as State (Node {goal = SOME goal, ...}, node::nodes)) = - let val others = find_all (i+1) (State (node, nodes)) - in - (context_of state, (i, goal)) :: others - end - | find_all i (State (Node {goal = NONE, ...}, node :: nodes)) = find_all (i + 1) (State (node, nodes)) - | find_all _ (state as State (_, [])) = []; - -val find_all_goals = find_all 0; - -fun find_all_goals_ctxts state = - let val all_goals = find_all_goals state - fun find_ctxt_g [] = [] - | find_ctxt_g ((ctxt, (_, ((_, (_, thm)), _)))::others) = (ctxt,thm) :: (find_ctxt_g others) - in - find_ctxt_g all_goals - end; -*) - fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal)); fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = @@ -322,7 +291,7 @@ fun get_mode (State (Node {mode, ...}, _)) = mode; fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal)); -val enter_forward_aux = put_mode Forward; +val enter_forward = put_mode Forward; val enter_forward_chain = put_mode ForwardChain; val enter_backward = put_mode Backward; @@ -340,30 +309,6 @@ val assert_no_chain = assert_mode (not_equal ForwardChain); -(*Jia Meng: a hook to be used for calling ATPs. *) -(* send the entire proof context *) -val atp_hook = ref (fn ctxt_state: ProofContext.context * Thm.thm => ()); - -(*Jia Meng: the modified version of enter_forward. *) -(*Jia Meng: atp: Proof.state -> unit *) -local - fun atp state = - let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state - in - (!atp_hook) (ctxt,thm) - end; - -in - - fun enter_forward state = - if (!call_atp) then - ((atp state; enter_forward_aux state) - handle (STATE _) => enter_forward_aux state) - else (enter_forward_aux state); - -end; - - (* blocks *) fun level (State (_, nodes)) = length nodes; @@ -386,15 +331,13 @@ val verbose = ProofContext.verbose; -fun depth_of (State (_, nodes)) = length nodes div 2 - 1; - val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp; fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) = [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""]; -fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, _)) = +fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) = let val ref (_, _, begin_goal) = Display.current_goals_markers; @@ -425,7 +368,7 @@ val prts = [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ - (if ! verbose then ", depth " ^ string_of_int (depth_of state) + (if ! verbose then ", depth " ^ string_of_int (length nodes div 2 - 1) else "")), Pretty.str ""] @ (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @ (if ! verbose orelse mode = Forward then @@ -566,17 +509,23 @@ (* bind *) -fun gen_bind f x state = +local + +fun gen_bind f args state = state |> assert_forward - |> map_context (f x) + |> map_context (f args) |> reset_facts; +in + val match_bind = gen_bind (ProofContext.match_bind false); val match_bind_i = gen_bind (ProofContext.match_bind_i false); val let_bind = gen_bind (ProofContext.match_bind true); val let_bind_i = gen_bind (ProofContext.match_bind_i true); +end; + (* note_thmss *) @@ -636,24 +585,34 @@ (* fix *) -fun gen_fix f xs state = +local + +fun gen_fix f args state = state |> assert_forward - |> map_context (f xs) + |> map_context (f args) |> reset_facts; +in + val fix = gen_fix ProofContext.fix; val fix_i = gen_fix ProofContext.fix_i; +end; + (* assume and presume *) +local + fun gen_assume f exp args state = state |> assert_forward |> map_context_result (f exp args) |> these_factss; +in + val assm = gen_assume ProofContext.assume; val assm_i = gen_assume ProofContext.assume_i; val assume = assm ProofContext.export_assume; @@ -661,10 +620,14 @@ val presume = assm ProofContext.export_presume; val presume_i = assm_i ProofContext.export_presume; +end; + (** local definitions **) +local + fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state = let val _ = assert_forward state; @@ -685,9 +648,13 @@ |> assm_i ProofContext.export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])] end; +in + val def = gen_def fix ProofContext.read_term ProofContext.read_term_pats; val def_i = gen_def fix_i ProofContext.cert_term ProofContext.cert_term_pats; +end; + (* invoke_case *) @@ -726,6 +693,8 @@ (* setup goals *) +local + val rule_contextN = "rule_context"; fun setup_goal opt_block prepp autofix kind after_qed pr names raw_propp state = @@ -767,7 +736,6 @@ |> enter_backward end; -(*global goals*) fun global_goal prep kind after_global export raw_locale a elems concl thy = let val init = init_state thy; @@ -789,11 +757,6 @@ true (map (fst o fst) concl) propp end; -val multi_theorem = global_goal Locale.read_context_statement; -val multi_theorem_i = global_goal Locale.cert_context_statement; - - -(*local goals*) fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state = state |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args)) @@ -803,11 +766,17 @@ fun local_goal prepp kind f pr args = local_goal' prepp kind (K I) f pr args false; +in + +val multi_theorem = global_goal Locale.read_context_statement; +val multi_theorem_i = global_goal Locale.cert_context_statement; val show = local_goal' ProofContext.bind_propp Show; val show_i = local_goal' ProofContext.bind_propp_i Show; val have = local_goal ProofContext.bind_propp Have; val have_i = local_goal ProofContext.bind_propp_i Have; +end; + (** conclusions **) @@ -931,16 +900,18 @@ (** blocks **) -(* begin_block *) - fun begin_block state = state |> assert_forward |> new_block |> open_block; - -(* end_block *) +fun next_block state = + state + |> assert_forward + |> close_block + |> new_block + |> reset_facts; fun end_block state = state @@ -950,17 +921,6 @@ |> close_block |> transfer_facts state; - -(* next_block *) - -fun next_block state = - state - |> assert_forward - |> close_block - |> new_block - |> reset_facts; - - end; structure BasicProof: BASIC_PROOF = Proof;