# HG changeset patch # User berghofe # Date 1316708618 -7200 # Node ID 3aa8d3c391a4f63f910dd8ecbbf4ecbe08969675 # Parent 5ff8cd3b1673e1ade93d95cb8742ec4e06fa2e79 Moved extraction part of Higman's lemma to separate theory to allow reuse in theories compiled without support for proof terms. diff -r 5ff8cd3b1673 -r 3aa8d3c391a4 src/HOL/IsaMakefile --- 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 \ diff -r 5ff8cd3b1673 -r 3aa8d3c391a4 src/HOL/Proofs/Extraction/Higman.thy --- 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 \ Random.seed \ letter list \ Random.seed" where - "mk_word_aux k = exec { - i \ Random.range 10; - (if i > 7 \ k > 2 \ k > 1000 then Pair [] - else exec { - let l = (if i mod 2 = 0 then A else B); - ls \ mk_word_aux (Suc k); - Pair (l # ls) - })}" -by pat_completeness auto -termination by (relation "measure ((op -) 1001)") auto - -definition mk_word :: "Random.seed \ letter list \ Random.seed" where - "mk_word = mk_word_aux 0" - -primrec mk_word_s :: "nat \ Random.seed \ letter list \ Random.seed" where - "mk_word_s 0 = mk_word" - | "mk_word_s (Suc n) = exec { - _ \ mk_word; - mk_word_s n - }" - -definition g1 :: "nat \ letter list" where - "g1 s = fst (mk_word_s s (20000, 1))" - -definition g2 :: "nat \ letter list" where - "g2 s = fst (mk_word_s s (50000, 1))" - -fun f1 :: "nat \ letter list" where - "f1 0 = [A, A]" - | "f1 (Suc 0) = [B]" - | "f1 (Suc (Suc 0)) = [A, B]" - | "f1 _ = []" - -fun f2 :: "nat \ 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 +(*>*) diff -r 5ff8cd3b1673 -r 3aa8d3c391a4 src/HOL/Proofs/Extraction/Higman_Extraction.thy --- /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 \ Random.seed \ letter list \ Random.seed" where + "mk_word_aux k = exec { + i \ Random.range 10; + (if i > 7 \ k > 2 \ k > 1000 then Pair [] + else exec { + let l = (if i mod 2 = 0 then A else B); + ls \ mk_word_aux (Suc k); + Pair (l # ls) + })}" +by pat_completeness auto +termination by (relation "measure ((op -) 1001)") auto + +definition mk_word :: "Random.seed \ letter list \ Random.seed" where + "mk_word = mk_word_aux 0" + +primrec mk_word_s :: "nat \ Random.seed \ letter list \ Random.seed" where + "mk_word_s 0 = mk_word" + | "mk_word_s (Suc n) = exec { + _ \ mk_word; + mk_word_s n + }" + +definition g1 :: "nat \ letter list" where + "g1 s = fst (mk_word_s s (20000, 1))" + +definition g2 :: "nat \ letter list" where + "g2 s = fst (mk_word_s s (50000, 1))" + +fun f1 :: "nat \ letter list" where + "f1 0 = [A, A]" + | "f1 (Suc 0) = [B]" + | "f1 (Suc (Suc 0)) = [A, B]" + | "f1 _ = []" + +fun f2 :: "nat \ 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 diff -r 5ff8cd3b1673 -r 3aa8d3c391a4 src/HOL/Proofs/Extraction/ROOT.ML --- 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"];