1.1 --- a/src/HOL/IsaMakefile Thu Sep 22 17:15:46 2011 +0200
1.2 +++ b/src/HOL/IsaMakefile Thu Sep 22 18:23:38 2011 +0200
1.3 @@ -915,7 +915,8 @@
1.4 $(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \
1.5 Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy \
1.6 Proofs/Extraction/Greatest_Common_Divisor.thy \
1.7 - Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy \
1.8 + Proofs/Extraction/Higman.thy Proofs/Extraction/Higman_Extraction.thy \
1.9 + Proofs/Extraction/Pigeonhole.thy \
1.10 Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML \
1.11 Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy \
1.12 Proofs/Extraction/document/root.tex \
2.1 --- a/src/HOL/Proofs/Extraction/Higman.thy Thu Sep 22 17:15:46 2011 +0200
2.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy Thu Sep 22 18:23:38 2011 +0200
2.3 @@ -6,7 +6,7 @@
2.4 header {* Higman's lemma *}
2.5
2.6 theory Higman
2.7 -imports Main "~~/src/HOL/Library/State_Monad" Random
2.8 +imports Main
2.9 begin
2.10
2.11 text {*
2.12 @@ -310,156 +310,6 @@
2.13 using higman
2.14 by (rule good_prefix_lemma) simp+
2.15
2.16 -subsection {* Extracting the program *}
2.17 -
2.18 -declare R.induct [ind_realizer]
2.19 -declare T.induct [ind_realizer]
2.20 -declare L.induct [ind_realizer]
2.21 -declare good.induct [ind_realizer]
2.22 -declare bar.induct [ind_realizer]
2.23 -
2.24 -extract higman_idx
2.25 -
2.26 -text {*
2.27 - Program extracted from the proof of @{text higman_idx}:
2.28 - @{thm [display] higman_idx_def [no_vars]}
2.29 - Corresponding correctness theorem:
2.30 - @{thm [display] higman_idx_correctness [no_vars]}
2.31 - Program extracted from the proof of @{text higman}:
2.32 - @{thm [display] higman_def [no_vars]}
2.33 - Program extracted from the proof of @{text prop1}:
2.34 - @{thm [display] prop1_def [no_vars]}
2.35 - Program extracted from the proof of @{text prop2}:
2.36 - @{thm [display] prop2_def [no_vars]}
2.37 - Program extracted from the proof of @{text prop3}:
2.38 - @{thm [display] prop3_def [no_vars]}
2.39 -*}
2.40 -
2.41 -
2.42 -subsection {* Some examples *}
2.43 -
2.44 -instantiation LT and TT :: default
2.45 -begin
2.46 -
2.47 -definition "default = L0 [] []"
2.48 -
2.49 -definition "default = T0 A [] [] [] R0"
2.50 -
2.51 -instance ..
2.52 -
2.53 +(*<*)
2.54 end
2.55 -
2.56 -function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
2.57 - "mk_word_aux k = exec {
2.58 - i \<leftarrow> Random.range 10;
2.59 - (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
2.60 - else exec {
2.61 - let l = (if i mod 2 = 0 then A else B);
2.62 - ls \<leftarrow> mk_word_aux (Suc k);
2.63 - Pair (l # ls)
2.64 - })}"
2.65 -by pat_completeness auto
2.66 -termination by (relation "measure ((op -) 1001)") auto
2.67 -
2.68 -definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
2.69 - "mk_word = mk_word_aux 0"
2.70 -
2.71 -primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
2.72 - "mk_word_s 0 = mk_word"
2.73 - | "mk_word_s (Suc n) = exec {
2.74 - _ \<leftarrow> mk_word;
2.75 - mk_word_s n
2.76 - }"
2.77 -
2.78 -definition g1 :: "nat \<Rightarrow> letter list" where
2.79 - "g1 s = fst (mk_word_s s (20000, 1))"
2.80 -
2.81 -definition g2 :: "nat \<Rightarrow> letter list" where
2.82 - "g2 s = fst (mk_word_s s (50000, 1))"
2.83 -
2.84 -fun f1 :: "nat \<Rightarrow> letter list" where
2.85 - "f1 0 = [A, A]"
2.86 - | "f1 (Suc 0) = [B]"
2.87 - | "f1 (Suc (Suc 0)) = [A, B]"
2.88 - | "f1 _ = []"
2.89 -
2.90 -fun f2 :: "nat \<Rightarrow> letter list" where
2.91 - "f2 0 = [A, A]"
2.92 - | "f2 (Suc 0) = [B]"
2.93 - | "f2 (Suc (Suc 0)) = [B, A]"
2.94 - | "f2 _ = []"
2.95 -
2.96 -ML {*
2.97 -local
2.98 - val higman_idx = @{code higman_idx};
2.99 - val g1 = @{code g1};
2.100 - val g2 = @{code g2};
2.101 - val f1 = @{code f1};
2.102 - val f2 = @{code f2};
2.103 -in
2.104 - val (i1, j1) = higman_idx g1;
2.105 - val (v1, w1) = (g1 i1, g1 j1);
2.106 - val (i2, j2) = higman_idx g2;
2.107 - val (v2, w2) = (g2 i2, g2 j2);
2.108 - val (i3, j3) = higman_idx f1;
2.109 - val (v3, w3) = (f1 i3, f1 j3);
2.110 - val (i4, j4) = higman_idx f2;
2.111 - val (v4, w4) = (f2 i4, f2 j4);
2.112 -end;
2.113 -*}
2.114 -
2.115 -text {* The same story with the legacy SML code generator,
2.116 -this can be removed once the code generator is removed. *}
2.117 -
2.118 -code_module Higman
2.119 -contains
2.120 - higman = higman_idx
2.121 -
2.122 -ML {*
2.123 -local open Higman in
2.124 -
2.125 -val a = 16807.0;
2.126 -val m = 2147483647.0;
2.127 -
2.128 -fun nextRand seed =
2.129 - let val t = a*seed
2.130 - in t - m * real (Real.floor(t/m)) end;
2.131 -
2.132 -fun mk_word seed l =
2.133 - let
2.134 - val r = nextRand seed;
2.135 - val i = Real.round (r / m * 10.0);
2.136 - in if i > 7 andalso l > 2 then (r, []) else
2.137 - apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
2.138 - end;
2.139 -
2.140 -fun f s zero = mk_word s 0
2.141 - | f s (Suc n) = f (fst (mk_word s 0)) n;
2.142 -
2.143 -val g1 = snd o (f 20000.0);
2.144 -
2.145 -val g2 = snd o (f 50000.0);
2.146 -
2.147 -fun f1 zero = [A,A]
2.148 - | f1 (Suc zero) = [B]
2.149 - | f1 (Suc (Suc zero)) = [A,B]
2.150 - | f1 _ = [];
2.151 -
2.152 -fun f2 zero = [A,A]
2.153 - | f2 (Suc zero) = [B]
2.154 - | f2 (Suc (Suc zero)) = [B,A]
2.155 - | f2 _ = [];
2.156 -
2.157 -val (i1, j1) = higman g1;
2.158 -val (v1, w1) = (g1 i1, g1 j1);
2.159 -val (i2, j2) = higman g2;
2.160 -val (v2, w2) = (g2 i2, g2 j2);
2.161 -val (i3, j3) = higman f1;
2.162 -val (v3, w3) = (f1 i3, f1 j3);
2.163 -val (i4, j4) = higman f2;
2.164 -val (v4, w4) = (f2 i4, f2 j4);
2.165 -
2.166 -end;
2.167 -*}
2.168 -
2.169 -end
2.170 +(*>*)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Thu Sep 22 18:23:38 2011 +0200
3.3 @@ -0,0 +1,164 @@
3.4 +(* Title: HOL/Proofs/Extraction/Higman_Extraction.thy
3.5 + Author: Stefan Berghofer, TU Muenchen
3.6 + Author: Monika Seisenberger, LMU Muenchen
3.7 +*)
3.8 +
3.9 +(*<*)
3.10 +theory Higman_Extraction
3.11 +imports Higman "~~/src/HOL/Library/State_Monad" Random
3.12 +begin
3.13 +(*>*)
3.14 +
3.15 +subsection {* Extracting the program *}
3.16 +
3.17 +declare R.induct [ind_realizer]
3.18 +declare T.induct [ind_realizer]
3.19 +declare L.induct [ind_realizer]
3.20 +declare good.induct [ind_realizer]
3.21 +declare bar.induct [ind_realizer]
3.22 +
3.23 +extract higman_idx
3.24 +
3.25 +text {*
3.26 + Program extracted from the proof of @{text higman_idx}:
3.27 + @{thm [display] higman_idx_def [no_vars]}
3.28 + Corresponding correctness theorem:
3.29 + @{thm [display] higman_idx_correctness [no_vars]}
3.30 + Program extracted from the proof of @{text higman}:
3.31 + @{thm [display] higman_def [no_vars]}
3.32 + Program extracted from the proof of @{text prop1}:
3.33 + @{thm [display] prop1_def [no_vars]}
3.34 + Program extracted from the proof of @{text prop2}:
3.35 + @{thm [display] prop2_def [no_vars]}
3.36 + Program extracted from the proof of @{text prop3}:
3.37 + @{thm [display] prop3_def [no_vars]}
3.38 +*}
3.39 +
3.40 +
3.41 +subsection {* Some examples *}
3.42 +
3.43 +instantiation LT and TT :: default
3.44 +begin
3.45 +
3.46 +definition "default = L0 [] []"
3.47 +
3.48 +definition "default = T0 A [] [] [] R0"
3.49 +
3.50 +instance ..
3.51 +
3.52 +end
3.53 +
3.54 +function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
3.55 + "mk_word_aux k = exec {
3.56 + i \<leftarrow> Random.range 10;
3.57 + (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
3.58 + else exec {
3.59 + let l = (if i mod 2 = 0 then A else B);
3.60 + ls \<leftarrow> mk_word_aux (Suc k);
3.61 + Pair (l # ls)
3.62 + })}"
3.63 +by pat_completeness auto
3.64 +termination by (relation "measure ((op -) 1001)") auto
3.65 +
3.66 +definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
3.67 + "mk_word = mk_word_aux 0"
3.68 +
3.69 +primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
3.70 + "mk_word_s 0 = mk_word"
3.71 + | "mk_word_s (Suc n) = exec {
3.72 + _ \<leftarrow> mk_word;
3.73 + mk_word_s n
3.74 + }"
3.75 +
3.76 +definition g1 :: "nat \<Rightarrow> letter list" where
3.77 + "g1 s = fst (mk_word_s s (20000, 1))"
3.78 +
3.79 +definition g2 :: "nat \<Rightarrow> letter list" where
3.80 + "g2 s = fst (mk_word_s s (50000, 1))"
3.81 +
3.82 +fun f1 :: "nat \<Rightarrow> letter list" where
3.83 + "f1 0 = [A, A]"
3.84 + | "f1 (Suc 0) = [B]"
3.85 + | "f1 (Suc (Suc 0)) = [A, B]"
3.86 + | "f1 _ = []"
3.87 +
3.88 +fun f2 :: "nat \<Rightarrow> letter list" where
3.89 + "f2 0 = [A, A]"
3.90 + | "f2 (Suc 0) = [B]"
3.91 + | "f2 (Suc (Suc 0)) = [B, A]"
3.92 + | "f2 _ = []"
3.93 +
3.94 +ML {*
3.95 +local
3.96 + val higman_idx = @{code higman_idx};
3.97 + val g1 = @{code g1};
3.98 + val g2 = @{code g2};
3.99 + val f1 = @{code f1};
3.100 + val f2 = @{code f2};
3.101 +in
3.102 + val (i1, j1) = higman_idx g1;
3.103 + val (v1, w1) = (g1 i1, g1 j1);
3.104 + val (i2, j2) = higman_idx g2;
3.105 + val (v2, w2) = (g2 i2, g2 j2);
3.106 + val (i3, j3) = higman_idx f1;
3.107 + val (v3, w3) = (f1 i3, f1 j3);
3.108 + val (i4, j4) = higman_idx f2;
3.109 + val (v4, w4) = (f2 i4, f2 j4);
3.110 +end;
3.111 +*}
3.112 +
3.113 +text {* The same story with the legacy SML code generator,
3.114 +this can be removed once the code generator is removed. *}
3.115 +
3.116 +code_module Higman
3.117 +contains
3.118 + higman = higman_idx
3.119 +
3.120 +ML {*
3.121 +local open Higman in
3.122 +
3.123 +val a = 16807.0;
3.124 +val m = 2147483647.0;
3.125 +
3.126 +fun nextRand seed =
3.127 + let val t = a*seed
3.128 + in t - m * real (Real.floor(t/m)) end;
3.129 +
3.130 +fun mk_word seed l =
3.131 + let
3.132 + val r = nextRand seed;
3.133 + val i = Real.round (r / m * 10.0);
3.134 + in if i > 7 andalso l > 2 then (r, []) else
3.135 + apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
3.136 + end;
3.137 +
3.138 +fun f s zero = mk_word s 0
3.139 + | f s (Suc n) = f (fst (mk_word s 0)) n;
3.140 +
3.141 +val g1 = snd o (f 20000.0);
3.142 +
3.143 +val g2 = snd o (f 50000.0);
3.144 +
3.145 +fun f1 zero = [A,A]
3.146 + | f1 (Suc zero) = [B]
3.147 + | f1 (Suc (Suc zero)) = [A,B]
3.148 + | f1 _ = [];
3.149 +
3.150 +fun f2 zero = [A,A]
3.151 + | f2 (Suc zero) = [B]
3.152 + | f2 (Suc (Suc zero)) = [B,A]
3.153 + | f2 _ = [];
3.154 +
3.155 +val (i1, j1) = higman g1;
3.156 +val (v1, w1) = (g1 i1, g1 j1);
3.157 +val (i2, j2) = higman g2;
3.158 +val (v2, w2) = (g2 i2, g2 j2);
3.159 +val (i3, j3) = higman f1;
3.160 +val (v3, w3) = (f1 i3, f1 j3);
3.161 +val (i4, j4) = higman f2;
3.162 +val (v4, w4) = (f2 i4, f2 j4);
3.163 +
3.164 +end;
3.165 +*}
3.166 +
3.167 +end
4.1 --- a/src/HOL/Proofs/Extraction/ROOT.ML Thu Sep 22 17:15:46 2011 +0200
4.2 +++ b/src/HOL/Proofs/Extraction/ROOT.ML Thu Sep 22 18:23:38 2011 +0200
4.3 @@ -8,5 +8,5 @@
4.4
4.5 share_common_data ();
4.6
4.7 -no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
4.8 -use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
4.9 +no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization", "~~/src/HOL/Library/State_Monad"];
4.10 +use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"];