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 (!?);

5918

9 
 warn_vars;

5820

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


11 
 prep_result: avoid duplicate asms;


12 
 prep_result error: use error channel (!);

5918

13 
 check_finished: trace results (!?);

5820

14 
 next_block: fetch_facts (!?);


15 
*)


16 


17 
signature PROOF =


18 
sig


19 
type context


20 
type state


21 
exception STATE of string * state


22 
val context_of: state > context


23 
val theory_of: state > theory


24 
val sign_of: state > Sign.sg


25 
val the_facts: state > tthm list


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


27 
val use_facts: state > state


28 
val reset_facts: state > state


29 
val assert_backward: state > state


30 
val enter_forward: state > state


31 
val print_state: state > unit


32 
type method


33 
val method: (tthm list > thm >


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


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


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


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


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


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

5918

40 
val have_tthmss: string > context attribute list >


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

5820

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


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


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


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


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


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


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


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


50 
val chain: state > state


51 
val from_facts: tthm list > state > state


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


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


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


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


56 
val begin_block: state > state


57 
val next_block: state > state


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


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


60 
> theory * (string * string * tthm)


61 
end;


62 


63 
signature PROOF_PRIVATE =


64 
sig


65 
include PROOF


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


67 
end;


68 


69 
structure Proof: PROOF_PRIVATE =


70 
struct


71 


72 


73 
(** proof state **)


74 


75 
type context = ProofContext.context;


76 


77 


78 
(* type goal *)


79 


80 
datatype kind =


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


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


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


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


85 


86 
val kind_name =


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


88 


89 
type goal =


90 
(kind * (*result kind*)


91 
string * (*result name*)


92 
cterm list * (*result assumptions*)


93 
term) * (*result statement*)


94 
(tthm list * (*use facts*)


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


96 


97 


98 
(* type mode *)


99 


100 
datatype mode = Forward  ForwardChain  Backward;


101 


102 
val mode_name =


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


104 


105 


106 
(* type node *)


107 


108 
type node =


109 
{context: context,


110 
facts: tthm list option,


111 
mode: mode,


112 
goal: goal option};


113 


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


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


116 


117 


118 
(* datatype state *)


119 


120 
datatype state =


121 
State of


122 
node * (*current*)


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


124 


125 
exception STATE of string * state;


126 


127 
fun err_malformed name state =


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


129 


130 


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


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


133 


134 
fun init_state thy =

5875

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

5820

136 


137 


138 


139 
(** basic proof state operations **)


140 


141 
(* context *)


142 


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


144 
val theory_of = ProofContext.theory_of o context_of;


145 
val sign_of = ProofContext.sign_of o context_of;


146 


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


148 


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


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


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


152 


153 


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


155 
val declare_term = map_context o ProofContext.declare_term;


156 
val add_binds = map_context o ProofContext.add_binds_i;


157 
val put_tthms = map_context o ProofContext.put_tthms;


158 
val put_tthmss = map_context o ProofContext.put_tthmss;


159 


160 


161 
(* bind statements *)


162 


163 
fun bind_props bs state =


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


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


166 


167 
fun bind_tthms (name, tthms) state =


168 
let


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


170 
val named_props =


171 
(case props of


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


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


174 
in state > bind_props named_props end;


175 


176 
fun let_tthms name_tthms state =


177 
state


178 
> put_tthms name_tthms


179 
> bind_tthms name_tthms;


180 


181 


182 
(* facts *)


183 


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


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


186 


187 
fun put_facts facts state =


188 
state


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


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


191 


192 
val reset_facts = put_facts None;


193 


194 
fun have_facts (name, facts) state =


195 
state


196 
> put_facts (Some facts)


197 
> let_tthms (name, facts);


198 


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


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


201 


202 


203 
(* goal *)


204 


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


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


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


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


209 


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


211 


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


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


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


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


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


217 
 map_goal _ state = state;


218 


219 
fun goal_facts get state =


220 
state


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


222 


223 
fun use_facts state =


224 
state


225 
> goal_facts the_facts


226 
> reset_facts;


227 


228 


229 
(* mode *)


230 


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


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


233 


234 
val enter_forward = put_mode Forward;


235 
val enter_forward_chain = put_mode ForwardChain;


236 
val enter_backward = put_mode Backward;


237 


238 
fun assert_mode pred state =


239 
let val mode = get_mode state in


240 
if pred mode then state


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


242 
end;


243 


244 
fun is_chain state = get_mode state = ForwardChain;


245 
val assert_forward = assert_mode (equal Forward);


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


247 
val assert_backward = assert_mode (equal Backward);


248 


249 


250 
(* blocks *)


251 


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


253 


254 
fun new_block state =


255 
state


256 
> open_block


257 
> put_goal None;


258 


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


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


261 


262 


263 


264 
(** print_state **)


265 


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


267 
let


268 
val prt_tthm = Attribute.pretty_tthm;


269 


270 
fun print_facts None = ()


271 
 print_facts (Some ths) =


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


273 


274 
fun levels_up 0 = ""


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


276 


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


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


279 
Locale.print_goals (! goals_limit) thm);


280 
in


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


282 
writeln "";


283 
ProofContext.print_context context;


284 
writeln "";


285 
print_facts facts;


286 
print_goal (find_goal 0 state);


287 
writeln "";


288 
writeln (mode_name mode ^ " mode")


289 
end;


290 


291 


292 


293 
(** proof steps **)


294 


295 
(* datatype method *)


296 


297 
datatype method = Method of


298 
tthm list > (*use facts*)


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


300 
> (thm * (*refined goal*)


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


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


303 
Seq.seq;


304 


305 
val method = Method;


306 


307 


308 
(* refine goal *)


309 


310 
fun check_sign sg state =


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


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


313 


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


315 
let


316 
val Method meth = meth_fun context;


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


318 


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


320 
state


321 
> check_sign (sign_of_thm thm')


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


323 
> add_binds new_binds


324 
> put_tthmss new_thms;


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


326 


327 


328 
(* prepare result *)


329 


330 
fun varify_frees names thm =


331 
let


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


333 
 get_free _ (opt, _) = opt;


334 


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


336 


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


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


339 
in


340 
thm


341 
> Drule.forall_intr_list frees


342 
> Drule.forall_elim_vars (maxidx + 1)


343 
end;


344 


345 
fun implies_elim_hyps thm =


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


347 


348 
fun prep_result state asms t raw_thm =


349 
let


350 
val ctxt = context_of state;


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


352 


353 
val ngoals = Thm.nprems_of raw_thm;


354 
val _ =


355 
if ngoals = 0 then ()


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


357 


358 
val thm =


359 
raw_thm RS Drule.rev_triv_goal


360 
> implies_elim_hyps


361 
> Drule.implies_intr_list asms


362 
> varify_frees (ProofContext.fixed_names ctxt);


363 


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


365 
val tsig = Sign.tsig_of sign;


366 
in


367 
(* FIXME


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


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


370 
else ();


371 
*)


372 
if not (null hyps) then


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


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


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


376 
else thm


377 
end;


378 


379 


380 
(* prepare final result *)


381 


382 
fun strip_flexflex thm =


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


384 


385 
fun final_result state pre_thm =


386 
let


387 
val thm =


388 
pre_thm


389 
> strip_flexflex


390 
> Thm.strip_shyps


391 
> Drule.standard;


392 


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


394 
val xshyps = Thm.extra_shyps thm;


395 
in


396 
if not (null xshyps) then


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


398 
else thm


399 
end;


400 


401 


402 
(* solve goal *)


403 


404 
fun solve_goal rule state =


405 
let


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


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


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


409 


410 


411 


412 
(*** structured proof commands ***)


413 


414 
(** context **)


415 


416 
(* bind *)


417 


418 
fun gen_bind f x state =


419 
state


420 
> assert_forward


421 
> map_context (f x)


422 
> reset_facts;


423 


424 
val bind = gen_bind ProofContext.add_binds;


425 
val bind_i = gen_bind ProofContext.add_binds_i;


426 


427 
val match_bind = gen_bind ProofContext.match_binds;


428 
val match_bind_i = gen_bind ProofContext.match_binds_i;


429 


430 

5918

431 
(* have_tthmss *)

5820

432 

5918

433 
fun have_tthmss name atts ths_atts state =

5820

434 
state


435 
> assert_forward

5918

436 
> map_context_result (ProofContext.have_tthmss (PureThy.default_name name) atts ths_atts)

5820

437 
> these_facts;


438 


439 


440 
(* fix *)


441 


442 
fun gen_fix f xs state =


443 
state


444 
> assert_forward


445 
> map_context (f xs)


446 
> reset_facts;


447 


448 
val fix = gen_fix ProofContext.fix;


449 
val fix_i = gen_fix ProofContext.fix_i;


450 


451 


452 
(* assume *)


453 


454 
fun gen_assume f name atts props state =


455 
state


456 
> assert_forward

5918

457 
> map_context_result (f (PureThy.default_name name) atts props)

5820

458 
> these_facts


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


460 


461 
val assume = gen_assume ProofContext.assume;


462 
val assume_i = gen_assume ProofContext.assume_i;


463 


464 


465 


466 
(** goals **)


467 


468 
(* forward chaining *)


469 


470 
fun chain state =


471 
state


472 
> assert_forward


473 
> enter_forward_chain;


474 


475 
fun from_facts facts state =


476 
state


477 
> put_facts (Some facts)


478 
> chain;


479 


480 


481 
(* setup goals *)


482 


483 
val read_prop = ProofContext.read_prop o context_of;


484 
val cert_prop = ProofContext.cert_prop o context_of;


485 


486 
fun setup_goal opt_block prep kind name atts raw_prop state =


487 
let


488 
val sign = sign_of state;


489 
val ctxt = context_of state;


490 


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


492 
val asms = map Thm.term_of casms;


493 


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


495 
val cprop = Thm.cterm_of sign prop;


496 
val thm = Drule.mk_triv_goal cprop;


497 
in


498 
state


499 
> assert_forward_or_chain


500 
> enter_forward


501 
> opt_block


502 


503 
> declare_term prop

5918

504 
> put_goal (Some ((kind atts, (PureThy.default_name name), casms, prop), ([], thm)))

5820

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


506 
> (if is_chain state then use_facts else reset_facts)


507 


508 
> new_block


509 
> enter_backward


510 
end;


511 


512 


513 
(*global goals*)


514 
fun global_goal prep kind name atts x thy =


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


516 


517 
val theorem = global_goal read_prop Theorem;


518 
val theorem_i = global_goal cert_prop Theorem;


519 
val lemma = global_goal read_prop Lemma;


520 
val lemma_i = global_goal cert_prop Lemma;


521 


522 


523 
(*local goals*)


524 
fun local_goal prep kind name atts x =


525 
setup_goal open_block prep kind name atts x;


526 


527 
val show = local_goal read_prop Goal;


528 
val show_i = local_goal cert_prop Goal;


529 
val have = local_goal read_prop Aux;


530 
val have_i = local_goal cert_prop Aux;


531 


532 


533 


534 
(** blocks **)


535 


536 
(* begin_block *)


537 


538 
fun begin_block state =


539 
state


540 
> assert_forward


541 
> new_block


542 
> reset_facts


543 
> open_block;


544 


545 


546 
(* next_block *)


547 


548 
fun next_block state =


549 
state


550 
> assert_forward


551 
> close_block


552 
> new_block;


553 


554 


555 


556 
(** conclusions **)


557 


558 
(* current goal *)


559 


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


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


562 


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


564 


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


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


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


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


569 
 assert_bottom _ state = state;


570 


571 


572 
(* finish proof *)


573 


574 
fun check_finished state states =


575 
(case Seq.pull states of


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


577 
 Some s_sq => Seq.cons s_sq);


578 


579 
fun finish_proof bot meth_fun state =


580 
state


581 
> assert_forward


582 
> close_block


583 
> assert_bottom bot


584 
> assert_current_goal


585 
> refine meth_fun


586 
> check_finished state;


587 


588 


589 
(* conclude local proof *)


590 


591 
fun finish_local state =


592 
let


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


594 
val result = prep_result state asms t raw_thm;


595 
val (atts, opt_solve) =


596 
(case kind of


597 
Goal atts => (atts, solve_goal result)


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


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


600 
in


601 
state


602 
> close_block

5918

603 
> have_tthmss name atts [([(result, [])], [])]

5820

604 
> opt_solve


605 
end;


606 


607 
fun end_block meth_fun state =


608 
if can assert_current_goal (close_block state) then


609 
state


610 
> finish_proof false meth_fun


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


612 
else


613 
state


614 
> assert_forward


615 
> close_block


616 
> close_block


617 
> fetch_facts state


618 
> Seq.single;


619 


620 


621 
(* conclude global proof *)


622 


623 
fun finish_global alt_name alt_atts state =


624 
let


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


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


627 


628 
val name = if_none alt_name def_name;


629 
val atts =


630 
(case kind of


631 
Theorem atts => if_none alt_atts atts

5918

632 
 Lemma atts => (if_none alt_atts atts) @ [Attribute.tag_lemma]

5820

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


634 


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


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


637 


638 
fun qed meth_fun alt_name alt_atts state =


639 
state


640 
> finish_proof true meth_fun


641 
> Seq.hd


642 
> finish_global alt_name alt_atts;


643 


644 


645 
end;
