author | wenzelm |
Tue, 10 Feb 2015 14:48:26 +0100 | |
changeset 59498 | 50b60f501b05 |
parent 57954 | c52223cd1003 |
child 60754 | 02924903a6fd |
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 |
|
40832 | 64 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
65 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
66 |
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
|
67 |
struct |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
68 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
69 |
type iso_info = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
70 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
71 |
absT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
72 |
repT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
73 |
abs_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
74 |
rep_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
75 |
abs_inverse : thm, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
76 |
rep_inverse : thm |
40832 | 77 |
} |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
78 |
|
35651 | 79 |
type take_info = |
80 |
{ take_consts : term list, |
|
81 |
take_defs : thm list, |
|
82 |
chain_take_thms : thm list, |
|
83 |
take_0_thms : thm list, |
|
84 |
take_Suc_thms : thm list, |
|
85 |
deflation_take_thms : thm list, |
|
40015 | 86 |
take_strict_thms : thm list, |
35651 | 87 |
finite_consts : term list, |
88 |
finite_defs : thm list |
|
40832 | 89 |
} |
35651 | 90 |
|
35656 | 91 |
type take_induct_info = |
92 |
{ |
|
35659 | 93 |
take_consts : term list, |
94 |
take_defs : thm list, |
|
95 |
chain_take_thms : thm list, |
|
96 |
take_0_thms : thm list, |
|
97 |
take_Suc_thms : thm list, |
|
98 |
deflation_take_thms : thm list, |
|
40015 | 99 |
take_strict_thms : thm list, |
35659 | 100 |
finite_consts : term list, |
101 |
finite_defs : thm list, |
|
102 |
lub_take_thms : thm list, |
|
103 |
reach_thms : thm list, |
|
104 |
take_lemma_thms : thm list, |
|
105 |
is_finite : bool, |
|
106 |
take_induct_thms : thm list |
|
40832 | 107 |
} |
35656 | 108 |
|
40833
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
109 |
val beta_ss = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
110 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
111 |
addsimps @{thms 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 |
|
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40489
diff
changeset
|
126 |
fun add_rec_type (tname, bs) = |
40832 | 127 |
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
|
128 |
|
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
129 |
fun add_deflation_thm thm = |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56511
diff
changeset
|
130 |
Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
131 |
|
40832 | 132 |
val get_rec_tab = Rec_Data.get |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56511
diff
changeset
|
133 |
fun get_deflation_thms thy = |
57954
c52223cd1003
clarified order of rules for match_tac/resolve_tac;
wenzelm
parents:
57945
diff
changeset
|
134 |
rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}) |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
135 |
|
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56511
diff
changeset
|
136 |
val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID} |
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56511
diff
changeset
|
137 |
fun get_map_ID_thms thy = |
57954
c52223cd1003
clarified order of rules for match_tac/resolve_tac;
wenzelm
parents:
57945
diff
changeset
|
138 |
rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}) |
40489 | 139 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
140 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
141 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
142 |
(************************** building types and terms **************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
143 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
144 |
|
40832 | 145 |
open HOLCF_Library |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
146 |
|
40832 | 147 |
infixr 6 ->> |
148 |
infix -->> |
|
149 |
infix 9 ` |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
150 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
151 |
fun mk_deflation t = |
40832 | 152 |
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
|
153 |
|
40832 | 154 |
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
|
155 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
156 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
157 |
(****************************** isomorphism info ******************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
158 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
159 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
160 |
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
|
161 |
let |
40832 | 162 |
val abs_iso = #abs_inverse info |
163 |
val rep_iso = #rep_inverse info |
|
164 |
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
|
165 |
in |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
166 |
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
|
167 |
end |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
168 |
|
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 |
(********************* building map functions over types **********************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
171 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
172 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
173 |
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
|
174 |
let |
40832 | 175 |
val thms = get_map_ID_thms thy |
176 |
val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) thms |
|
177 |
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
|
178 |
in |
40489 | 179 |
mk_ID T |
180 |
|> Pattern.rewrite_term thy rules' [] |
|
181 |
|> Pattern.rewrite_term thy rules [] |
|
40832 | 182 |
end |
35514
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 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
185 |
(********************* declaring definitions and theorems *********************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
186 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
187 |
|
35773 | 188 |
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
|
189 |
yield_singleton (Global_Theory.add_defs false) |
40832 | 190 |
((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
|
191 |
|
35773 | 192 |
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
|
193 |
yield_singleton Global_Theory.add_thms |
40832 | 194 |
((Binding.qualified true name dbind, thm), []) |
35650 | 195 |
|
35773 | 196 |
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
|
197 |
yield_singleton Global_Theory.add_thms |
40832 | 198 |
((Binding.qualified true name dbind, thm), [Simplifier.simp_add]) |
35573 | 199 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
200 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
201 |
(************************** defining take functions ***************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
202 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
203 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
204 |
fun define_take_functions |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
205 |
(spec : (binding * iso_info) list) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
206 |
(thy : theory) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
207 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
208 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
209 |
(* retrieve components of spec *) |
40832 | 210 |
val dbinds = map fst spec |
211 |
val iso_infos = map snd spec |
|
212 |
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos |
|
213 |
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
|
214 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
215 |
fun mk_projs [] _ = [] |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
216 |
| mk_projs (x::[]) t = [(x, t)] |
40832 | 217 |
| 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
|
218 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
219 |
fun mk_cfcomp2 ((rep_const, abs_const), f) = |
40832 | 220 |
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
|
221 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
222 |
(* define take functional *) |
40832 | 223 |
val newTs : typ list = map fst dom_eqns |
224 |
val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs) |
|
225 |
val copy_arg = Free ("f", copy_arg_type) |
|
226 |
val copy_args = map snd (mk_projs dbinds copy_arg) |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
227 |
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
|
228 |
let |
40832 | 229 |
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
|
230 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
231 |
mk_cfcomp2 (rep_abs, body) |
40832 | 232 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
233 |
val take_functional = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
234 |
big_lambda copy_arg |
40832 | 235 |
(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
|
236 |
val take_rhss = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
237 |
let |
40832 | 238 |
val n = Free ("n", HOLogic.natT) |
239 |
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
|
240 |
in |
35773 | 241 |
map (lambda n o snd) (mk_projs dbinds rhs) |
40832 | 242 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
243 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
244 |
(* define take constants *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
245 |
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
|
246 |
let |
40832 | 247 |
val take_type = HOLogic.natT --> lhsT ->> lhsT |
248 |
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
|
249 |
val (take_const, thy) = |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
250 |
Sign.declare_const_global ((take_bind, take_type), NoSyn) thy |
40832 | 251 |
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
|
252 |
val (take_def_thm, thy) = |
40832 | 253 |
add_qualified_def "take_def" (dbind, take_eqn) thy |
254 |
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
|
255 |
val ((take_consts, take_defs), thy) = thy |
35773 | 256 |
|> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns) |
40832 | 257 |
|>> ListPair.unzip |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
258 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
259 |
(* prove chain_take lemmas *) |
35773 | 260 |
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
|
261 |
let |
40832 | 262 |
val goal = mk_trp (mk_chain take_const) |
263 |
val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd} |
|
54895 | 264 |
fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 |
265 |
val thm = Goal.prove_global thy [] [] goal (tac o #context) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
266 |
in |
35773 | 267 |
add_qualified_simp_thm "chain_take" (dbind, thm) thy |
40832 | 268 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
269 |
val (chain_take_thms, thy) = |
40832 | 270 |
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
|
271 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
272 |
(* prove take_0 lemmas *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
273 |
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
|
274 |
let |
40832 | 275 |
val lhs = take_const $ @{term "0::nat"} |
276 |
val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)) |
|
277 |
val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict} |
|
54895 | 278 |
fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 |
279 |
val take_0_thm = Goal.prove_global thy [] [] goal (tac o #context) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
280 |
in |
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40015
diff
changeset
|
281 |
add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy |
40832 | 282 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
283 |
val (take_0_thms, thy) = |
40832 | 284 |
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
|
285 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
286 |
(* prove take_Suc lemmas *) |
40832 | 287 |
val n = Free ("n", natT) |
288 |
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
|
289 |
fun prove_take_Suc |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
290 |
(((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
|
291 |
let |
40832 | 292 |
val lhs = take_const $ (@{term Suc} $ n) |
293 |
val body = map_of_typ thy (newTs ~~ take_is) rhsT |
|
294 |
val rhs = mk_cfcomp2 (rep_abs, body) |
|
295 |
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
|
296 |
val simps = @{thms iterate_Suc fst_conv snd_conv} |
40832 | 297 |
val rules = take_defs @ simps |
54895 | 298 |
fun tac ctxt = simp_tac (put_simpset beta_ss ctxt addsimps rules) 1 |
299 |
val take_Suc_thm = Goal.prove_global thy [] [] goal (tac o #context) |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
300 |
in |
35773 | 301 |
add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy |
40832 | 302 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
303 |
val (take_Suc_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
304 |
fold_map prove_take_Suc |
40832 | 305 |
(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
|
306 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
307 |
(* prove deflation theorems for take functions *) |
40832 | 308 |
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
|
309 |
val deflation_take_thm = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
310 |
let |
40832 | 311 |
val n = Free ("n", natT) |
312 |
fun mk_goal take_const = mk_deflation (take_const $ n) |
|
313 |
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
|
314 |
val bottom_rules = |
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40833
diff
changeset
|
315 |
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
|
316 |
val deflation_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
317 |
@{thms conjI deflation_ID} |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
318 |
@ deflation_abs_rep_thms |
40832 | 319 |
@ get_deflation_thms thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
320 |
in |
54895 | 321 |
Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} => |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
322 |
EVERY |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
323 |
[rtac @{thm nat.induct} 1, |
54895 | 324 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, |
325 |
asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1, |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
326 |
REPEAT (etac @{thm conjE} 1 |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
57954
diff
changeset
|
327 |
ORELSE resolve_tac ctxt deflation_rules 1 |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
328 |
ORELSE atac 1)]) |
40832 | 329 |
end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
330 |
fun conjuncts [] _ = [] |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
331 |
| conjuncts (n::[]) thm = [(n, thm)] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
332 |
| conjuncts (n::ns) thm = let |
40832 | 333 |
val thmL = thm RS @{thm conjunct1} |
334 |
val thmR = thm RS @{thm conjunct2} |
|
335 |
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
|
336 |
val (deflation_take_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
337 |
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
|
338 |
(map (apsnd Drule.zero_var_indexes) |
40832 | 339 |
(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
|
340 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
341 |
(* prove strictness of take functions *) |
35773 | 342 |
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
|
343 |
let |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
344 |
val take_strict_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
345 |
Drule.zero_var_indexes |
40832 | 346 |
(@{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
|
347 |
in |
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40015
diff
changeset
|
348 |
add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy |
40832 | 349 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
350 |
val (take_strict_thms, thy) = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
351 |
fold_map prove_take_strict |
40832 | 352 |
(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
|
353 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
354 |
(* prove take/take rules *) |
35773 | 355 |
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
|
356 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
357 |
val take_take_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
358 |
Drule.zero_var_indexes |
40832 | 359 |
(@{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
|
360 |
in |
35773 | 361 |
add_qualified_thm "take_take" (dbind, take_take_thm) thy |
40832 | 362 |
end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
363 |
val (_, thy) = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
364 |
fold_map prove_take_take |
40832 | 365 |
(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
|
366 |
|
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
367 |
(* prove take_below rules *) |
35773 | 368 |
fun prove_take_below (deflation_take, dbind) thy = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
369 |
let |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
370 |
val take_below_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
371 |
Drule.zero_var_indexes |
40832 | 372 |
(@{thm deflation.below} OF [deflation_take]) |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
373 |
in |
35773 | 374 |
add_qualified_thm "take_below" (dbind, take_below_thm) thy |
40832 | 375 |
end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
376 |
val (_, thy) = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
377 |
fold_map prove_take_below |
40832 | 378 |
(deflation_take_thms ~~ dbinds) thy |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
379 |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
380 |
(* define finiteness predicates *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
381 |
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
|
382 |
let |
40832 | 383 |
val finite_type = lhsT --> boolT |
384 |
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
|
385 |
val (finite_const, thy) = |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
386 |
Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy |
40832 | 387 |
val x = Free ("x", lhsT) |
388 |
val n = Free ("n", natT) |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
389 |
val finite_rhs = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
390 |
lambda x (HOLogic.exists_const natT $ |
40832 | 391 |
(lambda n (mk_eq (mk_capply (take_const $ n, x), x)))) |
392 |
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
|
393 |
val (finite_def_thm, thy) = |
40832 | 394 |
add_qualified_def "finite_def" (dbind, finite_eqn) thy |
395 |
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
|
396 |
val ((finite_consts, finite_defs), thy) = thy |
35773 | 397 |
|> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns) |
40832 | 398 |
|>> ListPair.unzip |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
399 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
400 |
val result = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
401 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
402 |
take_consts = take_consts, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
403 |
take_defs = take_defs, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
take_Suc_thms = take_Suc_thms, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
407 |
deflation_take_thms = deflation_take_thms, |
40015 | 408 |
take_strict_thms = take_strict_thms, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
409 |
finite_consts = finite_consts, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
410 |
finite_defs = finite_defs |
40832 | 411 |
} |
35514
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 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
414 |
(result, thy) |
40832 | 415 |
end |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
416 |
|
35655 | 417 |
fun prove_finite_take_induct |
418 |
(spec : (binding * iso_info) list) |
|
419 |
(take_info : take_info) |
|
420 |
(lub_take_thms : thm list) |
|
421 |
(thy : theory) = |
|
422 |
let |
|
40832 | 423 |
val dbinds = map fst spec |
424 |
val iso_infos = map snd spec |
|
425 |
val absTs = map #absT iso_infos |
|
426 |
val {take_consts, ...} = take_info |
|
427 |
val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info |
|
428 |
val {finite_consts, finite_defs, ...} = take_info |
|
35655 | 429 |
|
430 |
val decisive_lemma = |
|
431 |
let |
|
37165 | 432 |
fun iso_locale (info : iso_info) = |
40832 | 433 |
@{thm iso.intro} OF [#abs_inverse info, #rep_inverse info] |
434 |
val iso_locale_thms = map iso_locale iso_infos |
|
35655 | 435 |
val decisive_abs_rep_thms = |
40832 | 436 |
map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms |
437 |
val n = Free ("n", @{typ nat}) |
|
35655 | 438 |
fun mk_decisive t = |
40832 | 439 |
Const (@{const_name decisive}, fastype_of t --> boolT) $ t |
440 |
fun f take_const = mk_decisive (take_const $ n) |
|
441 |
val goal = mk_trp (foldr1 mk_conj (map f take_consts)) |
|
442 |
val rules0 = @{thm decisive_bottom} :: take_0_thms |
|
35655 | 443 |
val rules1 = |
444 |
take_Suc_thms @ decisive_abs_rep_thms |
|
40832 | 445 |
@ @{thms decisive_ID decisive_ssum_map decisive_sprod_map} |
54895 | 446 |
fun tac ctxt = EVERY [ |
35655 | 447 |
rtac @{thm nat.induct} 1, |
54895 | 448 |
simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1, |
449 |
asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1] |
|
450 |
in Goal.prove_global thy [] [] goal (tac o #context) end |
|
35655 | 451 |
fun conjuncts 1 thm = [thm] |
452 |
| conjuncts n thm = let |
|
40832 | 453 |
val thmL = thm RS @{thm conjunct1} |
454 |
val thmR = thm RS @{thm conjunct2} |
|
455 |
in thmL :: conjuncts (n-1) thmR end |
|
456 |
val decisive_thms = conjuncts (length spec) decisive_lemma |
|
35655 | 457 |
|
458 |
fun prove_finite_thm (absT, finite_const) = |
|
459 |
let |
|
40832 | 460 |
val goal = mk_trp (finite_const $ Free ("x", absT)) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
461 |
fun tac ctxt = |
35655 | 462 |
EVERY [ |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
463 |
rewrite_goals_tac ctxt finite_defs, |
35655 | 464 |
rtac @{thm lub_ID_finite} 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
57954
diff
changeset
|
465 |
resolve_tac ctxt chain_take_thms 1, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
57954
diff
changeset
|
466 |
resolve_tac ctxt lub_take_thms 1, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
57954
diff
changeset
|
467 |
resolve_tac ctxt decisive_thms 1] |
35655 | 468 |
in |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
469 |
Goal.prove_global thy [] [] goal (tac o #context) |
40832 | 470 |
end |
35655 | 471 |
val finite_thms = |
40832 | 472 |
map prove_finite_thm (absTs ~~ finite_consts) |
35655 | 473 |
|
474 |
fun prove_take_induct ((ch_take, lub_take), decisive) = |
|
475 |
Drule.export_without_context |
|
40832 | 476 |
(@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]) |
35655 | 477 |
val take_induct_thms = |
478 |
map prove_take_induct |
|
40832 | 479 |
(chain_take_thms ~~ lub_take_thms ~~ decisive_thms) |
35655 | 480 |
|
481 |
val thy = thy |
|
482 |
|> fold (snd oo add_qualified_thm "finite") |
|
35773 | 483 |
(dbinds ~~ finite_thms) |
35655 | 484 |
|> fold (snd oo add_qualified_thm "take_induct") |
40832 | 485 |
(dbinds ~~ take_induct_thms) |
35655 | 486 |
in |
487 |
((finite_thms, take_induct_thms), thy) |
|
40832 | 488 |
end |
35655 | 489 |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
490 |
fun add_lub_take_theorems |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
491 |
(spec : (binding * iso_info) list) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
492 |
(take_info : take_info) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
493 |
(lub_take_thms : thm list) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
494 |
(thy : theory) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
495 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
496 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
497 |
(* retrieve components of spec *) |
40832 | 498 |
val dbinds = map fst spec |
499 |
val iso_infos = map snd spec |
|
500 |
val absTs = map #absT iso_infos |
|
501 |
val repTs = map #repT iso_infos |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
502 |
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
|
503 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
504 |
(* prove take lemmas *) |
35773 | 505 |
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
|
506 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
507 |
val take_lemma = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
508 |
Drule.export_without_context |
40832 | 509 |
(@{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
|
510 |
in |
35773 | 511 |
add_qualified_thm "take_lemma" (dbind, take_lemma) thy |
40832 | 512 |
end |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
513 |
val (take_lemma_thms, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
514 |
fold_map prove_take_lemma |
40832 | 515 |
(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
|
516 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
517 |
(* prove reach lemmas *) |
35773 | 518 |
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
|
519 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
520 |
val thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
521 |
Drule.zero_var_indexes |
40832 | 522 |
(@{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
|
523 |
in |
35773 | 524 |
add_qualified_thm "reach" (dbind, thm) thy |
40832 | 525 |
end |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
526 |
val (reach_thms, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
527 |
fold_map prove_reach_lemma |
40832 | 528 |
(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
|
529 |
|
35655 | 530 |
(* test for finiteness of domain definitions *) |
531 |
local |
|
40832 | 532 |
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
|
533 |
fun finite d T = if member (op =) absTs T then d else finite' d T |
35655 | 534 |
and finite' d (Type (c, Ts)) = |
40832 | 535 |
let val d' = d andalso member (op =) types c |
35655 | 536 |
in forall (finite d') Ts end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
537 |
| finite' _ _ = true |
35655 | 538 |
in |
40832 | 539 |
val is_finite = forall (finite true) repTs |
540 |
end |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
541 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42375
diff
changeset
|
542 |
val ((_, take_induct_thms), thy) = |
35655 | 543 |
if is_finite |
544 |
then |
|
545 |
let |
|
546 |
val ((finites, take_inducts), thy) = |
|
40832 | 547 |
prove_finite_take_induct spec take_info lub_take_thms thy |
35655 | 548 |
in |
549 |
((SOME finites, take_inducts), thy) |
|
550 |
end |
|
551 |
else |
|
552 |
let |
|
553 |
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
|
554 |
Drule.zero_var_indexes |
40832 | 555 |
(@{thm lub_ID_take_induct} OF [chain_take, lub_take]) |
35655 | 556 |
val take_inducts = |
40832 | 557 |
map prove_take_induct (chain_take_thms ~~ lub_take_thms) |
35655 | 558 |
val thy = fold (snd oo add_qualified_thm "take_induct") |
40832 | 559 |
(dbinds ~~ take_inducts) thy |
35655 | 560 |
in |
561 |
((NONE, take_inducts), thy) |
|
40832 | 562 |
end |
35655 | 563 |
|
35656 | 564 |
val result = |
565 |
{ |
|
35659 | 566 |
take_consts = #take_consts take_info, |
567 |
take_defs = #take_defs take_info, |
|
568 |
chain_take_thms = #chain_take_thms take_info, |
|
569 |
take_0_thms = #take_0_thms take_info, |
|
570 |
take_Suc_thms = #take_Suc_thms take_info, |
|
571 |
deflation_take_thms = #deflation_take_thms take_info, |
|
40015 | 572 |
take_strict_thms = #take_strict_thms take_info, |
35659 | 573 |
finite_consts = #finite_consts take_info, |
574 |
finite_defs = #finite_defs take_info, |
|
575 |
lub_take_thms = lub_take_thms, |
|
576 |
reach_thms = reach_thms, |
|
577 |
take_lemma_thms = take_lemma_thms, |
|
578 |
is_finite = is_finite, |
|
579 |
take_induct_thms = take_induct_thms |
|
40832 | 580 |
} |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
581 |
in |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
582 |
(result, thy) |
40832 | 583 |
end |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
584 |
|
40832 | 585 |
end |