--- a/src/HOL/ex/Meson_Test.thy Mon Jul 12 16:40:48 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy Mon Jul 12 18:59:38 2010 +0200
@@ -5,12 +5,6 @@
imports Main
begin
-ML {*
- val Goal = OldGoals.Goal;
- val by = OldGoals.by;
- val gethyps = OldGoals.gethyps;
-*}
-
text {*
WARNING: there are many potential conflicts between variables used
below and constants declared in HOL!
@@ -26,66 +20,69 @@
subsection {* Interactive examples *}
-ML {*
-writeln"Problem 25";
-Goal "(\<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)";
-by (rtac ccontr 1);
-val [prem25] = gethyps 1;
-val nnf25 = Meson.make_nnf @{context} prem25;
-val xsko25 = Meson.skolemize @{context} nnf25;
-by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
-val [_,sko25] = gethyps 1;
-val clauses25 = Meson.make_clauses [sko25]; (*7 clauses*)
-val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*)
-val go25::_ = Meson.gocls clauses25;
-*}
+lemma problem_25:
+ "(\<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 prem25 = Thm.assume @{cprop "\<not> ?thesis"};
+ val nnf25 = Meson.make_nnf @{context} prem25;
+ val xsko25 = Meson.skolemize @{context} nnf25;
+ *}
+ apply (tactic {* cut_facts_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 [sko25]; (*7 clauses*)
+ val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*)
+ val go25 :: _ = Meson.gocls clauses25;
-ML {*
-Goal "False";
-by (rtac go25 1);
-by (Meson.depth_prolog_tac horns25);
-*}
+ Goal.prove @{context} [] [] @{prop False} (fn _ =>
+ rtac go25 1 THEN
+ Meson.depth_prolog_tac horns25);
+ *}
+ oops
-ML {*
-writeln"Problem 26";
-Goal "((\<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))";
-by (rtac ccontr 1);
-val [prem26] = gethyps 1;
-val nnf26 = Meson.make_nnf @{context} prem26;
-val xsko26 = Meson.skolemize @{context} nnf26;
-by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
-val [_,sko26] = gethyps 1;
-val clauses26 = Meson.make_clauses [sko26]; (*9 clauses*)
-val horns26 = Meson.make_horns clauses26; (*24 Horn clauses*)
-val go26::_ = Meson.gocls clauses26;
-*}
+lemma problem_26:
+ "((\<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 prem26 = Thm.assume @{cprop "\<not> ?thesis"}
+ val nnf26 = Meson.make_nnf @{context} prem26;
+ val xsko26 = Meson.skolemize @{context} nnf26;
+ *}
+ apply (tactic {* cut_facts_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 [sko26]; (*9 clauses*)
+ val horns26 = Meson.make_horns clauses26; (*24 Horn clauses*)
+ val go26 :: _ = Meson.gocls clauses26;
-ML {*
-Goal "False";
-by (rtac go26 1);
-by (Meson.depth_prolog_tac horns26); (*1.4 secs*)
-(*Proof is of length 107!!*)
-*}
+ Goal.prove @{context} [] [] @{prop False} (fn _ =>
+ rtac go26 1 THEN
+ Meson.depth_prolog_tac horns26); (*7 ms*)
+ (*Proof is of length 107!!*)
+ *}
+ oops
-ML {*
-writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; (*16 Horn clauses*)
-Goal "(\<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)))";
-by (rtac ccontr 1);
-val [prem43] = gethyps 1;
-val nnf43 = Meson.make_nnf @{context} prem43;
-val xsko43 = Meson.skolemize @{context} nnf43;
-by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
-val [_,sko43] = gethyps 1;
-val clauses43 = Meson.make_clauses [sko43]; (*6*)
-val horns43 = Meson.make_horns clauses43; (*16*)
-val go43::_ = Meson.gocls clauses43;
-*}
+lemma problem_43: -- "NOW PROVED AUTOMATICALLY!!" (*16 Horn clauses*)
+ "(\<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 prem43 = Thm.assume @{cprop "\<not> ?thesis"};
+ val nnf43 = Meson.make_nnf @{context} prem43;
+ val xsko43 = Meson.skolemize @{context} nnf43;
+ *}
+ apply (tactic {* cut_facts_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 [sko43]; (*6*)
+ val horns43 = Meson.make_horns clauses43; (*16*)
+ val go43 :: _ = Meson.gocls clauses43;
-ML {*
-Goal "False";
-by (rtac go43 1);
-by (Meson.best_prolog_tac Meson.size_of_subgoals horns43); (*1.6 secs*)
-*}
+ Goal.prove @{context} [] [] @{prop False} (fn _ =>
+ rtac go43 1 THEN
+ Meson.best_prolog_tac Meson.size_of_subgoals horns43); (*7ms*)
+ *}
+ oops
(*
#1 (q x xa ==> ~ q x xa) ==> q xa x