# HG changeset patch # User paulson # Date 1385224897 0 # Node ID e51a0c4965f7a3d74571e73ce5c9491e5930e22c # Parent cfe53047dc16e465ac0d819cb649283866f08e2d# Parent 08b642269a0d66e0e45baa14e603b1c7feeb4db4 merged diff -r 08b642269a0d -r e51a0c4965f7 src/HOL/Tools/Function/mutual.ML --- 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 diff -r 08b642269a0d -r e51a0c4965f7 src/HOL/ex/Meson_Test.thy --- 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 @@ "(\x. P x) & (\x. L x --> ~ (M x & R x)) & (\x. P x --> (M x & L x)) & ((\x. P x --> Q x) | (\x. P x & R x)) --> (\x. Q x & P x)" apply (rule ccontr) ML_prf {* + val ctxt = @{context}; val prem25 = Thm.assume @{cprop "\ ?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 @@ "((\x. p x) = (\x. q x)) & (\x. \y. p x & q y --> (r x = s y)) --> ((\x. p x --> r x) = (\x. q x --> s x))" apply (rule ccontr) ML_prf {* + val ctxt = @{context}; val prem26 = Thm.assume @{cprop "\ ?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 @@ "(\x. \y. q x y = (\z. p z x = (p z y::bool))) --> (\x. (\y. q x y = (q y x::bool)))" apply (rule ccontr) ML_prf {* + val ctxt = @{context}; val prem43 = Thm.assume @{cprop "\ ?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*) *} diff -r 08b642269a0d -r e51a0c4965f7 src/Provers/Arith/cancel_numerals.ML --- 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 diff -r 08b642269a0d -r e51a0c4965f7 src/Pure/Isar/expression.ML --- 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; diff -r 08b642269a0d -r e51a0c4965f7 src/Pure/Isar/proof.ML --- 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 diff -r 08b642269a0d -r e51a0c4965f7 src/Pure/assumption.ML --- 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 *) diff -r 08b642269a0d -r e51a0c4965f7 src/Pure/goal.ML --- 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 () diff -r 08b642269a0d -r e51a0c4965f7 src/Tools/Code/lib/Tools/codegen --- 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,"