removed ad-hoc atp_hook, cal_atp;
authorwenzelm
Wed Jul 13 16:07:35 2005 +0200 (2005-07-13)
changeset 1681367140ae50e77
parent 16812 c7d38e714768
child 16814 b829a6c9a87a
removed ad-hoc atp_hook, cal_atp;
removed depth_of;
tuned;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Jul 13 16:07:34 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jul 13 16:07:35 2005 +0200
     1.3 @@ -5,9 +5,6 @@
     1.4  The Isar/VM proof language interpreter.
     1.5  *)
     1.6  
     1.7 -
     1.8 -(*Jia Meng: added in atp_hook and modified enter_forward. *)
     1.9 -
    1.10  signature BASIC_PROOF =
    1.11  sig
    1.12    val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
    1.13 @@ -32,6 +29,7 @@
    1.14    val reset_thms: string -> state -> state
    1.15    val the_facts: state -> thm list
    1.16    val the_fact: state -> thm
    1.17 +  val thisN: string
    1.18    val get_goal: state -> context * (thm list * thm)
    1.19    val goal_facts: (state -> thm list) -> state -> state
    1.20    val get_mode: state -> mode
    1.21 @@ -40,11 +38,9 @@
    1.22    val assert_forward_or_chain: state -> state
    1.23    val assert_backward: state -> state
    1.24    val assert_no_chain: state -> state
    1.25 -  val atp_hook: (context * thm -> unit) ref
    1.26    val enter_forward: state -> state
    1.27    val show_main_goal: bool ref
    1.28    val verbose: bool ref
    1.29 -  val depth_of: state -> int
    1.30    val pretty_state: int -> state -> Pretty.T list
    1.31    val pretty_goals: bool -> state -> Pretty.T list
    1.32    val level: state -> int
    1.33 @@ -123,23 +119,18 @@
    1.34    val global_qed: (state -> state Seq.seq) -> state
    1.35      -> (theory * ((string * string) * (string * thm list) list)) Seq.seq
    1.36    val begin_block: state -> state
    1.37 +  val next_block: state -> state
    1.38    val end_block: state -> state Seq.seq
    1.39 -  val next_block: state -> state
    1.40 -  val thisN: string
    1.41 -  val call_atp: bool ref;
    1.42  end;
    1.43  
    1.44  structure Proof: PROOF =
    1.45  struct
    1.46  
    1.47 -(*Jia Meng: by default, no ATP is called. *)
    1.48 -val call_atp = ref false;
    1.49 +type context = ProofContext.context;
    1.50 +
    1.51  
    1.52  (** proof state **)
    1.53  
    1.54 -type context = ProofContext.context;
    1.55 -
    1.56 -
    1.57  (* type goal *)
    1.58  
    1.59  datatype kind =
    1.60 @@ -276,28 +267,6 @@
    1.61    let val (ctxt, (_, ((_, x), _))) = find_goal state
    1.62    in (ctxt, x) end;
    1.63  
    1.64 -
    1.65 -(*
    1.66 -(* Jia: added here: get all goals from the state 10/01/05 *)
    1.67 -fun find_all i (state as State (Node {goal = SOME goal, ...}, node::nodes)) =
    1.68 -    let val others = find_all (i+1) (State (node, nodes))
    1.69 -    in
    1.70 -        (context_of state, (i, goal)) :: others
    1.71 -    end
    1.72 -  | find_all i (State (Node {goal = NONE, ...}, node :: nodes)) = find_all (i + 1) (State (node, nodes))
    1.73 -  | find_all _ (state as State (_, [])) = [];
    1.74 -
    1.75 -val find_all_goals = find_all 0;
    1.76 -
    1.77 -fun find_all_goals_ctxts state =
    1.78 -    let val all_goals = find_all_goals state
    1.79 -        fun find_ctxt_g [] = []
    1.80 -          | find_ctxt_g ((ctxt, (_, ((_, (_, thm)), _)))::others) = (ctxt,thm) :: (find_ctxt_g others)
    1.81 -    in
    1.82 -        find_ctxt_g all_goals
    1.83 -    end;
    1.84 -*)
    1.85 -
    1.86  fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
    1.87  
    1.88  fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) =
    1.89 @@ -322,7 +291,7 @@
    1.90  fun get_mode (State (Node {mode, ...}, _)) = mode;
    1.91  fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
    1.92  
    1.93 -val enter_forward_aux = put_mode Forward;
    1.94 +val enter_forward = put_mode Forward;
    1.95  val enter_forward_chain = put_mode ForwardChain;
    1.96  val enter_backward = put_mode Backward;
    1.97  
    1.98 @@ -340,30 +309,6 @@
    1.99  val assert_no_chain = assert_mode (not_equal ForwardChain);
   1.100  
   1.101  
   1.102 -(*Jia Meng: a hook to be used for calling ATPs. *)
   1.103 -(* send the entire proof context *)
   1.104 -val atp_hook = ref (fn ctxt_state: ProofContext.context * Thm.thm => ());
   1.105 -
   1.106 -(*Jia Meng: the modified version of enter_forward. *)
   1.107 -(*Jia Meng: atp: Proof.state -> unit *)
   1.108 -local
   1.109 - fun atp state =
   1.110 -     let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
   1.111 -     in
   1.112 -         (!atp_hook) (ctxt,thm)
   1.113 -     end;
   1.114 -
   1.115 -in
   1.116 -
   1.117 - fun enter_forward state =
   1.118 -   if (!call_atp) then
   1.119 -   ((atp state; enter_forward_aux state)
   1.120 -                           handle (STATE _) => enter_forward_aux state)
   1.121 -       else (enter_forward_aux state);
   1.122 -
   1.123 -end;
   1.124 -
   1.125 -
   1.126  (* blocks *)
   1.127  
   1.128  fun level (State (_, nodes)) = length nodes;
   1.129 @@ -386,15 +331,13 @@
   1.130  val verbose = ProofContext.verbose;
   1.131  
   1.132  
   1.133 -fun depth_of (State (_, nodes)) = length nodes div 2 - 1;
   1.134 -
   1.135  val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp;
   1.136  
   1.137  fun pretty_facts _ _ NONE = []
   1.138    | pretty_facts s ctxt (SOME ths) =
   1.139        [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
   1.140  
   1.141 -fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, _)) =
   1.142 +fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) =
   1.143    let
   1.144      val ref (_, _, begin_goal) = Display.current_goals_markers;
   1.145  
   1.146 @@ -425,7 +368,7 @@
   1.147  
   1.148      val prts =
   1.149       [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
   1.150 -        (if ! verbose then ", depth " ^ string_of_int (depth_of state)
   1.151 +        (if ! verbose then ", depth " ^ string_of_int (length nodes div 2 - 1)
   1.152          else "")), Pretty.str ""] @
   1.153       (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
   1.154       (if ! verbose orelse mode = Forward then
   1.155 @@ -566,17 +509,23 @@
   1.156  
   1.157  (* bind *)
   1.158  
   1.159 -fun gen_bind f x state =
   1.160 +local
   1.161 +
   1.162 +fun gen_bind f args state =
   1.163    state
   1.164    |> assert_forward
   1.165 -  |> map_context (f x)
   1.166 +  |> map_context (f args)
   1.167    |> reset_facts;
   1.168  
   1.169 +in
   1.170 +
   1.171  val match_bind = gen_bind (ProofContext.match_bind false);
   1.172  val match_bind_i = gen_bind (ProofContext.match_bind_i false);
   1.173  val let_bind = gen_bind (ProofContext.match_bind true);
   1.174  val let_bind_i = gen_bind (ProofContext.match_bind_i true);
   1.175  
   1.176 +end;
   1.177 +
   1.178  
   1.179  (* note_thmss *)
   1.180  
   1.181 @@ -636,24 +585,34 @@
   1.182  
   1.183  (* fix *)
   1.184  
   1.185 -fun gen_fix f xs state =
   1.186 +local
   1.187 +
   1.188 +fun gen_fix f args state =
   1.189    state
   1.190    |> assert_forward
   1.191 -  |> map_context (f xs)
   1.192 +  |> map_context (f args)
   1.193    |> reset_facts;
   1.194  
   1.195 +in
   1.196 +
   1.197  val fix = gen_fix ProofContext.fix;
   1.198  val fix_i = gen_fix ProofContext.fix_i;
   1.199  
   1.200 +end;
   1.201 +
   1.202  
   1.203  (* assume and presume *)
   1.204  
   1.205 +local
   1.206 +
   1.207  fun gen_assume f exp args state =
   1.208    state
   1.209    |> assert_forward
   1.210    |> map_context_result (f exp args)
   1.211    |> these_factss;
   1.212  
   1.213 +in
   1.214 +
   1.215  val assm = gen_assume ProofContext.assume;
   1.216  val assm_i = gen_assume ProofContext.assume_i;
   1.217  val assume = assm ProofContext.export_assume;
   1.218 @@ -661,10 +620,14 @@
   1.219  val presume = assm ProofContext.export_presume;
   1.220  val presume_i = assm_i ProofContext.export_presume;
   1.221  
   1.222 +end;
   1.223 +
   1.224  
   1.225  
   1.226  (** local definitions **)
   1.227  
   1.228 +local
   1.229 +
   1.230  fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state =
   1.231    let
   1.232      val _ = assert_forward state;
   1.233 @@ -685,9 +648,13 @@
   1.234      |> assm_i ProofContext.export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
   1.235    end;
   1.236  
   1.237 +in
   1.238 +
   1.239  val def = gen_def fix ProofContext.read_term ProofContext.read_term_pats;
   1.240  val def_i = gen_def fix_i ProofContext.cert_term ProofContext.cert_term_pats;
   1.241  
   1.242 +end;
   1.243 +
   1.244  
   1.245  (* invoke_case *)
   1.246  
   1.247 @@ -726,6 +693,8 @@
   1.248  
   1.249  (* setup goals *)
   1.250  
   1.251 +local
   1.252 +
   1.253  val rule_contextN = "rule_context";
   1.254  
   1.255  fun setup_goal opt_block prepp autofix kind after_qed pr names raw_propp state =
   1.256 @@ -767,7 +736,6 @@
   1.257      |> enter_backward
   1.258    end;
   1.259  
   1.260 -(*global goals*)
   1.261  fun global_goal prep kind after_global export raw_locale a elems concl thy =
   1.262    let
   1.263      val init = init_state thy;
   1.264 @@ -789,11 +757,6 @@
   1.265        true (map (fst o fst) concl) propp
   1.266    end;
   1.267  
   1.268 -val multi_theorem = global_goal Locale.read_context_statement;
   1.269 -val multi_theorem_i = global_goal Locale.cert_context_statement;
   1.270 -
   1.271 -
   1.272 -(*local goals*)
   1.273  fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state =
   1.274    state
   1.275    |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
   1.276 @@ -803,11 +766,17 @@
   1.277  
   1.278  fun local_goal prepp kind f pr args = local_goal' prepp kind (K I) f pr args false;
   1.279  
   1.280 +in
   1.281 +
   1.282 +val multi_theorem = global_goal Locale.read_context_statement;
   1.283 +val multi_theorem_i = global_goal Locale.cert_context_statement;
   1.284  val show = local_goal' ProofContext.bind_propp Show;
   1.285  val show_i = local_goal' ProofContext.bind_propp_i Show;
   1.286  val have = local_goal ProofContext.bind_propp Have;
   1.287  val have_i = local_goal ProofContext.bind_propp_i Have;
   1.288  
   1.289 +end;
   1.290 +
   1.291  
   1.292  
   1.293  (** conclusions **)
   1.294 @@ -931,16 +900,18 @@
   1.295  
   1.296  (** blocks **)
   1.297  
   1.298 -(* begin_block *)
   1.299 -
   1.300  fun begin_block state =
   1.301    state
   1.302    |> assert_forward
   1.303    |> new_block
   1.304    |> open_block;
   1.305  
   1.306 -
   1.307 -(* end_block *)
   1.308 +fun next_block state =
   1.309 +  state
   1.310 +  |> assert_forward
   1.311 +  |> close_block
   1.312 +  |> new_block
   1.313 +  |> reset_facts;
   1.314  
   1.315  fun end_block state =
   1.316    state
   1.317 @@ -950,17 +921,6 @@
   1.318    |> close_block
   1.319    |> transfer_facts state;
   1.320  
   1.321 -
   1.322 -(* next_block *)
   1.323 -
   1.324 -fun next_block state =
   1.325 -  state
   1.326 -  |> assert_forward
   1.327 -  |> close_block
   1.328 -  |> new_block
   1.329 -  |> reset_facts;
   1.330 -
   1.331 -
   1.332  end;
   1.333  
   1.334  structure BasicProof: BASIC_PROOF = Proof;