--- 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';
--- 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))
--- 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))
--- 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;
--- 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*)
--- 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 =
--- 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;
--- 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
--- 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
--- 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 =>