wenzelm@7674: (* Title: Pure/Isar/obtain.ML wenzelm@7674: ID: $Id$ wenzelm@7674: Author: Markus Wenzel, TU Muenchen wenzelm@7674: wenzelm@17858: The 'obtain' and 'guess' language elements -- generalized existence at wenzelm@17858: the level of proof texts: 'obtain' involves a proof that certain wenzelm@17858: fixes/assumes may be introduced into the present context; 'guess' is wenzelm@17858: similar, but derives these elements from the course of reasoning! wenzelm@7674: wenzelm@9468: wenzelm@18870: obtain x where "A x" == wenzelm@7674: wenzelm@18870: have "!!thesis. (!!x. A x ==> thesis) ==> thesis" wenzelm@12970: proof succeed wenzelm@9468: fix thesis wenzelm@18870: assume that [intro?]: "!!x. A x ==> thesis" wenzelm@18870: wenzelm@18870: show thesis wenzelm@18870: apply (insert that) wenzelm@18870: wenzelm@12970: qed wenzelm@18870: fix x assm <> "A x" wenzelm@17858: wenzelm@17858: wenzelm@17858: wenzelm@17858: guess x == wenzelm@17858: wenzelm@17858: { wenzelm@17858: fix thesis wenzelm@17858: have "PROP ?guess" wenzelm@18870: apply magic -- {* turns goal into "thesis ==> #thesis" *} wenzelm@17858: wenzelm@18870: apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into wenzelm@18870: "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} wenzelm@17858: wenzelm@17858: } wenzelm@18870: fix x assm <> "A x" wenzelm@8094: *) wenzelm@7674: wenzelm@7674: signature OBTAIN = wenzelm@7674: sig wenzelm@19844: val obtain: string -> (string * string option * mixfix) list -> wenzelm@19585: ((string * Attrib.src list) * (string * string list) list) list wenzelm@17357: -> bool -> Proof.state -> Proof.state wenzelm@19844: val obtain_i: string -> (string * typ option * mixfix) list -> wenzelm@19585: ((string * attribute list) * (term * term list) list) list wenzelm@17357: -> bool -> Proof.state -> Proof.state wenzelm@19844: val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state wenzelm@19844: val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state wenzelm@18897: val statement: (string * ((string * 'typ option) list * 'term list)) list -> wenzelm@18897: (('typ, 'term, 'fact) Element.ctxt list * wenzelm@19585: ((string * Attrib.src list) * ('term * 'term list) list) list) * wenzelm@19585: (((string * Attrib.src list) * (term * term list) list) list -> Proof.context -> wenzelm@19585: (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context) wenzelm@7674: end; wenzelm@7674: wenzelm@10379: structure Obtain: OBTAIN = wenzelm@7674: struct wenzelm@7674: wenzelm@8094: wenzelm@18670: (** obtain_export **) wenzelm@18670: wenzelm@18870: (* wenzelm@18897: [x, A x] wenzelm@18897: : wenzelm@18897: B wenzelm@18897: -------- wenzelm@18897: B wenzelm@18870: *) wenzelm@18678: fun obtain_export ctxt parms rule cprops thm = wenzelm@9468: let wenzelm@19978: val {thy, prop, ...} = Thm.rep_thm thm; wenzelm@19978: val concl = Logic.strip_assums_concl prop; wenzelm@19978: val bads = Term.fold_aterms (fn v as Free (x, _) => wenzelm@19978: if member (op =) parms x then insert (op aconv) v else I | _ => I) concl []; wenzelm@9468: wenzelm@19978: val thm' = thm |> Drule.implies_intr_protected cprops; wenzelm@19978: val thm'' = thm' |> Thm.generalize ([], parms) (Thm.maxidx_of thm' + 1); wenzelm@18040: val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI); wenzelm@9468: in wenzelm@9468: if not (null bads) then wenzelm@18678: error ("Conclusion contains obtained parameters: " ^ wenzelm@18678: space_implode " " (map (ProofContext.string_of_term ctxt) bads)) wenzelm@17858: else if not (ObjectLogic.is_judgment thy concl) then wenzelm@19978: error "Conclusion in obtained context must be object-logic judgment" wenzelm@19978: else (Tactic.rtac thm'' THEN' RANGE elim_tacs) 1 rule wenzelm@9468: end; wenzelm@9468: wenzelm@9468: wenzelm@9468: wenzelm@17858: (** obtain **) wenzelm@17858: wenzelm@17858: fun bind_judgment ctxt name = wenzelm@18670: let wenzelm@18670: val (bind, _) = ProofContext.bind_fixes [name] ctxt; wenzelm@18670: val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name); wenzelm@17858: in (v, t) end; wenzelm@17858: wenzelm@18897: val thatN = "that"; wenzelm@18897: wenzelm@17858: local wenzelm@8094: wenzelm@18897: fun gen_obtain prep_att prep_vars prep_propp wenzelm@18897: name raw_vars raw_asms int state = wenzelm@7674: let wenzelm@9468: val _ = Proof.assert_forward_or_chain state; wenzelm@17858: val ctxt = Proof.context_of state; wenzelm@18678: val thy = Proof.theory_of state; wenzelm@17357: val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; wenzelm@7674: wenzelm@8543: (*obtain vars*) wenzelm@19844: val (vars, vars_ctxt) = prep_vars raw_vars ctxt; wenzelm@18670: val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; wenzelm@18670: val xs = map #1 vars; wenzelm@7674: wenzelm@8543: (*obtain asms*) wenzelm@11890: val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); wenzelm@19482: val asm_props = maps (map fst) proppss; wenzelm@18678: val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; wenzelm@10464: wenzelm@19897: val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt; wenzelm@7674: wenzelm@12970: (*obtain statements*) wenzelm@16606: val thesisN = Term.variant xs AutoBind.thesisN; wenzelm@17858: val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN; wenzelm@9468: wenzelm@10582: fun occs_var x = Library.get_first (fn t => wenzelm@18151: Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props; wenzelm@19978: val parms = wenzelm@19978: map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (map occs_var xs ~~ xs); wenzelm@10582: wenzelm@18897: val that_name = if name = "" then thatN else name; wenzelm@10582: val that_prop = wenzelm@19978: Term.list_all_free (map #1 parms, Logic.list_implies (asm_props, thesis)) wenzelm@19978: |> Library.curry Logic.list_rename_params (map #2 parms); wenzelm@12970: val obtain_prop = wenzelm@12970: Logic.list_rename_params ([AutoBind.thesisN], wenzelm@17858: Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis))); wenzelm@7674: wenzelm@18124: fun after_qed _ = wenzelm@17357: Proof.local_qed (NONE, false) wenzelm@17858: #> Seq.map (`Proof.the_fact #-> (fn rule => wenzelm@19844: Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars) wenzelm@19978: #> Proof.assm_i (K (obtain_export ctxt (map (#1 o #1) parms) rule)) asms)); wenzelm@7674: in wenzelm@8094: state wenzelm@9468: |> Proof.enter_forward wenzelm@19585: |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int wenzelm@17858: |> Proof.proof (SOME Method.succeed_text) |> Seq.hd wenzelm@19844: |> Proof.fix_i [(thesisN, NONE, NoSyn)] wenzelm@19585: |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])] wenzelm@16842: |> `Proof.the_facts wenzelm@17357: ||> Proof.chain_facts chain_facts wenzelm@19585: ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false wenzelm@18907: |-> Proof.refine_insert wenzelm@7674: end; wenzelm@7674: wenzelm@17858: in wenzelm@17858: wenzelm@18728: val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp; wenzelm@17111: val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp; wenzelm@8094: wenzelm@8094: end; wenzelm@17858: wenzelm@17858: wenzelm@17858: wenzelm@17858: (** guess **) wenzelm@17858: wenzelm@17858: local wenzelm@17858: wenzelm@19978: fun unify_params vars thesis_name raw_rule ctxt = wenzelm@17858: let wenzelm@18678: val thy = ProofContext.theory_of ctxt; wenzelm@19978: val certT = Thm.ctyp_of thy; wenzelm@19978: val cert = Thm.cterm_of thy; wenzelm@17891: val string_of_typ = ProofContext.string_of_typ ctxt; wenzelm@17858: val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt); wenzelm@17891: wenzelm@18678: fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th); wenzelm@17858: wenzelm@19978: val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; wenzelm@19779: val rule = Thm.incr_indexes (maxidx + 1) raw_rule; wenzelm@19779: wenzelm@17858: val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); wenzelm@17858: val m = length vars; wenzelm@17858: val n = length params; wenzelm@19779: val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; wenzelm@17858: wenzelm@19779: fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) wenzelm@19779: handle Type.TUNIFY => wenzelm@19779: err ("Failed to unify variable " ^ wenzelm@19779: string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ wenzelm@19779: string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule; wenzelm@19978: val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params)) wenzelm@19779: (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); wenzelm@17858: val norm_type = Envir.norm_type tyenv; wenzelm@17858: wenzelm@19978: val xs = map (apsnd norm_type o fst) vars; wenzelm@19779: val ys = map (apsnd norm_type) (Library.drop (m, params)); wenzelm@19906: val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys; wenzelm@19978: val terms = map (Drule.mk_term o cert o Free) (xs @ ys'); wenzelm@19779: wenzelm@17858: val instT = wenzelm@17858: fold (Term.add_tvarsT o #2) params [] wenzelm@19978: |> map (TVar #> (fn T => (certT T, certT (norm_type T)))); wenzelm@19978: val (rule' :: terms', ctxt') = wenzelm@19978: Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt; wenzelm@17891: wenzelm@19978: val vars' = wenzelm@19978: map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ wenzelm@19978: (map snd vars @ replicate (length ys) NoSyn); wenzelm@19978: val rule'' = Thm.generalize ([], [thesis_name]) (Thm.maxidx_of rule' + 1) rule'; wenzelm@19978: in ((vars', rule''), ctxt') end; wenzelm@17858: wenzelm@18693: fun inferred_type (x, _, mx) ctxt = wenzelm@18769: let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt wenzelm@19779: in ((x, T, mx), ctxt') end; wenzelm@19779: wenzelm@19779: fun polymorphic (vars, ctxt) = wenzelm@19897: let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) wenzelm@19779: in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; wenzelm@18693: wenzelm@17858: fun gen_guess prep_vars raw_vars int state = wenzelm@17858: let wenzelm@17858: val _ = Proof.assert_forward_or_chain state; wenzelm@17858: val thy = Proof.theory_of state; wenzelm@17858: val ctxt = Proof.context_of state; wenzelm@17858: val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; wenzelm@17858: wenzelm@19978: val ((thesis_name, _), thesis) = bind_judgment ctxt AutoBind.thesisN; wenzelm@19844: val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic; wenzelm@17858: wenzelm@17974: fun check_result th = wenzelm@17974: (case Thm.prems_of th of wenzelm@17974: [prem] => wenzelm@17974: if Thm.concl_of th aconv thesis andalso wenzelm@17974: Logic.strip_assums_concl prem aconv thesis then () wenzelm@18678: else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th) wenzelm@18678: | [] => error "Goal solved -- nothing guessed." wenzelm@18678: | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th)); wenzelm@17891: wenzelm@19978: fun guess_context raw_rule state' = wenzelm@17858: let wenzelm@19978: val ((parms, rule), ctxt') = wenzelm@19978: unify_params vars thesis_name raw_rule (Proof.context_of state'); wenzelm@19978: val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt'; wenzelm@19978: val ts = map (bind o Free o #1) parms; wenzelm@17858: val ps = map dest_Free ts; wenzelm@17858: val asms = wenzelm@17858: Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) wenzelm@19585: |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), [])); wenzelm@19779: val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; wenzelm@17858: in wenzelm@19978: state' wenzelm@19978: |> Proof.map_context (K ctxt') wenzelm@19978: |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms) wenzelm@19978: |> Proof.assm_i (K (obtain_export ctxt' (map #1 ps) rule)) [(("", []), asms)] wenzelm@19978: |> Proof.add_binds_i AutoBind.no_facts wenzelm@17858: end; wenzelm@17858: wenzelm@19779: val goal = Var (("guess", 0), propT); wenzelm@19779: fun print_result ctxt' (k, [(s, [_, th])]) = wenzelm@19779: ProofDisplay.print_results int ctxt' (k, [(s, [th])]); wenzelm@19779: val before_qed = SOME (Method.primitive_text (Goal.conclude #> (fn th => wenzelm@19779: Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)))); wenzelm@19779: fun after_qed [[_, res]] = wenzelm@19978: (check_result res; Proof.end_block #> Seq.map (guess_context res)); wenzelm@17858: in wenzelm@17858: state wenzelm@17858: |> Proof.enter_forward wenzelm@17858: |> Proof.begin_block wenzelm@19844: |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)] wenzelm@17858: |> Proof.chain_facts chain_facts wenzelm@19779: |> Proof.local_goal print_result (K I) (apsnd (rpair I)) wenzelm@19779: "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])] wenzelm@18151: |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd wenzelm@17858: end; wenzelm@17858: wenzelm@17858: in wenzelm@17858: wenzelm@17858: val guess = gen_guess ProofContext.read_vars; wenzelm@17858: val guess_i = gen_guess ProofContext.cert_vars; wenzelm@17858: wenzelm@17858: end; wenzelm@17858: wenzelm@18897: wenzelm@18897: wenzelm@18897: (** statements with several cases **) wenzelm@18897: wenzelm@18897: fun statement cases = wenzelm@18897: let wenzelm@18907: val names = wenzelm@18907: cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); wenzelm@18897: val elems = cases |> map (fn (_, (vars, _)) => wenzelm@19482: Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))); wenzelm@19585: val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props)); wenzelm@18897: wenzelm@18897: fun mk_stmt stmt ctxt = wenzelm@18897: let wenzelm@18897: val thesis = wenzelm@18897: ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; wenzelm@18907: val atts = map Attrib.internal wenzelm@18907: [RuleCases.consumes (~ (length cases)), RuleCases.case_names names]; wenzelm@18907: wenzelm@18897: fun assume_case ((name, (vars, _)), (_, propp)) ctxt' = wenzelm@18897: let wenzelm@18897: val xs = map fst vars; wenzelm@18897: val props = map fst propp; wenzelm@18897: val (parms, ctxt'') = wenzelm@18897: ctxt' wenzelm@19897: |> fold Variable.declare_term props wenzelm@18897: |> fold_map ProofContext.inferred_param xs; wenzelm@18897: val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); wenzelm@18897: in wenzelm@18897: ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); wenzelm@18897: ctxt' |> ProofContext.add_assms_i ProofContext.assume_export wenzelm@19585: [((name, [ContextRules.intro_query NONE]), [(asm, [])])] wenzelm@18897: |>> (fn [(_, [th])] => th) wenzelm@18897: end; wenzelm@18897: val (ths, ctxt') = ctxt wenzelm@18897: |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) wenzelm@18897: |> fold_map assume_case (cases ~~ stmt) wenzelm@18897: |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths); wenzelm@19585: in (([(("", atts), [(thesis, [])])], ths), ctxt') end; wenzelm@18897: in ((elems, concl), mk_stmt) end; wenzelm@18897: wenzelm@17858: end;