# HG changeset patch # User wenzelm # Date 1389393843 -3600 # Node ID fe454ca3405f43678cc9f1720dc7cc6e12ac6020 # Parent 7e0573a490ee83f48cf2b474488726403741fa49# Parent 9a1710a644126e95c76d094c4213522b1f29e997 merged diff -r 7e0573a490ee -r fe454ca3405f src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Jan 10 23:44:03 2014 +0100 @@ -343,19 +343,19 @@ map (fold_rev (NominalDatatype.mk_perm []) (rev pis' @ pis)) params' @ [z])) ihyp; fun mk_pi th = - Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}] + Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}] addsimprocs [NominalDatatype.perm_simproc]) - (Simplifier.simplify (put_simpset eqvt_ss ctxt) + (Simplifier.simplify (put_simpset eqvt_ss ctxt') (fold_rev (mk_perm_bool o cterm_of thy) (rev pis' @ pis) th)); val (gprems1, gprems2) = split_list (map (fn (th, t) => if null (preds_of ps t) then (SOME th, mk_pi th) else - (map_thm ctxt (split_conj (K o I) names) + (map_thm ctxt' (split_conj (K o I) names) (etac conjunct1 1) monos NONE th, - mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis'')) - (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th)))) + mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis'')) + (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))) (gprems ~~ oprems)) |>> map_filter I; val vc_compat_ths' = map (fn th => let @@ -625,9 +625,9 @@ in error ("Could not prove equivariance for introduction rule\n" ^ Syntax.string_of_term ctxt''' t ^ "\n" ^ s) end; - val res = SUBPROOF (fn {prems, params, ...} => + val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} => let - val prems' = map (fn th => the_default th (map_thm ctxt' + val prems' = map (fn th => the_default th (map_thm ctxt'' (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; val prems'' = map (fn th => Simplifier.simplify eqvt_simpset (mk_perm_bool (cterm_of thy pi) th)) prems'; diff -r 7e0573a490ee -r fe454ca3405f src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Jan 10 23:44:03 2014 +0100 @@ -335,13 +335,13 @@ (map Bound (length pTs - 1 downto 0)); val _ $ (f $ (_ $ pi $ l) $ r) = prop_of th2 val th2' = - Goal.prove ctxt [] [] + Goal.prove ctxt' [] [] (Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop (f $ fold_rev (NominalDatatype.mk_perm (rev pTs)) (pis1 @ pi :: pis2) l $ r))) (fn _ => cut_facts_tac [th2] 1 THEN - full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_set_forget) 1) |> - Simplifier.simplify (put_simpset eqvt_ss ctxt) + full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps perm_set_forget) 1) |> + Simplifier.simplify (put_simpset eqvt_ss ctxt') in (freshs @ [term_of cx], ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt') @@ -401,16 +401,16 @@ (map (fold_rev (NominalDatatype.mk_perm []) (pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]); fun mk_pi th = - Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}] + Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}] addsimprocs [NominalDatatype.perm_simproc]) - (Simplifier.simplify (put_simpset eqvt_ss ctxt) + (Simplifier.simplify (put_simpset eqvt_ss ctxt') (fold_rev (mk_perm_bool o cterm_of thy) (pis' @ pis) th)); val gprems2 = map (fn (th, t) => if null (preds_of ps t) then mk_pi th else - mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis'')) - (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th))) + mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis'')) + (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th))) (gprems ~~ oprems); val perm_freshs_freshs' = map (fn (th, (_, T)) => th RS the (AList.lookup op = perm_freshs_freshs T)) diff -r 7e0573a490ee -r fe454ca3405f src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Fri Jan 10 23:44:03 2014 +0100 @@ -187,8 +187,7 @@ | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) | _ => raise General.Fail "Too many conditions" - val (_, simp_ctxt) = ctxt - |> Assumption.add_assumes (#hyps (Thm.crep_thm simp)) + val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt in Goal.prove simp_ctxt [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) diff -r 7e0573a490ee -r fe454ca3405f src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jan 10 23:44:03 2014 +0100 @@ -425,16 +425,17 @@ val (prems0, concl) = th |> prop_of |> Logic.strip_horn val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped val goal = Logic.list_implies (prems, concl) + val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt val tac = cut_tac th 1 - THEN rewrite_goals_tac ctxt @{thms not_not [THEN eq_reflection]} + THEN rewrite_goals_tac ctxt' @{thms not_not [THEN eq_reflection]} THEN ALLGOALS assume_tac in if length prems = length prems0 then raise METIS_RECONSTRUCT ("resynchronize", "Out of sync") else - Goal.prove ctxt [] [] goal (K tac) - |> resynchronize ctxt fol_th + Goal.prove ctxt' [] [] goal (K tac) + |> resynchronize ctxt' fol_th end end @@ -722,8 +723,9 @@ THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) fun rotation_of_subgoal i = find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs + val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt in - Goal.prove ctxt [] [] @{prop False} + Goal.prove ctxt' [] [] @{prop False} (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts) THEN rename_tac outer_param_names 1 @@ -736,9 +738,9 @@ THEN PRIMITIVE (unify_first_prem_with_concl thy i) THEN assume_tac i THEN flexflex_tac))) - handle ERROR _ => - error ("Cannot replay Metis proof in Isabelle:\n\ - \Error when discharging Skolem assumptions.") + handle ERROR msg => + cat_error msg + "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions." end end; diff -r 7e0573a490ee -r fe454ca3405f src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Fri Jan 10 17:24:52 2014 +0100 +++ b/src/HOL/ex/Meson_Test.thy Fri Jan 10 23:44:03 2014 +0100 @@ -37,7 +37,7 @@ val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*) val go25 :: _ = Meson.gocls clauses25; - val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt; + val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => rtac go25 1 THEN Meson.depth_prolog_tac horns25); @@ -63,7 +63,7 @@ val _ = @{assert} (length horns26 = 24); val go26 :: _ = Meson.gocls clauses26; - val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt; + val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => rtac go26 1 THEN Meson.depth_prolog_tac horns26); (*7 ms*) @@ -90,7 +90,7 @@ val _ = @{assert} (length horns43 = 16); val go43 :: _ = Meson.gocls clauses43; - val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt; + val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => rtac go43 1 THEN Meson.best_prolog_tac Meson.size_of_subgoals horns43); (*7ms*) diff -r 7e0573a490ee -r fe454ca3405f src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/Pure/Isar/proof.ML Fri Jan 10 23:44:03 2014 +0100 @@ -481,6 +481,8 @@ let val thy = Proof_Context.theory_of ctxt; + val _ = + Theory.subthy (theory_of_thm goal, thy) orelse error "Bad background theory of goal state"; val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal); @@ -490,7 +492,7 @@ handle THM _ => lost_structure ()) |> Drule.flexflex_unique |> Thm.check_shyps (Variable.sorts_of ctxt) - |> Assumption.check_hyps ctxt; + |> Thm.check_hyps ctxt; val goal_propss = filter_out null propss; val results = diff -r 7e0573a490ee -r fe454ca3405f src/Pure/assumption.ML --- a/src/Pure/assumption.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/Pure/assumption.ML Fri Jan 10 23:44:03 2014 +0100 @@ -10,9 +10,9 @@ val assume_export: export val presume_export: export val assume: Proof.context -> cterm -> thm + val assume_hyps: cterm -> Proof.context -> thm * Proof.context val all_assms_of: Proof.context -> cterm list val all_prems_of: Proof.context -> thm list - val check_hyps: Proof.context -> thm -> thm val local_assms_of: Proof.context -> Proof.context -> cterm list val local_prems_of: Proof.context -> Proof.context -> thm list val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context @@ -48,8 +48,13 @@ *) fun presume_export _ = assume_export false; + fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume; +fun assume_hyps ct ctxt = + let val (th, ctxt') = Thm.assume_hyps ct ctxt + in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end; + (** local context data **) @@ -76,13 +81,6 @@ val all_assms_of = maps #2 o all_assumptions_of; val all_prems_of = #prems o rep_data; -fun check_hyps ctxt th = - let - val extra_hyps = subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th); - val _ = null extra_hyps orelse - error ("Additional hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) extra_hyps)); - in th end; - (* local assumptions *) @@ -98,8 +96,8 @@ (* add assumptions *) fun add_assms export new_asms ctxt = - let val new_prems = map (assume ctxt) new_asms in - ctxt + let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in + ctxt' |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) |> pair new_prems end; diff -r 7e0573a490ee -r fe454ca3405f src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/Pure/goal.ML Fri Jan 10 23:44:03 2014 +0100 @@ -215,11 +215,13 @@ NONE => err "Tactic failed" | SOME st => let + val _ = + Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state"; val res = (finish ctxt' st |> Drule.flexflex_unique |> Thm.check_shyps sorts - (* |> Assumption.check_hyps ctxt' FIXME *)) + (* |> Thm.check_hyps ctxt' *) (* FIXME *)) handle THM (msg, _, _) => err msg | ERROR msg => err msg; in if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res diff -r 7e0573a490ee -r fe454ca3405f src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/Pure/more_thm.ML Fri Jan 10 23:44:03 2014 +0100 @@ -52,6 +52,9 @@ val full_rules: thm Item_Net.T val intro_rules: thm Item_Net.T val elim_rules: thm Item_Net.T + val declare_hyps: cterm -> Proof.context -> Proof.context + val assume_hyps: cterm -> Proof.context -> thm * Proof.context + val check_hyps: Proof.context -> thm -> thm val elim_implies: thm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm @@ -259,6 +262,30 @@ +(** declared hyps **) + +structure Hyps = Proof_Data +( + type T = Termtab.set; + fun init _ : T = Termtab.empty; +); + +fun declare_hyps ct ctxt = + if Theory.subthy (theory_of_cterm ct, Proof_Context.theory_of ctxt) then + Hyps.map (Termtab.update (term_of ct, ())) ctxt + else raise CTERM ("assume_hyps: bad background theory", [ct]); + +fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); + +fun check_hyps ctxt th = + let + val undeclared = filter_out (Termtab.defined (Hyps.get ctxt)) (Thm.hyps_of th); + val _ = null undeclared orelse + error ("Undeclared hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) undeclared)); + in th end; + + + (** basic derived rules **) (*Elimination of implication diff -r 7e0573a490ee -r fe454ca3405f src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Jan 10 17:24:52 2014 +0100 +++ b/src/Pure/raw_simplifier.ML Fri Jan 10 23:44:03 2014 +0100 @@ -604,26 +604,26 @@ else rrule_eq_True ctxt thm name lhs elhs rhs thm end; -fun extract_rews (ctxt, thms) = +fun extract_rews ctxt thms = let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms end; -fun extract_safe_rrules (ctxt, thm) = - maps (orient_rrule ctxt) (extract_rews (ctxt, [thm])); +fun extract_safe_rrules ctxt thm = + maps (orient_rrule ctxt) (extract_rews ctxt [thm]); (* add/del rules explicitly *) -fun comb_simps comb mk_rrule (ctxt, thms) = +fun comb_simps ctxt comb mk_rrule thms = let - val rews = extract_rews (ctxt, thms); + val rews = extract_rews ctxt thms; in fold (fold comb o mk_rrule) rews ctxt end; fun ctxt addsimps thms = - comb_simps insert_rrule (mk_rrule ctxt) (ctxt, thms); + comb_simps ctxt insert_rrule (mk_rrule ctxt) thms; fun ctxt delsimps thms = - comb_simps del_rrule (map mk_rrule2 o mk_rrule ctxt) (ctxt, thms); + comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) thms; fun add_simp thm ctxt = ctxt addsimps [thm]; fun del_simp thm ctxt = ctxt delsimps [thm]; @@ -1190,14 +1190,14 @@ if mutsimp then mut_impc0 [] ct [] [] ctxt else nonmut_impc ct ctxt - and rules_of_prem ctxt prem = + and rules_of_prem prem ctxt = if maxidx_of_term (term_of prem) <> ~1 then (trace_cterm ctxt true (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:") - prem; ([], NONE)) + prem; (([], NONE), ctxt)) else - let val asm = Thm.assume prem - in (extract_safe_rrules (ctxt, asm), SOME asm) end + let val (asm, ctxt') = Thm.assume_hyps prem ctxt + in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end and add_rrules (rrss, asms) ctxt = (fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms) @@ -1242,10 +1242,10 @@ and mut_impc0 prems concl rrss asms ctxt = let val prems' = strip_imp_prems concl; - val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems'); + val ((rrss', asms'), ctxt') = fold_map rules_of_prem prems' ctxt |>> split_list; in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') - (asms @ asms') [] [] [] [] ctxt ~1 ~1 + (asms @ asms') [] [] [] [] ctxt' ~1 ~1 end and mut_impc [] concl [] [] prems' rrss' asms' eqns ctxt changed k = @@ -1270,7 +1270,7 @@ val tprems = map term_of prems; val i = 1 + fold Integer.max (map (fn p => find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1; - val (rrs', asm') = rules_of_prem ctxt prem'; + val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt; in mut_impc prems concl rrss asms (prem' :: prems') (rrs' :: rrss') (asm' :: asms') @@ -1278,7 +1278,7 @@ (take i prems) (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies (drop i prems, concl))))) :: eqns) - ctxt (length prems') ~1 + ctxt' (length prems') ~1 end) (*legacy code -- only for backwards compatibility*) @@ -1289,7 +1289,9 @@ val prem1 = the_default prem (Option.map Thm.rhs_of thm1); val ctxt1 = if not useprem then ctxt - else add_rrules (apsnd single (apfst single (rules_of_prem ctxt prem1))) ctxt + else + let val ((rrs, asm), ctxt') = rules_of_prem prem1 ctxt + in add_rrules ([rrs], [asm]) ctxt' end; in (case botc skel0 ctxt1 conc of NONE =>