# HG changeset patch # User wenzelm # Date 1129327687 -7200 # Node ID bc4db8cfd92f1d899c669af93916c7b8a208c947 # Parent 810a67ecbc6431cb627bb85b263226da150ea646 added 'guess', which derives the obtained context from the course of reasoning; diff -r 810a67ecbc64 -r bc4db8cfd92f src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Sat Oct 15 00:08:06 2005 +0200 +++ b/src/Pure/Isar/obtain.ML Sat Oct 15 00:08:07 2005 +0200 @@ -2,8 +2,10 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -The 'obtain' language element -- generalized existence at the level of -proof texts. +The 'obtain' and 'guess' language elements -- generalized existence at +the level of proof texts: 'obtain' involves a proof that certain +fixes/assumes may be introduced into the present context; 'guess' is +similar, but derives these elements from the course of reasoning! obtain x where "P x" == @@ -15,6 +17,21 @@ show thesis qed fix x assm (obtained) "P x" + + + + guess x == + + { + fix thesis + have "PROP ?guess" + apply magic -- {* turns goal into "thesis ==> thesis" (no goal marker!) *} + + apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> thesis" into + "GOAL ((!!x. P x ==> thesis) ==> thesis)" which is a finished goal state *} + + } + fix x assm (obtained) "P x" *) signature OBTAIN = @@ -25,15 +42,16 @@ val obtain_i: (string list * typ option) list -> ((string * Proof.context attribute list) * (term * (term list * term list)) list) list -> bool -> Proof.state -> Proof.state + val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state Seq.seq + val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state Seq.seq end; structure Obtain: OBTAIN = struct +(** export_obtained **) -(** export_obtain **) - -fun export_obtain state parms rule _ cprops thm = +fun export_obtained state parms rule cprops thm = let val {thy, prop, maxidx, ...} = Thm.rep_thm thm; val cparms = map (Thm.cterm_of thy) parms; @@ -50,44 +68,46 @@ if not (null bads) then raise Proof.STATE ("Conclusion contains obtained parameters: " ^ space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state) - else if not (ObjectLogic.is_judgment thy (Logic.strip_assums_concl prop)) then - raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state) + else if not (ObjectLogic.is_judgment thy concl) then + raise Proof.STATE ("Conclusion in obtained context must be object-logic judgments", state) else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule end; -(** obtain(_i) **) +(** obtain **) + +fun bind_judgment ctxt name = + let val (t as _ $ Free v) = + ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name + |> ProofContext.bind_skolem ctxt [name] + in (v, t) end; + +local val thatN = "that"; fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state = let val _ = Proof.assert_forward_or_chain state; + val ctxt = Proof.context_of state; val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; - val thy = Proof.theory_of state; (*obtain vars*) - val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars); + val (vars, vars_ctxt) = fold_map prep_vars raw_vars ctxt; + val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars; val xs = List.concat (map fst vars); - val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars; (*obtain asms*) val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); val asm_props = List.concat (map (map fst) proppss); - val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; + val asms = map fst (Attrib.map_specs (prep_att (Proof.theory_of state)) raw_asms) ~~ proppss; val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt; (*obtain statements*) val thesisN = Term.variant xs AutoBind.thesisN; - val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN]; - val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment thy thesisN); - val bound_thesis_raw as (bound_thesis_name, _) = - Term.dest_Free (bind_thesis (Free (thesisN, propT))); - val bound_thesis_var = - fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v) - | _ => I) bound_thesis bound_thesis_raw; + val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN; fun occs_var x = Library.get_first (fn t => ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props; @@ -97,31 +117,130 @@ List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs); val that_prop = - Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis)) + Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis)) |> Library.curry Logic.list_rename_params (map #2 parm_names); val obtain_prop = Logic.list_rename_params ([AutoBind.thesisN], - Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis))); + Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis))); fun after_qed _ _ = Proof.local_qed (NONE, false) - #> Seq.map (`Proof.the_fact #-> (fn this => + #> Seq.map (`Proof.the_fact #-> (fn rule => Proof.fix_i vars - #> Proof.assm_i (export_obtain state parms this) asms)); + #> Proof.assm_i (K (export_obtained state parms rule)) asms)); in state |> Proof.enter_forward - |> Proof.have_i (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int - |> Proof.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd + |> Proof.have_i NONE (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int + |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |> Proof.fix_i [([thesisN], NONE)] |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])] |> `Proof.the_facts ||> Proof.chain_facts chain_facts - ||> Proof.show_i after_qed [(("", []), [(bound_thesis, ([], []))])] false + ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd end; +in + val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp; val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp; end; + + + +(** guess **) + +local + +fun match_params state vars rule = + let + val ctxt = Proof.context_of state; + val thy = Proof.theory_of state; + val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt); + val string_of_thm = ProofContext.string_of_thm ctxt; + + val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); + val m = length vars; + val n = length params; + val _ = conditional (m > n) (fn () => + raise Proof.STATE ("More variables than parameters in obtained rule:\n" ^ + string_of_thm rule, state)); + + fun match ((x, SOME T), (y, U)) tyenv = + ((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH => + raise Proof.STATE ("Failed to match variable " ^ + string_of_term (Free (x, T)) ^ " against parameter " ^ + string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in:\n" ^ + string_of_thm rule, state)) + | match ((x, NONE), (_, U)) tyenv = ((x, U), tyenv); + val (xs, tyenv) = fold_map match (vars ~~ Library.take (m, params)) Vartab.empty; + val ys = Library.drop (m, params); + val norm_type = Envir.norm_type tyenv; + + val xs' = xs |> map (apsnd norm_type); + val ys' = + map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~ + map (norm_type o snd) ys; + val instT = + fold (Term.add_tvarsT o #2) params [] + |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T)))); + val rule' = rule |> Thm.instantiate (instT, []); + in (xs' @ ys', rule') end; + +fun gen_guess prep_vars raw_vars int state = + let + val _ = Proof.assert_forward_or_chain state; + val thy = Proof.theory_of state; + val ctxt = Proof.context_of state; + val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; + + val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN; + val thesis_goal = Drule.instantiate' [] [SOME (Thm.cterm_of thy thesis)] Drule.asm_rl; + val varss = #1 (fold_map prep_vars raw_vars ctxt); + val vars = List.concat (map (fn (xs, T) => map (rpair T) xs) varss); + + fun unary_rule rule = + (case Thm.nprems_of rule of 1 => rule + | 0 => raise Proof.STATE ("Goal solved -- nothing guessed.", state) + | _ => raise Proof.STATE ("Guess split into several cases:\n" ^ + ProofContext.string_of_thm ctxt rule, state)); + fun guess_context raw_rule = + let + val (parms, rule) = match_params state vars raw_rule; + val ts = map (ProofContext.bind_skolem ctxt (map #1 parms) o Free) parms; + val ps = map dest_Free ts; + val asms = + Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) + |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], []))); + in + Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms) + #> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)] + #> Proof.map_context (ProofContext.add_binds_i AutoBind.no_facts) + end; + + val before_qed = SOME (Method.primitive_text (fn th => + th COMP Drule.incr_indexes_wrt [] [] [] [th] Drule.triv_goal)); + fun after_qed _ _ = + Proof.end_block + #> Seq.map (`(unary_rule o Proof.the_fact) #-> guess_context); + in + state + |> Proof.enter_forward + |> Proof.begin_block + |> Proof.fix_i [([AutoBind.thesisN], NONE)] + |> Proof.chain_facts chain_facts + |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I)) + "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])] + |> Proof.refine (Method.primitive_text (K thesis_goal)) + end; + +in + +val guess = gen_guess ProofContext.read_vars; +val guess_i = gen_guess ProofContext.cert_vars; + +end; + +end;