# HG changeset patch # User wenzelm # Date 1151947989 -7200 # Node ID df19a78761831e3519119f2843de7e52fe6463ff # Parent ac1b062c81ace0eff21754a5af836d93694961af obtain_export: Thm.generalize; guess: fixed handling of mixfixes of vars; tuned; diff -r ac1b062c81ac -r df19a7876183 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Mon Jul 03 19:33:07 2006 +0200 +++ b/src/Pure/Isar/obtain.ML Mon Jul 03 19:33:09 2006 +0200 @@ -69,24 +69,21 @@ *) fun obtain_export ctxt parms rule cprops thm = let - val {thy, prop, maxidx, ...} = Thm.rep_thm thm; - val cparms = map (Thm.cterm_of thy) parms; + val {thy, prop, ...} = Thm.rep_thm thm; + val concl = Logic.strip_assums_concl prop; + val bads = Term.fold_aterms (fn v as Free (x, _) => + if member (op =) parms x then insert (op aconv) v else I | _ => I) concl []; - val thm' = thm - |> Drule.implies_intr_protected cprops - |> Drule.forall_intr_list cparms - |> Drule.forall_elim_vars (maxidx + 1); + val thm' = thm |> Drule.implies_intr_protected cprops; + val thm'' = thm' |> Thm.generalize ([], parms) (Thm.maxidx_of thm' + 1); val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI); - - val concl = Logic.strip_assums_concl prop; - val bads = parms inter (Term.term_frees concl); in if not (null bads) then error ("Conclusion contains obtained parameters: " ^ space_implode " " (map (ProofContext.string_of_term ctxt) bads)) else if not (ObjectLogic.is_judgment thy concl) then - error "Conclusion in obtained context must be object-logic judgments" - else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule + error "Conclusion in obtained context must be object-logic judgment" + else (Tactic.rtac thm'' THEN' RANGE elim_tacs) 1 rule end; @@ -129,15 +126,13 @@ fun occs_var x = Library.get_first (fn t => Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props; - val raw_parms = map occs_var xs; - val parms = map_filter I raw_parms; - val parm_names = - map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs); + val parms = + map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (map occs_var xs ~~ xs); val that_name = if name = "" then thatN else name; val that_prop = - Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis)) - |> Library.curry Logic.list_rename_params (map #2 parm_names); + Term.list_all_free (map #1 parms, Logic.list_implies (asm_props, thesis)) + |> Library.curry Logic.list_rename_params (map #2 parms); val obtain_prop = Logic.list_rename_params ([AutoBind.thesisN], Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis))); @@ -146,7 +141,7 @@ Proof.local_qed (NONE, false) #> Seq.map (`Proof.the_fact #-> (fn rule => Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars) - #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms)); + #> Proof.assm_i (K (obtain_export ctxt (map (#1 o #1) parms) rule)) asms)); in state |> Proof.enter_forward @@ -173,15 +168,17 @@ local -fun unify_params ctxt vars raw_rule = +fun unify_params vars thesis_name raw_rule ctxt = let val thy = ProofContext.theory_of ctxt; + val certT = Thm.ctyp_of thy; + val cert = Thm.cterm_of thy; val string_of_typ = ProofContext.string_of_typ ctxt; val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt); fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th); - val maxidx = fold (Term.maxidx_typ o snd) vars ~1; + val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; val rule = Thm.incr_indexes (maxidx + 1) raw_rule; val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); @@ -194,26 +191,26 @@ err ("Failed to unify variable " ^ string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule; - val (tyenv, _) = fold unify (vars ~~ Library.take (m, params)) + val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params)) (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); val norm_type = Envir.norm_type tyenv; - val xs = map (apsnd norm_type) vars; + val xs = map (apsnd norm_type o fst) vars; val ys = map (apsnd norm_type) (Library.drop (m, params)); val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys; + val terms = map (Drule.mk_term o cert o Free) (xs @ 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, []); + |> map (TVar #> (fn T => (certT T, certT (norm_type T)))); + val (rule' :: terms', ctxt') = + Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt; - val tvars = Drule.tvars_of rule'; - val vars = subtract (op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule'); - val _ = - if null tvars andalso null vars then () - else err ("Illegal schematic variable(s) " ^ - commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule'; - in (xs @ ys', rule') end; + val vars' = + map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ + (map snd vars @ replicate (length ys) NoSyn); + val rule'' = Thm.generalize ([], [thesis_name]) (Thm.maxidx_of rule' + 1) rule'; + in ((vars', rule''), ctxt') end; fun inferred_type (x, _, mx) ctxt = let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt @@ -230,7 +227,7 @@ 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_name, _), thesis) = bind_judgment ctxt AutoBind.thesisN; val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic; fun check_result th = @@ -242,20 +239,23 @@ | [] => error "Goal solved -- nothing guessed." | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th)); - fun guess_context [_, raw_rule] = + fun guess_context raw_rule state' = let - val (parms, rule) = unify_params ctxt (map #1 vars) raw_rule; - val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt; - val ts = map (bind o Free) parms; + val ((parms, rule), ctxt') = + unify_params vars thesis_name raw_rule (Proof.context_of state'); + val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt'; + val ts = map (bind o Free o #1) parms; val ps = map dest_Free ts; val asms = Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), [])); val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; in - Proof.fix_i (map2 (fn (x, T) => fn (_, mx) => (x, SOME T, mx)) parms vars) - #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)] - #> Proof.add_binds_i AutoBind.no_facts + state' + |> Proof.map_context (K ctxt') + |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms) + |> Proof.assm_i (K (obtain_export ctxt' (map #1 ps) rule)) [(("", []), asms)] + |> Proof.add_binds_i AutoBind.no_facts end; val goal = Var (("guess", 0), propT); @@ -264,7 +264,7 @@ val before_qed = SOME (Method.primitive_text (Goal.conclude #> (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)))); fun after_qed [[_, res]] = - (check_result res; Proof.end_block #> Seq.map (`Proof.the_facts #-> guess_context)); + (check_result res; Proof.end_block #> Seq.map (guess_context res)); in state |> Proof.enter_forward