5820

1 
(* Title: Pure/Isar/proof.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Proof states and methods.


6 


7 
TODO:


8 
 assume: improve schematic Vars handling (!?);


9 
 bind: check rhs (extra (T)Vars etc.) (How to handle these anyway?);


10 
 prep_result: avoid duplicate asms;


11 
 goal: need asms field? (may take from goal context!?);


12 
 finish: filter results (!??) (no?);


13 
 finish_tac: make a parameter (method) (!!?);


14 
 prep_result error: use error channel (!);


15 
 next_block: fetch_facts (!?);


16 
 warn_vars;


17 
 string constants in one place (e.g. "it", "thesis") (??!);


18 
 check_finished: trace results (!?);


19 
*)


20 


21 
signature PROOF =


22 
sig


23 
type context


24 
type state


25 
exception STATE of string * state


26 
val context_of: state > context


27 
val theory_of: state > theory


28 
val sign_of: state > Sign.sg


29 
val the_facts: state > tthm list


30 
val goal_facts: (state > tthm list) > state > state


31 
val use_facts: state > state


32 
val reset_facts: state > state


33 
val assert_backward: state > state


34 
val enter_forward: state > state


35 
val print_state: state > unit


36 
type method


37 
val method: (tthm list > thm >


38 
(thm * (indexname * term) list * (string * tthm list) list) Seq.seq) > method


39 
val refine: (context > method) > state > state Seq.seq


40 
val bind: (indexname * string) list > state > state


41 
val bind_i: (indexname * term) list > state > state


42 
val match_bind: (string * string) list > state > state


43 
val match_bind_i: (term * term) list > state > state


44 
val have_tthms: string > context attribute list >


45 
(tthm * context attribute list) list > state > state


46 
val assume: string > context attribute list > string list > state > state


47 
val assume_i: string > context attribute list > term list > state > state


48 
val fix: (string * string option) list > state > state


49 
val fix_i: (string * typ) list > state > state


50 
val theorem: bstring > theory attribute list > string > theory > state


51 
val theorem_i: bstring > theory attribute list > term > theory > state


52 
val lemma: bstring > theory attribute list > string > theory > state


53 
val lemma_i: bstring > theory attribute list > term > theory > state


54 
val chain: state > state


55 
val from_facts: tthm list > state > state


56 
val show: string > context attribute list > string > state > state


57 
val show_i: string > context attribute list > term > state > state


58 
val have: string > context attribute list > string > state > state


59 
val have_i: string > context attribute list > term > state > state


60 
val begin_block: state > state


61 
val next_block: state > state


62 
val end_block: (context > method) > state > state Seq.seq


63 
val qed: (context > method) > bstring option > theory attribute list option > state


64 
> theory * (string * string * tthm)


65 
end;


66 


67 
signature PROOF_PRIVATE =


68 
sig


69 
include PROOF


70 
val put_data: Object.kind > ('a > Object.T) > 'a > state > state


71 
end;


72 


73 


74 
structure Proof: PROOF_PRIVATE =


75 
struct


76 


77 


78 
(** proof state **)


79 


80 
type context = ProofContext.context;


81 


82 


83 
(* type goal *)


84 


85 
datatype kind =


86 
Theorem of theory attribute list  (*toplevel theorem*)


87 
Lemma of theory attribute list  (*toplevel lemma*)


88 
Goal of context attribute list  (*intermediate result, solving subgoal*)


89 
Aux of context attribute list ; (*intermediate result*)


90 


91 
val kind_name =


92 
fn Theorem _ => "theorem"  Lemma _ => "lemma"  Goal _ => "show"  Aux _ => "have";


93 


94 
type goal =


95 
(kind * (*result kind*)


96 
string * (*result name*)


97 
cterm list * (*result assumptions*)


98 
term) * (*result statement*)


99 
(tthm list * (*use facts*)


100 
thm); (*goal: subgoals ==> statement*)


101 


102 


103 
(* type mode *)


104 


105 
datatype mode = Forward  ForwardChain  Backward;


106 


107 
val mode_name =


108 
fn Forward => "forward"  ForwardChain => "forward chain"  Backward => "backward";


109 


110 


111 
(* type node *)


112 


113 
type node =


114 
{context: context,


115 
facts: tthm list option,


116 
mode: mode,


117 
goal: goal option};


118 


119 
fun make_node (context, facts, mode, goal) =


120 
{context = context, facts = facts, mode = mode, goal = goal}: node;


121 


122 


123 
(* datatype state *)


124 


125 
datatype state =


126 
State of


127 
node * (*current*)


128 
node list; (*parents wrt. block structure*)


129 


130 
exception STATE of string * state;


131 


132 
fun err_malformed name state =


133 
raise STATE (name ^ ": internal error  malformed proof state", state);


134 


135 


136 
fun map_current f (State ({context, facts, mode, goal}, nodes)) =


137 
State (make_node (f (context, facts, mode, goal)), nodes);


138 


139 
fun init_state thy =

5875

140 
State (make_node (ProofContext.init thy, None, Forward, None), []);

5820

141 


142 


143 


144 
(** basic proof state operations **)


145 


146 
(* context *)


147 


148 
fun context_of (State ({context, ...}, _)) = context;


149 
val theory_of = ProofContext.theory_of o context_of;


150 
val sign_of = ProofContext.sign_of o context_of;


151 


152 
fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));


153 


154 
fun map_context_result f (state as State ({context, facts, mode, goal}, nodes)) =


155 
let val (context', result) = f context


156 
in (State (make_node (context', facts, mode, goal), nodes), result) end;


157 


158 


159 
fun put_data kind f = map_context o ProofContext.put_data kind f;


160 
val declare_term = map_context o ProofContext.declare_term;


161 
val add_binds = map_context o ProofContext.add_binds_i;


162 
val put_tthms = map_context o ProofContext.put_tthms;


163 
val put_tthmss = map_context o ProofContext.put_tthmss;


164 


165 


166 
(* bind statements *)


167 


168 
fun bind_props bs state =


169 
let val mk_bind = map (fn (x, t) => ((Syntax.binding x, 0), t)) o ObjectLogic.dest_statement


170 
in state > add_binds (flat (map mk_bind bs)) end;


171 


172 
fun bind_tthms (name, tthms) state =


173 
let


174 
val props = map (#prop o Thm.rep_thm o Attribute.thm_of) tthms;


175 
val named_props =


176 
(case props of


177 
[prop] => [(name, prop)]


178 
 props => map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props));


179 
in state > bind_props named_props end;


180 


181 
fun let_tthms name_tthms state =


182 
state


183 
> put_tthms name_tthms


184 
> bind_tthms name_tthms;


185 


186 


187 
(* facts *)


188 


189 
fun the_facts (State ({facts = Some facts, ...}, _)) = facts


190 
 the_facts state = raise STATE ("No current facts available", state);


191 


192 
fun put_facts facts state =


193 
state


194 
> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))


195 
> let_tthms ("facts", if_none facts []);


196 


197 
val reset_facts = put_facts None;


198 


199 
fun have_facts (name, facts) state =


200 
state


201 
> put_facts (Some facts)


202 
> let_tthms (name, facts);


203 


204 
fun these_facts (state, ths) = have_facts ths state;


205 
fun fetch_facts (State ({facts, ...}, _)) = put_facts facts;


206 


207 


208 
(* goal *)


209 


210 
fun find_goal i (State ({goal = Some goal, ...}, _)) = (i, goal)


211 
 find_goal i (State ({goal = None, ...}, node :: nodes)) =


212 
find_goal (i + 1) (State (node, nodes))


213 
 find_goal _ (state as State (_, [])) = err_malformed "find_goal" state;


214 


215 
fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));


216 


217 
fun map_goal f (State ({context, facts, mode, goal = Some goal}, nodes)) =


218 
State (make_node (context, facts, mode, Some (f goal)), nodes)


219 
 map_goal f (State (nd, node :: nodes)) =


220 
let val State (node', nodes') = map_goal f (State (node, nodes))


221 
in State (nd, node' :: nodes') end


222 
 map_goal _ state = state;


223 


224 
fun goal_facts get state =


225 
state


226 
> map_goal (fn (result, (_, thm)) => (result, (get state, thm)));


227 


228 
fun use_facts state =


229 
state


230 
> goal_facts the_facts


231 
> reset_facts;


232 


233 


234 
(* mode *)


235 


236 
fun get_mode (State ({mode, ...}, _)) = mode;


237 
fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));


238 


239 
val enter_forward = put_mode Forward;


240 
val enter_forward_chain = put_mode ForwardChain;


241 
val enter_backward = put_mode Backward;


242 


243 
fun assert_mode pred state =


244 
let val mode = get_mode state in


245 
if pred mode then state


246 
else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state)


247 
end;


248 


249 
fun is_chain state = get_mode state = ForwardChain;


250 
val assert_forward = assert_mode (equal Forward);


251 
val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain);


252 
val assert_backward = assert_mode (equal Backward);


253 


254 


255 
(* blocks *)


256 


257 
fun open_block (State (node, nodes)) = State (node, node :: nodes);


258 


259 
fun new_block state =


260 
state


261 
> open_block


262 
> put_goal None;


263 


264 
fun close_block (State (_, node :: nodes)) = State (node, nodes)


265 
 close_block state = raise STATE ("Unbalanced block parentheses", state);


266 


267 


268 


269 
(** print_state **)


270 


271 
fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =


272 
let


273 
val prt_tthm = Attribute.pretty_tthm;


274 


275 
fun print_facts None = ()


276 
 print_facts (Some ths) =


277 
Pretty.writeln (Pretty.big_list "Current facts:" (map prt_tthm ths));


278 


279 
fun levels_up 0 = ""


280 
 levels_up i = " (" ^ string_of_int i ^ " levels up)";


281 


282 
fun print_goal (i, ((kind, name, _, _), (_, thm))) =


283 
(writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *)


284 
Locale.print_goals (! goals_limit) thm);


285 
in


286 
writeln ("Nesting level: " ^ string_of_int (length nodes div 1)); (* FIXME *)


287 
writeln "";


288 
ProofContext.print_context context;


289 
writeln "";


290 
print_facts facts;


291 
print_goal (find_goal 0 state);


292 
writeln "";


293 
writeln (mode_name mode ^ " mode")


294 
end;


295 


296 


297 


298 
(** proof steps **)


299 


300 
(* datatype method *)


301 


302 
datatype method = Method of


303 
tthm list > (*use facts*)


304 
thm (*goal: subgoals ==> statement*)


305 
> (thm * (*refined goal*)


306 
(indexname * term) list * (*new bindings*)


307 
(string * tthm list) list) (*new thms*)


308 
Seq.seq;


309 


310 
val method = Method;


311 


312 


313 
(* refine goal *)


314 


315 
fun check_sign sg state =


316 
if Sign.subsig (sg, sign_of state) then state


317 
else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);


318 


319 
fun refine meth_fun (state as State ({context, ...}, _)) =


320 
let


321 
val Method meth = meth_fun context;


322 
val (_, (result, (facts, thm))) = find_goal 0 state;


323 


324 
fun refn (thm', new_binds, new_thms) =


325 
state


326 
> check_sign (sign_of_thm thm')


327 
> map_goal (K (result, (facts, thm')))


328 
> add_binds new_binds


329 
> put_tthmss new_thms;


330 
in Seq.map refn (meth facts thm) end;


331 


332 


333 
(* prepare result *)


334 


335 
fun varify_frees names thm =


336 
let


337 
fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None


338 
 get_free _ (opt, _) = opt;


339 


340 
fun find_free t x = foldl_aterms (get_free x) (None, t);


341 


342 
val {sign, maxidx, prop, ...} = Thm.rep_thm thm;


343 
val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names);


344 
in


345 
thm


346 
> Drule.forall_intr_list frees


347 
> Drule.forall_elim_vars (maxidx + 1)


348 
end;


349 


350 
fun implies_elim_hyps thm =


351 
foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm));


352 


353 
fun prep_result state asms t raw_thm =


354 
let


355 
val ctxt = context_of state;


356 
fun err msg = raise STATE (msg, state);


357 


358 
val ngoals = Thm.nprems_of raw_thm;


359 
val _ =


360 
if ngoals = 0 then ()


361 
else (Locale.print_goals ngoals raw_thm; err (string_of_int ngoals ^ " unsolved goal(s)!"));


362 


363 
val thm =


364 
raw_thm RS Drule.rev_triv_goal


365 
> implies_elim_hyps


366 
> Drule.implies_intr_list asms


367 
> varify_frees (ProofContext.fixed_names ctxt);


368 


369 
val {hyps, prop, sign, ...} = Thm.rep_thm thm;


370 
val tsig = Sign.tsig_of sign;


371 
in


372 
(* FIXME


373 
if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then


374 
warning ("Proved a different theorem: " ^ Sign.string_of_term sign prop)


375 
else ();


376 
*)


377 
if not (null hyps) then


378 
err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))


379 
(* FIXME else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then


380 
err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)


381 
else thm


382 
end;


383 


384 


385 
(* prepare final result *)


386 


387 
fun strip_flexflex thm =


388 
Seq.hd (Thm.flexflex_rule thm) handle THM _ => thm;


389 


390 
fun final_result state pre_thm =


391 
let


392 
val thm =


393 
pre_thm


394 
> strip_flexflex


395 
> Thm.strip_shyps


396 
> Drule.standard;


397 


398 
val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm);


399 
val xshyps = Thm.extra_shyps thm;


400 
in


401 
if not (null xshyps) then


402 
raise STATE ("Extra sort hypotheses: " ^ commas (map str_of_sort xshyps), state)


403 
else thm


404 
end;


405 


406 


407 
(* solve goal *)


408 


409 
fun solve_goal rule state =


410 
let


411 
val (_, (result, (facts, thm))) = find_goal 0 state;


412 
val thms' = FIRSTGOAL (solve_tac [rule]) thm;


413 
in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;


414 


415 


416 


417 
(*** structured proof commands ***)


418 


419 
(** context **)


420 


421 
(* bind *)


422 


423 
fun gen_bind f x state =


424 
state


425 
> assert_forward


426 
> map_context (f x)


427 
> reset_facts;


428 


429 
val bind = gen_bind ProofContext.add_binds;


430 
val bind_i = gen_bind ProofContext.add_binds_i;


431 


432 
val match_bind = gen_bind ProofContext.match_binds;


433 
val match_bind_i = gen_bind ProofContext.match_binds_i;


434 


435 


436 
(* have_tthms *)


437 


438 
val def_name = fn "" => "it"  name => name;


439 


440 
fun have_tthms name atts ths_atts state =


441 
state


442 
> assert_forward


443 
> map_context_result (ProofContext.have_tthms (def_name name) atts ths_atts)


444 
> these_facts;


445 


446 


447 
(* fix *)


448 


449 
fun gen_fix f xs state =


450 
state


451 
> assert_forward


452 
> map_context (f xs)


453 
> reset_facts;


454 


455 
val fix = gen_fix ProofContext.fix;


456 
val fix_i = gen_fix ProofContext.fix_i;


457 


458 


459 
(* assume *)


460 


461 
fun gen_assume f name atts props state =


462 
state


463 
> assert_forward


464 
> map_context_result (f (def_name name) atts props)


465 
> these_facts


466 
> (fn st => let_tthms ("prems", ProofContext.assumptions (context_of st)) st);


467 


468 
val assume = gen_assume ProofContext.assume;


469 
val assume_i = gen_assume ProofContext.assume_i;


470 


471 


472 


473 
(** goals **)


474 


475 
(* forward chaining *)


476 


477 
fun chain state =


478 
state


479 
> assert_forward


480 
> enter_forward_chain;


481 


482 
fun from_facts facts state =


483 
state


484 
> put_facts (Some facts)


485 
> chain;


486 


487 


488 
(* setup goals *)


489 


490 
val read_prop = ProofContext.read_prop o context_of;


491 
val cert_prop = ProofContext.cert_prop o context_of;


492 


493 
fun setup_goal opt_block prep kind name atts raw_prop state =


494 
let


495 
val sign = sign_of state;


496 
val ctxt = context_of state;


497 


498 
val casms = map (#prop o Thm.crep_thm o Attribute.thm_of) (ProofContext.assumptions ctxt);


499 
val asms = map Thm.term_of casms;


500 


501 
val prop = Logic.list_implies (asms, prep state raw_prop);


502 
val cprop = Thm.cterm_of sign prop;


503 
val thm = Drule.mk_triv_goal cprop;


504 
in


505 
state


506 
> assert_forward_or_chain


507 
> enter_forward


508 
> opt_block


509 


510 
> declare_term prop


511 
> put_goal (Some ((kind atts, (def_name name), casms, prop), ([], thm)))


512 
> bind_props [("thesis", prop)]


513 
> (if is_chain state then use_facts else reset_facts)


514 


515 
> new_block


516 
> enter_backward


517 
end;


518 


519 


520 
(*global goals*)


521 
fun global_goal prep kind name atts x thy =


522 
setup_goal I prep kind name atts x (init_state thy);


523 


524 
val theorem = global_goal read_prop Theorem;


525 
val theorem_i = global_goal cert_prop Theorem;


526 
val lemma = global_goal read_prop Lemma;


527 
val lemma_i = global_goal cert_prop Lemma;


528 


529 


530 
(*local goals*)


531 
fun local_goal prep kind name atts x =


532 
setup_goal open_block prep kind name atts x;


533 


534 
val show = local_goal read_prop Goal;


535 
val show_i = local_goal cert_prop Goal;


536 
val have = local_goal read_prop Aux;


537 
val have_i = local_goal cert_prop Aux;


538 


539 


540 


541 
(** blocks **)


542 


543 
(* begin_block *)


544 


545 
fun begin_block state =


546 
state


547 
> assert_forward


548 
> new_block


549 
> reset_facts


550 
> open_block;


551 


552 


553 
(* next_block *)


554 


555 
fun next_block state =


556 
state


557 
> assert_forward


558 
> close_block


559 
> new_block;


560 


561 


562 


563 
(** conclusions **)


564 


565 
(* current goal *)


566 


567 
fun current_goal (State ({goal = Some goal, ...}, _)) = goal


568 
 current_goal state = raise STATE ("No current goal!", state);


569 


570 
fun assert_current_goal state = (current_goal state; state);


571 


572 
fun assert_bottom true (state as State (_, _ :: _)) =


573 
raise STATE ("Not at bottom of proof!", state)


574 
 assert_bottom false (state as State (_, [])) =


575 
raise STATE ("Already at bottom of proof!", state)


576 
 assert_bottom _ state = state;


577 


578 


579 
(* finish proof *)


580 


581 
fun check_finished state states =


582 
(case Seq.pull states of


583 
None => raise STATE ("Failed to finish proof", state)


584 
 Some s_sq => Seq.cons s_sq);


585 


586 
fun finish_proof bot meth_fun state =


587 
state


588 
> assert_forward


589 
> close_block


590 
> assert_bottom bot


591 
> assert_current_goal


592 
> refine meth_fun


593 
> check_finished state;


594 


595 


596 
(* conclude local proof *)


597 


598 
fun finish_local state =


599 
let


600 
val ((kind, name, asms, t), (_, raw_thm)) = current_goal state;


601 
val result = prep_result state asms t raw_thm;


602 
val (atts, opt_solve) =


603 
(case kind of


604 
Goal atts => (atts, solve_goal result)


605 
 Aux atts => (atts, Seq.single)


606 
 _ => raise STATE ("No local goal!", state));


607 
in


608 
state


609 
> close_block


610 
> have_tthms name atts [((result, []), [])]


611 
> opt_solve


612 
end;


613 


614 
fun end_block meth_fun state =


615 
if can assert_current_goal (close_block state) then


616 
state


617 
> finish_proof false meth_fun


618 
> (Seq.flat o Seq.map finish_local)


619 
else


620 
state


621 
> assert_forward


622 
> close_block


623 
> close_block


624 
> fetch_facts state


625 
> Seq.single;


626 


627 


628 
(* conclude global proof *)


629 


630 
fun finish_global alt_name alt_atts state =


631 
let


632 
val ((kind, def_name, asms, t), (_, raw_thm)) = current_goal state;


633 
val result = final_result state (prep_result state asms t raw_thm);


634 


635 
val name = if_none alt_name def_name;


636 
val atts =


637 
(case kind of


638 
Theorem atts => if_none alt_atts atts


639 
 Lemma atts => Attribute.tag_lemma :: if_none alt_atts atts


640 
 _ => raise STATE ("No global goal!", state));


641 


642 
val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state);


643 
in (thy', (kind_name kind, name, result')) end;


644 


645 
fun qed meth_fun alt_name alt_atts state =


646 
state


647 
> finish_proof true meth_fun


648 
> Seq.hd


649 
> finish_global alt_name alt_atts;


650 


651 


652 
end;
