# HG changeset patch
# User wenzelm
# Date 1278953978 -7200
# Node ID 22107b894e5a556ae9f026827d089e3921fc294d
# Parent  df0350f1e7f25b07d67921e481e3bb440a1c3eae
some modernization of really ancient Meson experiments;

diff -r df0350f1e7f2 -r 22107b894e5a src/HOL/ex/Meson_Test.thy
--- 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