author | Lars Hupel <lars.hupel@mytum.de> |
Tue, 11 Jul 2017 17:22:33 +0200 | |
changeset 66270 | 403d84138c5c |
parent 66258 | 2b83dd24b301 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Proofs/Extraction/Higman_Extraction.thy |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
2 |
Author: Stefan Berghofer, TU Muenchen |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
3 |
Author: Monika Seisenberger, LMU Muenchen |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
4 |
*) |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
5 |
|
63361 | 6 |
subsection \<open>Extracting the program\<close> |
7 |
||
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
8 |
theory Higman_Extraction |
66270
403d84138c5c
State_Monad ~> Open_State_Syntax
Lars Hupel <lars.hupel@mytum.de>
parents:
66258
diff
changeset
|
9 |
imports Higman Old_Datatype "~~/src/HOL/Library/Open_State_Syntax" |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
10 |
begin |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
11 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
12 |
declare R.induct [ind_realizer] |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
13 |
declare T.induct [ind_realizer] |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
14 |
declare L.induct [ind_realizer] |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
15 |
declare good.induct [ind_realizer] |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
16 |
declare bar.induct [ind_realizer] |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
17 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
18 |
extract higman_idx |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
19 |
|
61986 | 20 |
text \<open> |
21 |
Program extracted from the proof of \<open>higman_idx\<close>: |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
22 |
@{thm [display] higman_idx_def [no_vars]} |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
23 |
Corresponding correctness theorem: |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
24 |
@{thm [display] higman_idx_correctness [no_vars]} |
61986 | 25 |
Program extracted from the proof of \<open>higman\<close>: |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
26 |
@{thm [display] higman_def [no_vars]} |
61986 | 27 |
Program extracted from the proof of \<open>prop1\<close>: |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
28 |
@{thm [display] prop1_def [no_vars]} |
61986 | 29 |
Program extracted from the proof of \<open>prop2\<close>: |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
30 |
@{thm [display] prop2_def [no_vars]} |
61986 | 31 |
Program extracted from the proof of \<open>prop3\<close>: |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
32 |
@{thm [display] prop3_def [no_vars]} |
61986 | 33 |
\<close> |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
34 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
35 |
|
61986 | 36 |
subsection \<open>Some examples\<close> |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
37 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
38 |
instantiation LT and TT :: default |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
39 |
begin |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
40 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
41 |
definition "default = L0 [] []" |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
42 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
43 |
definition "default = T0 A [] [] [] R0" |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
44 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
45 |
instance .. |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
46 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
47 |
end |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
48 |
|
63361 | 49 |
function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" |
50 |
where |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
51 |
"mk_word_aux k = exec { |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
52 |
i \<leftarrow> Random.range 10; |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
53 |
(if i > 7 \<and> k > 2 \<or> k > 1000 then Pair [] |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
54 |
else exec { |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
55 |
let l = (if i mod 2 = 0 then A else B); |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
56 |
ls \<leftarrow> mk_word_aux (Suc k); |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
57 |
Pair (l # ls) |
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
58 |
})}" |
63361 | 59 |
by pat_completeness auto |
60 |
termination |
|
61 |
by (relation "measure ((op -) 1001)") auto |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
62 |
|
63361 | 63 |
definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" |
64 |
where "mk_word = mk_word_aux 0" |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
65 |
|
63361 | 66 |
primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" |
67 |
where |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
68 |
"mk_word_s 0 = mk_word" |
63361 | 69 |
| "mk_word_s (Suc n) = exec { |
70 |
_ \<leftarrow> mk_word; |
|
71 |
mk_word_s n |
|
72 |
}" |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
73 |
|
63361 | 74 |
definition g1 :: "nat \<Rightarrow> letter list" |
75 |
where "g1 s = fst (mk_word_s s (20000, 1))" |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
76 |
|
63361 | 77 |
definition g2 :: "nat \<Rightarrow> letter list" |
78 |
where "g2 s = fst (mk_word_s s (50000, 1))" |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
79 |
|
63361 | 80 |
fun f1 :: "nat \<Rightarrow> letter list" |
81 |
where |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
82 |
"f1 0 = [A, A]" |
63361 | 83 |
| "f1 (Suc 0) = [B]" |
84 |
| "f1 (Suc (Suc 0)) = [A, B]" |
|
85 |
| "f1 _ = []" |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
86 |
|
63361 | 87 |
fun f2 :: "nat \<Rightarrow> letter list" |
88 |
where |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
89 |
"f2 0 = [A, A]" |
63361 | 90 |
| "f2 (Suc 0) = [B]" |
91 |
| "f2 (Suc (Suc 0)) = [B, A]" |
|
92 |
| "f2 _ = []" |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
93 |
|
61986 | 94 |
ML_val \<open> |
63361 | 95 |
local |
96 |
val higman_idx = @{code higman_idx}; |
|
97 |
val g1 = @{code g1}; |
|
98 |
val g2 = @{code g2}; |
|
99 |
val f1 = @{code f1}; |
|
100 |
val f2 = @{code f2}; |
|
101 |
in |
|
102 |
val (i1, j1) = higman_idx g1; |
|
103 |
val (v1, w1) = (g1 i1, g1 j1); |
|
104 |
val (i2, j2) = higman_idx g2; |
|
105 |
val (v2, w2) = (g2 i2, g2 j2); |
|
106 |
val (i3, j3) = higman_idx f1; |
|
107 |
val (v3, w3) = (f1 i3, f1 j3); |
|
108 |
val (i4, j4) = higman_idx f2; |
|
109 |
val (v4, w4) = (f2 i4, f2 j4); |
|
110 |
end; |
|
61986 | 111 |
\<close> |
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
112 |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
diff
changeset
|
113 |
end |