--- a/src/HOL/Tools/Function/mutual.ML Sat Nov 23 16:39:48 2013 +0000
+++ b/src/HOL/Tools/Function/mutual.ML Sat Nov 23 16:41:37 2013 +0000
@@ -187,8 +187,10 @@
| [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))
in
- Goal.prove ctxt [] []
+ Goal.prove simp_ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
(fn _ =>
Local_Defs.unfold_tac ctxt all_orig_fdefs
--- a/src/HOL/ex/Meson_Test.thy Sat Nov 23 16:39:48 2013 +0000
+++ b/src/HOL/ex/Meson_Test.thy Sat Nov 23 16:41:37 2013 +0000
@@ -24,18 +24,21 @@
"(\<exists>x. P x) & (\<forall>x. L x --> ~ (M x & R x)) & (\<forall>x. P x --> (M x & L x)) & ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x)) --> (\<exists>x. Q x & P x)"
apply (rule ccontr)
ML_prf {*
+ val ctxt = @{context};
val prem25 = Thm.assume @{cprop "\<not> ?thesis"};
- val nnf25 = Meson.make_nnf @{context} prem25;
- val xsko25 = Meson.skolemize @{context} nnf25;
+ val nnf25 = Meson.make_nnf ctxt prem25;
+ val xsko25 = Meson.skolemize ctxt nnf25;
*}
apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *})
ML_val {*
- val [_, sko25] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
- val clauses25 = Meson.make_clauses @{context} [sko25]; (*7 clauses*)
+ val ctxt = @{context};
+ val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
+ val clauses25 = Meson.make_clauses ctxt [sko25]; (*7 clauses*)
val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*)
val go25 :: _ = Meson.gocls clauses25;
- Goal.prove @{context} [] [] @{prop False} (fn _ =>
+ val (_, ctxt') = Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
+ Goal.prove ctxt' [] [] @{prop False} (fn _ =>
rtac go25 1 THEN
Meson.depth_prolog_tac horns25);
*}
@@ -45,18 +48,23 @@
"((\<exists>x. p x) = (\<exists>x. q x)) & (\<forall>x. \<forall>y. p x & q y --> (r x = s y)) --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))"
apply (rule ccontr)
ML_prf {*
+ val ctxt = @{context};
val prem26 = Thm.assume @{cprop "\<not> ?thesis"}
- val nnf26 = Meson.make_nnf @{context} prem26;
- val xsko26 = Meson.skolemize @{context} nnf26;
+ val nnf26 = Meson.make_nnf ctxt prem26;
+ val xsko26 = Meson.skolemize ctxt nnf26;
*}
apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *})
ML_val {*
- val [_, sko26] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
- val clauses26 = Meson.make_clauses @{context} [sko26]; (*9 clauses*)
- val horns26 = Meson.make_horns clauses26; (*24 Horn clauses*)
+ val ctxt = @{context};
+ val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
+ val clauses26 = Meson.make_clauses ctxt [sko26];
+ val _ = @{assert} (length clauses26 = 9);
+ val horns26 = Meson.make_horns clauses26;
+ val _ = @{assert} (length horns26 = 24);
val go26 :: _ = Meson.gocls clauses26;
- Goal.prove @{context} [] [] @{prop False} (fn _ =>
+ val (_, ctxt') = Assumption.add_assumes (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*)
(*Proof is of length 107!!*)
@@ -67,18 +75,23 @@
"(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool))) --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
apply (rule ccontr)
ML_prf {*
+ val ctxt = @{context};
val prem43 = Thm.assume @{cprop "\<not> ?thesis"};
- val nnf43 = Meson.make_nnf @{context} prem43;
- val xsko43 = Meson.skolemize @{context} nnf43;
+ val nnf43 = Meson.make_nnf ctxt prem43;
+ val xsko43 = Meson.skolemize ctxt nnf43;
*}
apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *})
ML_val {*
- val [_, sko43] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
- val clauses43 = Meson.make_clauses @{context} [sko43]; (*6*)
- val horns43 = Meson.make_horns clauses43; (*16*)
+ val ctxt = @{context};
+ val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
+ val clauses43 = Meson.make_clauses ctxt [sko43];
+ val _ = @{assert} (length clauses43 = 6);
+ val horns43 = Meson.make_horns clauses43;
+ val _ = @{assert} (length horns43 = 16);
val go43 :: _ = Meson.gocls clauses43;
- Goal.prove @{context} [] [] @{prop False} (fn _ =>
+ val (_, ctxt') = Assumption.add_assumes (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/Provers/Arith/cancel_numerals.ML Sat Nov 23 16:39:48 2013 +0000
+++ b/src/Provers/Arith/cancel_numerals.ML Sat Nov 23 16:41:37 2013 +0000
@@ -70,7 +70,7 @@
val prems = Simplifier.prems_of ctxt
val ([t'], ctxt') = Variable.import_terms true [t] ctxt
val export = singleton (Variable.export ctxt' ctxt)
- (* FIXME ctxt cs. ctxt' (!?) *)
+ (* FIXME ctxt vs. ctxt' (!?) *)
val (t1,t2) = Data.dest_bal t'
val terms1 = Data.dest_sum t1
--- a/src/Pure/Isar/expression.ML Sat Nov 23 16:39:48 2013 +0000
+++ b/src/Pure/Isar/expression.ML Sat Nov 23 16:41:37 2013 +0000
@@ -676,8 +676,11 @@
val conjuncts =
(Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
|> Conjunction.elim_balanced (length ts);
+
+ val (_, axioms_ctxt) = defs_ctxt
+ |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
- Element.prove_witness defs_ctxt t
+ Element.prove_witness axioms_ctxt t
(rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
in ((statement, intro, axioms), defs_thy) end;
--- a/src/Pure/Isar/proof.ML Sat Nov 23 16:39:48 2013 +0000
+++ b/src/Pure/Isar/proof.ML Sat Nov 23 16:41:37 2013 +0000
@@ -480,28 +480,25 @@
fun conclude_goal ctxt goal propss =
let
val thy = Proof_Context.theory_of ctxt;
- val string_of_term = Syntax.string_of_term ctxt;
- val string_of_thm = Display.string_of_thm ctxt;
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
- val extra_hyps = Assumption.extra_hyps ctxt goal;
- val _ = null extra_hyps orelse
- error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
+ fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
- fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
+ val th =
+ (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
+ handle THM _ => lost_structure ())
+ |> Drule.flexflex_unique
+ |> Thm.check_shyps (Variable.sorts_of ctxt)
+ |> Assumption.check_hyps ctxt;
- val th = Goal.conclude
- (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
- handle THM _ => lost_structure ();
val goal_propss = filter_out null propss;
val results =
Conjunction.elim_balanced (length goal_propss) th
|> map2 Conjunction.elim_balanced (map length goal_propss)
handle THM _ => lost_structure ();
val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
- error ("Proved a different theorem:\n" ^ string_of_thm th);
- val _ = Thm.check_shyps (Variable.sorts_of ctxt) th;
+ error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
| recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
--- a/src/Pure/assumption.ML Sat Nov 23 16:39:48 2013 +0000
+++ b/src/Pure/assumption.ML Sat Nov 23 16:41:37 2013 +0000
@@ -12,7 +12,7 @@
val assume: cterm -> thm
val all_assms_of: Proof.context -> cterm list
val all_prems_of: Proof.context -> thm list
- val extra_hyps: Proof.context -> thm -> term 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
@@ -76,8 +76,12 @@
val all_assms_of = maps #2 o all_assumptions_of;
val all_prems_of = #prems o rep_data;
-fun extra_hyps ctxt th =
- subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
+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 *)
--- a/src/Pure/goal.ML Sat Nov 23 16:39:48 2013 +0000
+++ b/src/Pure/goal.ML Sat Nov 23 16:41:37 2013 +0000
@@ -182,7 +182,6 @@
fun prove_common immediate pri ctxt xs asms props tac =
let
val thy = Proof_Context.theory_of ctxt;
- val string_of_term = Syntax.string_of_term ctxt;
val schematic = exists is_schematic props;
val future = future_enabled 1;
@@ -191,7 +190,7 @@
val pos = Position.thread_data ();
fun err msg = cat_error msg
("The error(s) above occurred for the goal statement:\n" ^
- string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
+ Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
(case Position.here pos of "" => "" | s => "\n" ^ s));
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
@@ -215,10 +214,16 @@
(case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
NONE => err "Tactic failed"
| SOME st =>
- let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
- if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
- then Thm.check_shyps sorts res
- else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
+ let
+ val res =
+ (finish ctxt' st
+ |> Drule.flexflex_unique
+ |> Thm.check_shyps sorts
+ (* |> Assumption.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
+ else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
end);
val res =
if immediate orelse schematic orelse not future orelse skip then result ()
--- a/src/Tools/Code/lib/Tools/codegen Sat Nov 23 16:39:48 2013 +0000
+++ b/src/Tools/Code/lib/Tools/codegen Sat Nov 23 16:41:37 2013 +0000
@@ -13,7 +13,7 @@
echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
echo
echo " Options are:"
- echo " -q run in quick'n'dirty mode"
+ echo " -q run in quick_and_dirty mode"
echo
echo " Issues code generation using image IMAGE,"
echo " theory THYNAME,"