author | wenzelm |
Sun, 20 Nov 2011 21:07:06 +0100 | |
changeset 45606 | b1e1508643b1 |
parent 45294 | 3c5d3d286055 |
child 45654 | cf10bde35973 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/Domain/domain_take_proofs.ML |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
3 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
4 |
Defines take functions for the given domain equation |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
5 |
and proves related theorems. |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
6 |
*) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
7 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
8 |
signature DOMAIN_TAKE_PROOFS = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
9 |
sig |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
10 |
type iso_info = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
11 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
12 |
absT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
13 |
repT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
14 |
abs_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
15 |
rep_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
16 |
abs_inverse : thm, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
17 |
rep_inverse : thm |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
18 |
} |
35651 | 19 |
type take_info = |
35659 | 20 |
{ |
21 |
take_consts : term list, |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
22 |
take_defs : thm list, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
23 |
chain_take_thms : thm list, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
24 |
take_0_thms : thm list, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
25 |
take_Suc_thms : thm list, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
26 |
deflation_take_thms : thm list, |
40015 | 27 |
take_strict_thms : thm list, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
28 |
finite_consts : term list, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
29 |
finite_defs : thm list |
35651 | 30 |
} |
35656 | 31 |
type take_induct_info = |
32 |
{ |
|
35659 | 33 |
take_consts : term list, |
34 |
take_defs : thm list, |
|
35 |
chain_take_thms : thm list, |
|
36 |
take_0_thms : thm list, |
|
37 |
take_Suc_thms : thm list, |
|
38 |
deflation_take_thms : thm list, |
|
40015 | 39 |
take_strict_thms : thm list, |
35659 | 40 |
finite_consts : term list, |
41 |
finite_defs : thm list, |
|
42 |
lub_take_thms : thm list, |
|
43 |
reach_thms : thm list, |
|
44 |
take_lemma_thms : thm list, |
|
45 |
is_finite : bool, |
|
46 |
take_induct_thms : thm list |
|
35656 | 47 |
} |
35651 | 48 |
val define_take_functions : |
49 |
(binding * iso_info) list -> theory -> take_info * theory |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
50 |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
51 |
val add_lub_take_theorems : |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
52 |
(binding * iso_info) list -> take_info -> thm list -> |
35656 | 53 |
theory -> take_induct_info * theory |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
54 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
55 |
val map_of_typ : |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
56 |
theory -> (typ * term) list -> typ -> term |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
57 |
|
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40489
diff
changeset
|
58 |
val add_rec_type : (string * bool list) -> theory -> theory |
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40489
diff
changeset
|
59 |
val get_rec_tab : theory -> (bool list) Symtab.table |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
60 |
val add_deflation_thm : thm -> theory -> theory |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
61 |
val get_deflation_thms : theory -> thm list |
40489 | 62 |
val map_ID_add : attribute |
63 |
val get_map_ID_thms : theory -> thm list |
|
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
64 |
val setup : theory -> theory |
40832 | 65 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
66 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
67 |
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
68 |
struct |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
69 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
70 |
type iso_info = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
71 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
72 |
absT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
73 |
repT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
74 |
abs_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
75 |
rep_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
76 |
abs_inverse : thm, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
77 |
rep_inverse : thm |
40832 | 78 |
} |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
79 |
|
35651 | 80 |
type take_info = |
81 |
{ take_consts : term list, |
|
82 |
take_defs : thm list, |
|
83 |
chain_take_thms : thm list, |
|
84 |
take_0_thms : thm list, |
|
85 |
take_Suc_thms : thm list, |
|
86 |
deflation_take_thms : thm list, |
|
40015 | 87 |
take_strict_thms : thm list, |
35651 | 88 |
finite_consts : term list, |
89 |
finite_defs : thm list |
|
40832 | 90 |
} |
35651 | 91 |
|
35656 | 92 |
type take_induct_info = |
93 |
{ |
|
35659 | 94 |
take_consts : term list, |
95 |
take_defs : thm list, |
|
96 |
chain_take_thms : thm list, |
|
97 |
take_0_thms : thm list, |
|
98 |
take_Suc_thms : thm list, |
|
99 |
deflation_take_thms : thm list, |
|
40015 | 100 |
take_strict_thms : thm list, |
35659 | 101 |
finite_consts : term list, |
102 |
finite_defs : thm list, |
|
103 |
lub_take_thms : thm list, |
|
104 |
reach_thms : thm list, |
|
105 |
take_lemma_thms : thm list, |
|
106 |
is_finite : bool, |
|
107 |
take_induct_thms : thm list |
|
40832 | 108 |
} |
35656 | 109 |
|
40833
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
110 |
val beta_ss = |
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
111 |
HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}] |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
112 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
113 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
114 |
(******************************** theory data *********************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
115 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
116 |
|
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40489
diff
changeset
|
117 |
structure Rec_Data = Theory_Data |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
118 |
( |
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40489
diff
changeset
|
119 |
(* list indicates which type arguments allow indirect recursion *) |
40832 | 120 |
type T = (bool list) Symtab.table |
121 |
val empty = Symtab.empty |
|
122 |
val extend = I |
|
123 |
fun merge data = Symtab.merge (K true) data |
|
124 |
) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
125 |
|
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
126 |
structure DeflMapData = Named_Thms |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
127 |
( |
45294 | 128 |
val name = @{binding domain_deflation} |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
129 |
val description = "theorems like deflation a ==> deflation (foo_map$a)" |
40832 | 130 |
) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
131 |
|
40489 | 132 |
structure Map_Id_Data = Named_Thms |
133 |
( |
|
45294 | 134 |
val name = @{binding domain_map_ID} |
40489 | 135 |
val description = "theorems like foo_map$ID = ID" |
40832 | 136 |
) |
40489 | 137 |
|
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40489
diff
changeset
|
138 |
fun add_rec_type (tname, bs) = |
40832 | 139 |
Rec_Data.map (Symtab.insert (K true) (tname, bs)) |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
140 |
|
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
141 |
fun add_deflation_thm thm = |
40832 | 142 |
Context.theory_map (DeflMapData.add_thm thm) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
143 |
|
40832 | 144 |
val get_rec_tab = Rec_Data.get |
42361 | 145 |
fun get_deflation_thms thy = DeflMapData.get (Proof_Context.init_global thy) |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
146 |
|
40832 | 147 |
val map_ID_add = Map_Id_Data.add |
42361 | 148 |
val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global |
40489 | 149 |
|
40832 | 150 |
val setup = DeflMapData.setup #> Map_Id_Data.setup |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
151 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
152 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
153 |
(************************** building types and terms **************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
154 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
155 |
|
40832 | 156 |
open HOLCF_Library |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
157 |
|
40832 | 158 |
infixr 6 ->> |
159 |
infix -->> |
|
160 |
infix 9 ` |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
161 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
162 |
fun mk_deflation t = |
40832 | 163 |
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
164 |
|
40832 | 165 |
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
166 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
167 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
168 |
(****************************** isomorphism info ******************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
169 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
170 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
171 |
fun deflation_abs_rep (info : iso_info) : thm = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
172 |
let |
40832 | 173 |
val abs_iso = #abs_inverse info |
174 |
val rep_iso = #rep_inverse info |
|
175 |
val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso] |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
176 |
in |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
177 |
Drule.zero_var_indexes thm |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
178 |
end |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
179 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
180 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
181 |
(********************* building map functions over types **********************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
182 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
183 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
184 |
fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
185 |
let |
40832 | 186 |
val thms = get_map_ID_thms thy |
187 |
val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms |
|
188 |
val rules' = map (apfst mk_ID) sub @ map swap rules |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
189 |
in |
40489 | 190 |
mk_ID T |
191 |
|> Pattern.rewrite_term thy rules' [] |
|
192 |
|> Pattern.rewrite_term thy rules [] |
|
40832 | 193 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
194 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
195 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
196 |
(********************* declaring definitions and theorems *********************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
197 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
198 |
|
35773 | 199 |
fun add_qualified_def name (dbind, eqn) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
200 |
yield_singleton (Global_Theory.add_defs false) |
40832 | 201 |
((Binding.qualified true name dbind, eqn), []) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
202 |
|
35773 | 203 |
fun add_qualified_thm name (dbind, thm) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
204 |
yield_singleton Global_Theory.add_thms |
40832 | 205 |
((Binding.qualified true name dbind, thm), []) |
35650 | 206 |
|
35773 | 207 |
fun add_qualified_simp_thm name (dbind, thm) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
208 |
yield_singleton Global_Theory.add_thms |
40832 | 209 |
((Binding.qualified true name dbind, thm), [Simplifier.simp_add]) |
35573 | 210 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
211 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
212 |
(************************** defining take functions ***************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
213 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
214 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
215 |
fun define_take_functions |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
216 |
(spec : (binding * iso_info) list) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
217 |
(thy : theory) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
218 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
219 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
220 |
(* retrieve components of spec *) |
40832 | 221 |
val dbinds = map fst spec |
222 |
val iso_infos = map snd spec |
|
223 |
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos |
|
224 |
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
225 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
226 |
fun mk_projs [] _ = [] |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
227 |
| mk_projs (x::[]) t = [(x, t)] |
40832 | 228 |
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
229 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
230 |
fun mk_cfcomp2 ((rep_const, abs_const), f) = |
40832 | 231 |
mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
232 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
233 |
(* define take functional *) |
40832 | 234 |
val newTs : typ list = map fst dom_eqns |
235 |
val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs) |
|
236 |
val copy_arg = Free ("f", copy_arg_type) |
|
237 |
val copy_args = map snd (mk_projs dbinds copy_arg) |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
238 |
fun one_copy_rhs (rep_abs, (_, rhsT)) = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
239 |
let |
40832 | 240 |
val body = map_of_typ thy (newTs ~~ copy_args) rhsT |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
241 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
242 |
mk_cfcomp2 (rep_abs, body) |
40832 | 243 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
244 |
val take_functional = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
245 |
big_lambda copy_arg |
40832 | 246 |
(mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
247 |
val take_rhss = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
248 |
let |
40832 | 249 |
val n = Free ("n", HOLogic.natT) |
250 |
val rhs = mk_iterate (n, take_functional) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
251 |
in |
35773 | 252 |
map (lambda n o snd) (mk_projs dbinds rhs) |
40832 | 253 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
254 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
255 |
(* define take constants *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
256 |
fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
257 |
let |
40832 | 258 |
val take_type = HOLogic.natT --> lhsT ->> lhsT |
259 |
val take_bind = Binding.suffix_name "_take" dbind |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
260 |
val (take_const, thy) = |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
261 |
Sign.declare_const_global ((take_bind, take_type), NoSyn) thy |
40832 | 262 |
val take_eqn = Logic.mk_equals (take_const, take_rhs) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
263 |
val (take_def_thm, thy) = |
40832 | 264 |
add_qualified_def "take_def" (dbind, take_eqn) thy |
265 |
in ((take_const, take_def_thm), thy) end |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
266 |
val ((take_consts, take_defs), thy) = thy |
35773 | 267 |
|> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns) |
40832 | 268 |
|>> ListPair.unzip |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
269 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
270 |
(* prove chain_take lemmas *) |
35773 | 271 |
fun prove_chain_take (take_const, dbind) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
272 |
let |
40832 | 273 |
val goal = mk_trp (mk_chain take_const) |
274 |
val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd} |
|
275 |
val tac = simp_tac (HOL_basic_ss addsimps rules) 1 |
|
276 |
val thm = Goal.prove_global thy [] [] goal (K tac) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
277 |
in |
35773 | 278 |
add_qualified_simp_thm "chain_take" (dbind, thm) thy |
40832 | 279 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
280 |
val (chain_take_thms, thy) = |
40832 | 281 |
fold_map prove_chain_take (take_consts ~~ dbinds) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
282 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
283 |
(* prove take_0 lemmas *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
284 |
fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
285 |
let |
40832 | 286 |
val lhs = take_const $ @{term "0::nat"} |
287 |
val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)) |
|
288 |
val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict} |
|
289 |
val tac = simp_tac (HOL_basic_ss addsimps rules) 1 |
|
290 |
val take_0_thm = Goal.prove_global thy [] [] goal (K tac) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
291 |
in |
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40015
diff
changeset
|
292 |
add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy |
40832 | 293 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
294 |
val (take_0_thms, thy) = |
40832 | 295 |
fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
296 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
297 |
(* prove take_Suc lemmas *) |
40832 | 298 |
val n = Free ("n", natT) |
299 |
val take_is = map (fn t => t $ n) take_consts |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
300 |
fun prove_take_Suc |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
301 |
(((take_const, rep_abs), dbind), (_, rhsT)) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
302 |
let |
40832 | 303 |
val lhs = take_const $ (@{term Suc} $ n) |
304 |
val body = map_of_typ thy (newTs ~~ take_is) rhsT |
|
305 |
val rhs = mk_cfcomp2 (rep_abs, body) |
|
306 |
val goal = mk_eqs (lhs, rhs) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
307 |
val simps = @{thms iterate_Suc fst_conv snd_conv} |
40832 | 308 |
val rules = take_defs @ simps |
309 |
val tac = simp_tac (beta_ss addsimps rules) 1 |
|
310 |
val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
311 |
in |
35773 | 312 |
add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy |
40832 | 313 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
314 |
val (take_Suc_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
315 |
fold_map prove_take_Suc |
40832 | 316 |
(take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
317 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
318 |
(* prove deflation theorems for take functions *) |
40832 | 319 |
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
320 |
val deflation_take_thm = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
321 |
let |
40832 | 322 |
val n = Free ("n", natT) |
323 |
fun mk_goal take_const = mk_deflation (take_const $ n) |
|
324 |
val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
325 |
val bottom_rules = |
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40833
diff
changeset
|
326 |
take_0_thms @ @{thms deflation_bottom simp_thms} |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
327 |
val deflation_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
328 |
@{thms conjI deflation_ID} |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
329 |
@ deflation_abs_rep_thms |
40832 | 330 |
@ get_deflation_thms thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
331 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
332 |
Goal.prove_global thy [] [] goal (fn _ => |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
333 |
EVERY |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
334 |
[rtac @{thm nat.induct} 1, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
335 |
simp_tac (HOL_basic_ss addsimps bottom_rules) 1, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
336 |
asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
337 |
REPEAT (etac @{thm conjE} 1 |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
338 |
ORELSE resolve_tac deflation_rules 1 |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
339 |
ORELSE atac 1)]) |
40832 | 340 |
end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
341 |
fun conjuncts [] _ = [] |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
342 |
| conjuncts (n::[]) thm = [(n, thm)] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
343 |
| conjuncts (n::ns) thm = let |
40832 | 344 |
val thmL = thm RS @{thm conjunct1} |
345 |
val thmR = thm RS @{thm conjunct2} |
|
346 |
in (n, thmL):: conjuncts ns thmR end |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
347 |
val (deflation_take_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
348 |
fold_map (add_qualified_thm "deflation_take") |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
349 |
(map (apsnd Drule.zero_var_indexes) |
40832 | 350 |
(conjuncts dbinds deflation_take_thm)) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
351 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
352 |
(* prove strictness of take functions *) |
35773 | 353 |
fun prove_take_strict (deflation_take, dbind) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
354 |
let |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
355 |
val take_strict_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
356 |
Drule.zero_var_indexes |
40832 | 357 |
(@{thm deflation_strict} OF [deflation_take]) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
358 |
in |
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40015
diff
changeset
|
359 |
add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy |
40832 | 360 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
361 |
val (take_strict_thms, thy) = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
362 |
fold_map prove_take_strict |
40832 | 363 |
(deflation_take_thms ~~ dbinds) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
364 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
365 |
(* prove take/take rules *) |
35773 | 366 |
fun prove_take_take ((chain_take, deflation_take), dbind) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
367 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
368 |
val take_take_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
369 |
Drule.zero_var_indexes |
40832 | 370 |
(@{thm deflation_chain_min} OF [chain_take, deflation_take]) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
371 |
in |
35773 | 372 |
add_qualified_thm "take_take" (dbind, take_take_thm) thy |
40832 | 373 |
end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
374 |
val (_, thy) = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
375 |
fold_map prove_take_take |
40832 | 376 |
(chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
377 |
|
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
378 |
(* prove take_below rules *) |
35773 | 379 |
fun prove_take_below (deflation_take, dbind) thy = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
380 |
let |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
381 |
val take_below_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
382 |
Drule.zero_var_indexes |
40832 | 383 |
(@{thm deflation.below} OF [deflation_take]) |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
384 |
in |
35773 | 385 |
add_qualified_thm "take_below" (dbind, take_below_thm) thy |
40832 | 386 |
end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
387 |
val (_, thy) = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
388 |
fold_map prove_take_below |
40832 | 389 |
(deflation_take_thms ~~ dbinds) thy |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
390 |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
391 |
(* define finiteness predicates *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
392 |
fun define_finite_const ((dbind, take_const), (lhsT, _)) thy = |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
393 |
let |
40832 | 394 |
val finite_type = lhsT --> boolT |
395 |
val finite_bind = Binding.suffix_name "_finite" dbind |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
396 |
val (finite_const, thy) = |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
397 |
Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy |
40832 | 398 |
val x = Free ("x", lhsT) |
399 |
val n = Free ("n", natT) |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
400 |
val finite_rhs = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
401 |
lambda x (HOLogic.exists_const natT $ |
40832 | 402 |
(lambda n (mk_eq (mk_capply (take_const $ n, x), x)))) |
403 |
val finite_eqn = Logic.mk_equals (finite_const, finite_rhs) |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
404 |
val (finite_def_thm, thy) = |
40832 | 405 |
add_qualified_def "finite_def" (dbind, finite_eqn) thy |
406 |
in ((finite_const, finite_def_thm), thy) end |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
407 |
val ((finite_consts, finite_defs), thy) = thy |
35773 | 408 |
|> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns) |
40832 | 409 |
|>> ListPair.unzip |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
410 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
411 |
val result = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
412 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
413 |
take_consts = take_consts, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
414 |
take_defs = take_defs, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
415 |
chain_take_thms = chain_take_thms, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
416 |
take_0_thms = take_0_thms, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
417 |
take_Suc_thms = take_Suc_thms, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
418 |
deflation_take_thms = deflation_take_thms, |
40015 | 419 |
take_strict_thms = take_strict_thms, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
420 |
finite_consts = finite_consts, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
421 |
finite_defs = finite_defs |
40832 | 422 |
} |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
423 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
424 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
425 |
(result, thy) |
40832 | 426 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
427 |
|
35655 | 428 |
fun prove_finite_take_induct |
429 |
(spec : (binding * iso_info) list) |
|
430 |
(take_info : take_info) |
|
431 |
(lub_take_thms : thm list) |
|
432 |
(thy : theory) = |
|
433 |
let |
|
40832 | 434 |
val dbinds = map fst spec |
435 |
val iso_infos = map snd spec |
|
436 |
val absTs = map #absT iso_infos |
|
437 |
val {take_consts, ...} = take_info |
|
438 |
val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info |
|
439 |
val {finite_consts, finite_defs, ...} = take_info |
|
35655 | 440 |
|
441 |
val decisive_lemma = |
|
442 |
let |
|
37165 | 443 |
fun iso_locale (info : iso_info) = |
40832 | 444 |
@{thm iso.intro} OF [#abs_inverse info, #rep_inverse info] |
445 |
val iso_locale_thms = map iso_locale iso_infos |
|
35655 | 446 |
val decisive_abs_rep_thms = |
40832 | 447 |
map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms |
448 |
val n = Free ("n", @{typ nat}) |
|
35655 | 449 |
fun mk_decisive t = |
40832 | 450 |
Const (@{const_name decisive}, fastype_of t --> boolT) $ t |
451 |
fun f take_const = mk_decisive (take_const $ n) |
|
452 |
val goal = mk_trp (foldr1 mk_conj (map f take_consts)) |
|
453 |
val rules0 = @{thm decisive_bottom} :: take_0_thms |
|
35655 | 454 |
val rules1 = |
455 |
take_Suc_thms @ decisive_abs_rep_thms |
|
40832 | 456 |
@ @{thms decisive_ID decisive_ssum_map decisive_sprod_map} |
35655 | 457 |
val tac = EVERY [ |
458 |
rtac @{thm nat.induct} 1, |
|
459 |
simp_tac (HOL_ss addsimps rules0) 1, |
|
40832 | 460 |
asm_simp_tac (HOL_ss addsimps rules1) 1] |
461 |
in Goal.prove_global thy [] [] goal (K tac) end |
|
35655 | 462 |
fun conjuncts 1 thm = [thm] |
463 |
| conjuncts n thm = let |
|
40832 | 464 |
val thmL = thm RS @{thm conjunct1} |
465 |
val thmR = thm RS @{thm conjunct2} |
|
466 |
in thmL :: conjuncts (n-1) thmR end |
|
467 |
val decisive_thms = conjuncts (length spec) decisive_lemma |
|
35655 | 468 |
|
469 |
fun prove_finite_thm (absT, finite_const) = |
|
470 |
let |
|
40832 | 471 |
val goal = mk_trp (finite_const $ Free ("x", absT)) |
35655 | 472 |
val tac = |
473 |
EVERY [ |
|
474 |
rewrite_goals_tac finite_defs, |
|
475 |
rtac @{thm lub_ID_finite} 1, |
|
476 |
resolve_tac chain_take_thms 1, |
|
477 |
resolve_tac lub_take_thms 1, |
|
40832 | 478 |
resolve_tac decisive_thms 1] |
35655 | 479 |
in |
480 |
Goal.prove_global thy [] [] goal (K tac) |
|
40832 | 481 |
end |
35655 | 482 |
val finite_thms = |
40832 | 483 |
map prove_finite_thm (absTs ~~ finite_consts) |
35655 | 484 |
|
485 |
fun prove_take_induct ((ch_take, lub_take), decisive) = |
|
486 |
Drule.export_without_context |
|
40832 | 487 |
(@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]) |
35655 | 488 |
val take_induct_thms = |
489 |
map prove_take_induct |
|
40832 | 490 |
(chain_take_thms ~~ lub_take_thms ~~ decisive_thms) |
35655 | 491 |
|
492 |
val thy = thy |
|
493 |
|> fold (snd oo add_qualified_thm "finite") |
|
35773 | 494 |
(dbinds ~~ finite_thms) |
35655 | 495 |
|> fold (snd oo add_qualified_thm "take_induct") |
40832 | 496 |
(dbinds ~~ take_induct_thms) |
35655 | 497 |
in |
498 |
((finite_thms, take_induct_thms), thy) |
|
40832 | 499 |
end |
35655 | 500 |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
501 |
fun add_lub_take_theorems |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
502 |
(spec : (binding * iso_info) list) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
503 |
(take_info : take_info) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
504 |
(lub_take_thms : thm list) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
505 |
(thy : theory) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
506 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
507 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
508 |
(* retrieve components of spec *) |
40832 | 509 |
val dbinds = map fst spec |
510 |
val iso_infos = map snd spec |
|
511 |
val absTs = map #absT iso_infos |
|
512 |
val repTs = map #repT iso_infos |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
513 |
val {chain_take_thms, ...} = take_info |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
514 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
515 |
(* prove take lemmas *) |
35773 | 516 |
fun prove_take_lemma ((chain_take, lub_take), dbind) thy = |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
517 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
518 |
val take_lemma = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
519 |
Drule.export_without_context |
40832 | 520 |
(@{thm lub_ID_take_lemma} OF [chain_take, lub_take]) |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
521 |
in |
35773 | 522 |
add_qualified_thm "take_lemma" (dbind, take_lemma) thy |
40832 | 523 |
end |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
524 |
val (take_lemma_thms, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
525 |
fold_map prove_take_lemma |
40832 | 526 |
(chain_take_thms ~~ lub_take_thms ~~ dbinds) thy |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
527 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
528 |
(* prove reach lemmas *) |
35773 | 529 |
fun prove_reach_lemma ((chain_take, lub_take), dbind) thy = |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
530 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
531 |
val thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
532 |
Drule.zero_var_indexes |
40832 | 533 |
(@{thm lub_ID_reach} OF [chain_take, lub_take]) |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
534 |
in |
35773 | 535 |
add_qualified_thm "reach" (dbind, thm) thy |
40832 | 536 |
end |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
537 |
val (reach_thms, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
538 |
fold_map prove_reach_lemma |
40832 | 539 |
(chain_take_thms ~~ lub_take_thms ~~ dbinds) thy |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
540 |
|
35655 | 541 |
(* test for finiteness of domain definitions *) |
542 |
local |
|
40832 | 543 |
val types = [@{type_name ssum}, @{type_name sprod}] |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36241
diff
changeset
|
544 |
fun finite d T = if member (op =) absTs T then d else finite' d T |
35655 | 545 |
and finite' d (Type (c, Ts)) = |
40832 | 546 |
let val d' = d andalso member (op =) types c |
35655 | 547 |
in forall (finite d') Ts end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
548 |
| finite' _ _ = true |
35655 | 549 |
in |
40832 | 550 |
val is_finite = forall (finite true) repTs |
551 |
end |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
552 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
553 |
val ((_, take_induct_thms), thy) = |
35655 | 554 |
if is_finite |
555 |
then |
|
556 |
let |
|
557 |
val ((finites, take_inducts), thy) = |
|
40832 | 558 |
prove_finite_take_induct spec take_info lub_take_thms thy |
35655 | 559 |
in |
560 |
((SOME finites, take_inducts), thy) |
|
561 |
end |
|
562 |
else |
|
563 |
let |
|
564 |
fun prove_take_induct (chain_take, lub_take) = |
|
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
565 |
Drule.zero_var_indexes |
40832 | 566 |
(@{thm lub_ID_take_induct} OF [chain_take, lub_take]) |
35655 | 567 |
val take_inducts = |
40832 | 568 |
map prove_take_induct (chain_take_thms ~~ lub_take_thms) |
35655 | 569 |
val thy = fold (snd oo add_qualified_thm "take_induct") |
40832 | 570 |
(dbinds ~~ take_inducts) thy |
35655 | 571 |
in |
572 |
((NONE, take_inducts), thy) |
|
40832 | 573 |
end |
35655 | 574 |
|
35656 | 575 |
val result = |
576 |
{ |
|
35659 | 577 |
take_consts = #take_consts take_info, |
578 |
take_defs = #take_defs take_info, |
|
579 |
chain_take_thms = #chain_take_thms take_info, |
|
580 |
take_0_thms = #take_0_thms take_info, |
|
581 |
take_Suc_thms = #take_Suc_thms take_info, |
|
582 |
deflation_take_thms = #deflation_take_thms take_info, |
|
40015 | 583 |
take_strict_thms = #take_strict_thms take_info, |
35659 | 584 |
finite_consts = #finite_consts take_info, |
585 |
finite_defs = #finite_defs take_info, |
|
586 |
lub_take_thms = lub_take_thms, |
|
587 |
reach_thms = reach_thms, |
|
588 |
take_lemma_thms = take_lemma_thms, |
|
589 |
is_finite = is_finite, |
|
590 |
take_induct_thms = take_induct_thms |
|
40832 | 591 |
} |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
592 |
in |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
593 |
(result, thy) |
40832 | 594 |
end |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
595 |
|
40832 | 596 |
end |