Moved extraction part of Higman's lemma to separate theory to allow reuse in
theories compiled without support for proof terms.

--- a/src/HOL/IsaMakefile	Thu Sep 22 17:15:46 2011 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 22 18:23:38 2011 +0200
@@ -915,7 +915,8 @@
 $(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs		\
   Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy	\
   Proofs/Extraction/Greatest_Common_Divisor.thy			\
-  Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy	\
+  Proofs/Extraction/Higman.thy Proofs/Extraction/Higman_Extraction.thy	\
+  Proofs/Extraction/Pigeonhole.thy				\
   Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML	\
   Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy	\
   Proofs/Extraction/document/root.tex				\

--- a/src/HOL/Proofs/Extraction/Higman.thy	Thu Sep 22 17:15:46 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Thu Sep 22 18:23:38 2011 +0200
@@ -6,7 +6,7 @@
 header {* Higman's lemma *}
 
 theory Higman
-imports Main "~~/src/HOL/Library/State_Monad" Random
+imports Main
 begin
 
 text {*
@@ -310,156 +310,6 @@
   using higman
   by (rule good_prefix_lemma) simp+
 
-subsection {* Extracting the program *}
-
-declare R.induct [ind_realizer]
-declare T.induct [ind_realizer]
-declare L.induct [ind_realizer]
-declare good.induct [ind_realizer]
-declare bar.induct [ind_realizer]
-
-extract higman_idx
-
-text {*
-  Program extracted from the proof of @{text higman_idx}:
-  @{thm [display] higman_idx_def [no_vars]}
-  Corresponding correctness theorem:
-  @{thm [display] higman_idx_correctness [no_vars]}
-  Program extracted from the proof of @{text higman}:
-  @{thm [display] higman_def [no_vars]}
-  Program extracted from the proof of @{text prop1}:
-  @{thm [display] prop1_def [no_vars]}
-  Program extracted from the proof of @{text prop2}:
-  @{thm [display] prop2_def [no_vars]}
-  Program extracted from the proof of @{text prop3}:
-  @{thm [display] prop3_def [no_vars]}
-*}
-
-
-subsection {* Some examples *}
-
-instantiation LT and TT :: default
-begin
-
-definition "default = L0 [] []"
-
-definition "default = T0 A [] [] [] R0"
-
-instance ..
-
+(*<*)
 end
-
-function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
-  "mk_word_aux k = exec {
-     i \<leftarrow> Random.range 10;
-     (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
-     else exec {
-       let l = (if i mod 2 = 0 then A else B);
-       ls \<leftarrow> mk_word_aux (Suc k);
-       Pair (l # ls)
-     })}"
-by pat_completeness auto
-termination by (relation "measure ((op -) 1001)") auto
-
-definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
-  "mk_word = mk_word_aux 0"
-
-primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
-  "mk_word_s 0 = mk_word"
-  | "mk_word_s (Suc n) = exec {
-       _ \<leftarrow> mk_word;
-       mk_word_s n
-     }"
-
-definition g1 :: "nat \<Rightarrow> letter list" where
-  "g1 s = fst (mk_word_s s (20000, 1))"
-
-definition g2 :: "nat \<Rightarrow> letter list" where
-  "g2 s = fst (mk_word_s s (50000, 1))"
-
-fun f1 :: "nat \<Rightarrow> letter list" where
-  "f1 0 = [A, A]"
-  | "f1 (Suc 0) = [B]"
-  | "f1 (Suc (Suc 0)) = [A, B]"
-  | "f1 _ = []"
-
-fun f2 :: "nat \<Rightarrow> letter list" where
-  "f2 0 = [A, A]"
-  | "f2 (Suc 0) = [B]"
-  | "f2 (Suc (Suc 0)) = [B, A]"
-  | "f2 _ = []"
-
-ML {*
-local
-  val higman_idx = @{code higman_idx};
-  val g1 = @{code g1};
-  val g2 = @{code g2};
-  val f1 = @{code f1};
-  val f2 = @{code f2};
-in
-  val (i1, j1) = higman_idx g1;
-  val (v1, w1) = (g1 i1, g1 j1);
-  val (i2, j2) = higman_idx g2;
-  val (v2, w2) = (g2 i2, g2 j2);
-  val (i3, j3) = higman_idx f1;
-  val (v3, w3) = (f1 i3, f1 j3);
-  val (i4, j4) = higman_idx f2;
-  val (v4, w4) = (f2 i4, f2 j4);
-end;
-*}
-
-text {* The same story with the legacy SML code generator,
-this can be removed once the code generator is removed. *}
-
-code_module Higman
-contains
-  higman = higman_idx
-
-ML {*
-local open Higman in
-
-val a = 16807.0;
-val m = 2147483647.0;
-
-fun nextRand seed =
-  let val t = a*seed
-  in  t - m * real (Real.floor(t/m)) end;
-
-fun mk_word seed l =
-  let
-    val r = nextRand seed;
-    val i = Real.round (r / m * 10.0);
-  in if i > 7 andalso l > 2 then (r, []) else
-    apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
-  end;
-
-fun f s zero = mk_word s 0
-  | f s (Suc n) = f (fst (mk_word s 0)) n;
-
-val g1 = snd o (f 20000.0);
-
-val g2 = snd o (f 50000.0);
-
-fun f1 zero = [A,A]
-  | f1 (Suc zero) = [B]
-  | f1 (Suc (Suc zero)) = [A,B]
-  | f1 _ = [];
-
-fun f2 zero = [A,A]
-  | f2 (Suc zero) = [B]
-  | f2 (Suc (Suc zero)) = [B,A]
-  | f2 _ = [];
-
-val (i1, j1) = higman g1;
-val (v1, w1) = (g1 i1, g1 j1);
-val (i2, j2) = higman g2;
-val (v2, w2) = (g2 i2, g2 j2);
-val (i3, j3) = higman f1;
-val (v3, w3) = (f1 i3, f1 j3);
-val (i4, j4) = higman f2;
-val (v4, w4) = (f2 i4, f2 j4);
-
-end;
-*}
-
-end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Thu Sep 22 18:23:38 2011 +0200
@@ -0,0 +1,164 @@
+(*  Title:      HOL/Proofs/Extraction/Higman_Extraction.thy
+    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Monika Seisenberger, LMU Muenchen
+*)
+
+(*<*)
+theory Higman_Extraction
+imports Higman "~~/src/HOL/Library/State_Monad" Random
+begin
+(*>*)
+
+subsection {* Extracting the program *}
+
+declare R.induct [ind_realizer]
+declare T.induct [ind_realizer]
+declare L.induct [ind_realizer]
+declare good.induct [ind_realizer]
+declare bar.induct [ind_realizer]
+
+extract higman_idx
+
+text {*
+  Program extracted from the proof of @{text higman_idx}:
+  @{thm [display] higman_idx_def [no_vars]}
+  Corresponding correctness theorem:
+  @{thm [display] higman_idx_correctness [no_vars]}
+  Program extracted from the proof of @{text higman}:
+  @{thm [display] higman_def [no_vars]}
+  Program extracted from the proof of @{text prop1}:
+  @{thm [display] prop1_def [no_vars]}
+  Program extracted from the proof of @{text prop2}:
+  @{thm [display] prop2_def [no_vars]}
+  Program extracted from the proof of @{text prop3}:
+  @{thm [display] prop3_def [no_vars]}
+*}
+
+
+subsection {* Some examples *}
+
+instantiation LT and TT :: default
+begin
+
+definition "default = L0 [] []"
+
+definition "default = T0 A [] [] [] R0"
+
+instance ..
+
+end
+
+function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+  "mk_word_aux k = exec {
+     i \<leftarrow> Random.range 10;
+     (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
+     else exec {
+       let l = (if i mod 2 = 0 then A else B);
+       ls \<leftarrow> mk_word_aux (Suc k);
+       Pair (l # ls)
+     })}"
+by pat_completeness auto
+termination by (relation "measure ((op -) 1001)") auto
+
+definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+  "mk_word = mk_word_aux 0"
+
+primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+  "mk_word_s 0 = mk_word"
+  | "mk_word_s (Suc n) = exec {
+       _ \<leftarrow> mk_word;
+       mk_word_s n
+     }"
+
+definition g1 :: "nat \<Rightarrow> letter list" where
+  "g1 s = fst (mk_word_s s (20000, 1))"
+
+definition g2 :: "nat \<Rightarrow> letter list" where
+  "g2 s = fst (mk_word_s s (50000, 1))"
+
+fun f1 :: "nat \<Rightarrow> letter list" where
+  "f1 0 = [A, A]"
+  | "f1 (Suc 0) = [B]"
+  | "f1 (Suc (Suc 0)) = [A, B]"
+  | "f1 _ = []"
+
+fun f2 :: "nat \<Rightarrow> letter list" where
+  "f2 0 = [A, A]"
+  | "f2 (Suc 0) = [B]"
+  | "f2 (Suc (Suc 0)) = [B, A]"
+  | "f2 _ = []"
+
+ML {*
+local
+  val higman_idx = @{code higman_idx};
+  val g1 = @{code g1};
+  val g2 = @{code g2};
+  val f1 = @{code f1};
+  val f2 = @{code f2};
+in
+  val (i1, j1) = higman_idx g1;
+  val (v1, w1) = (g1 i1, g1 j1);
+  val (i2, j2) = higman_idx g2;
+  val (v2, w2) = (g2 i2, g2 j2);
+  val (i3, j3) = higman_idx f1;
+  val (v3, w3) = (f1 i3, f1 j3);
+  val (i4, j4) = higman_idx f2;
+  val (v4, w4) = (f2 i4, f2 j4);
+end;
+*}
+
+text {* The same story with the legacy SML code generator,
+this can be removed once the code generator is removed. *}
+
+code_module Higman
+contains
+  higman = higman_idx
+
+ML {*
+local open Higman in
+
+val a = 16807.0;
+val m = 2147483647.0;
+
+fun nextRand seed =
+  let val t = a*seed
+  in  t - m * real (Real.floor(t/m)) end;
+
+fun mk_word seed l =
+  let
+    val r = nextRand seed;
+    val i = Real.round (r / m * 10.0);
+  in if i > 7 andalso l > 2 then (r, []) else
+    apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
+  end;
+
+fun f s zero = mk_word s 0
+  | f s (Suc n) = f (fst (mk_word s 0)) n;
+
+val g1 = snd o (f 20000.0);
+
+val g2 = snd o (f 50000.0);
+
+fun f1 zero = [A,A]
+  | f1 (Suc zero) = [B]
+  | f1 (Suc (Suc zero)) = [A,B]
+  | f1 _ = [];
+
+fun f2 zero = [A,A]
+  | f2 (Suc zero) = [B]
+  | f2 (Suc (Suc zero)) = [B,A]
+  | f2 _ = [];
+
+val (i1, j1) = higman g1;
+val (v1, w1) = (g1 i1, g1 j1);
+val (i2, j2) = higman g2;
+val (v2, w2) = (g2 i2, g2 j2);
+val (i3, j3) = higman f1;
+val (v3, w3) = (f1 i3, f1 j3);
+val (i4, j4) = higman f2;
+val (v4, w4) = (f2 i4, f2 j4);
+
+end;
+*}
+
+end

--- a/src/HOL/Proofs/Extraction/ROOT.ML	Thu Sep 22 17:15:46 2011 +0200
+++ b/src/HOL/Proofs/Extraction/ROOT.ML	Thu Sep 22 18:23:38 2011 +0200
@@ -8,5 +8,5 @@
 
 share_common_data ();
 
-no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
-use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
+no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization", "~~/src/HOL/Library/State_Monad"];
+use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"];