author | huffman |
Fri, 29 Oct 2010 16:51:40 -0700 | |
changeset 40326 | 73d45866dbda |
parent 40218 | f7d4d023a899 |
child 40489 | 0f37a553bc1a |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: 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 |
|
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
58 |
val add_map_function : (string * string * bool list) -> theory -> theory |
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
59 |
val get_map_tab : theory -> (string * 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 |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
62 |
val setup : theory -> theory |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
63 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
64 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
65 |
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
|
66 |
struct |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
67 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
68 |
type iso_info = |
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 |
absT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
71 |
repT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
72 |
abs_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
73 |
rep_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
74 |
abs_inverse : thm, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
75 |
rep_inverse : thm |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
76 |
}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
77 |
|
35651 | 78 |
type take_info = |
79 |
{ take_consts : term list, |
|
80 |
take_defs : thm list, |
|
81 |
chain_take_thms : thm list, |
|
82 |
take_0_thms : thm list, |
|
83 |
take_Suc_thms : thm list, |
|
84 |
deflation_take_thms : thm list, |
|
40015 | 85 |
take_strict_thms : thm list, |
35651 | 86 |
finite_consts : term list, |
87 |
finite_defs : thm list |
|
88 |
}; |
|
89 |
||
35656 | 90 |
type take_induct_info = |
91 |
{ |
|
35659 | 92 |
take_consts : term list, |
93 |
take_defs : thm list, |
|
94 |
chain_take_thms : thm list, |
|
95 |
take_0_thms : thm list, |
|
96 |
take_Suc_thms : thm list, |
|
97 |
deflation_take_thms : thm list, |
|
40015 | 98 |
take_strict_thms : thm list, |
35659 | 99 |
finite_consts : term list, |
100 |
finite_defs : thm list, |
|
101 |
lub_take_thms : thm list, |
|
102 |
reach_thms : thm list, |
|
103 |
take_lemma_thms : thm list, |
|
104 |
is_finite : bool, |
|
105 |
take_induct_thms : thm list |
|
35656 | 106 |
}; |
107 |
||
37078
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36692
diff
changeset
|
108 |
val beta_rules = |
40326
73d45866dbda
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman
parents:
40218
diff
changeset
|
109 |
@{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ |
37078
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36692
diff
changeset
|
110 |
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; |
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36692
diff
changeset
|
111 |
|
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36692
diff
changeset
|
112 |
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); |
35514
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 |
val beta_tac = simp_tac beta_ss; |
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 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
117 |
(******************************** theory data *********************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
118 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
119 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
120 |
structure MapData = Theory_Data |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
121 |
( |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
122 |
(* constant names like "foo_map" *) |
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
123 |
(* list indicates which type arguments correspond to map arguments *) |
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
124 |
(* alternatively, which type arguments allow indirect recursion *) |
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
125 |
type T = (string * bool list) Symtab.table; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
126 |
val empty = Symtab.empty; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
127 |
val extend = I; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
128 |
fun merge data = Symtab.merge (K true) data; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
129 |
); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
130 |
|
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
131 |
structure DeflMapData = Named_Thms |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
132 |
( |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
133 |
val name = "domain_deflation" |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
134 |
val description = "theorems like deflation a ==> deflation (foo_map$a)" |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
135 |
); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
136 |
|
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
137 |
fun add_map_function (tname, map_name, bs) = |
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
138 |
MapData.map (Symtab.insert (K true) (tname, (map_name, bs))); |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
139 |
|
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
140 |
fun add_deflation_thm thm = |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
141 |
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
|
142 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
143 |
val get_map_tab = MapData.get; |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
144 |
fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy); |
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
145 |
|
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
146 |
val setup = DeflMapData.setup; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
147 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
148 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
149 |
(************************** building types and terms **************************) |
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 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
152 |
open HOLCF_Library; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
153 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
154 |
infixr 6 ->>; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
155 |
infix -->>; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
156 |
infix 9 `; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
157 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
158 |
fun mapT (T as Type (_, Ts)) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
159 |
(map (fn T => T ->> T) Ts) -->> (T ->> T) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
160 |
| mapT T = T ->> T; |
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 = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
163 |
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
164 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
165 |
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); |
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 |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
173 |
val abs_iso = #abs_inverse info; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
174 |
val rep_iso = #rep_inverse info; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
175 |
val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; |
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 |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
186 |
val map_tab = get_map_tab thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
187 |
fun auto T = T ->> T; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
188 |
fun map_of T = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
189 |
case AList.lookup (op =) sub T of |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
190 |
SOME m => (m, true) | NONE => map_of' T |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
191 |
and map_of' (T as (Type (c, Ts))) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
192 |
(case Symtab.lookup map_tab c of |
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
193 |
SOME (map_name, ds) => |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
194 |
let |
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
195 |
val Ts' = map snd (filter fst (ds ~~ Ts)); |
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
196 |
val map_type = map auto Ts' -->> auto T; |
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
197 |
val (ms, bs) = map_split map_of Ts'; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
198 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
199 |
if exists I bs |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
200 |
then (list_ccomb (Const (map_name, map_type), ms), true) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
201 |
else (mk_ID T, false) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
202 |
end |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
203 |
| NONE => (mk_ID T, false)) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
204 |
| map_of' T = (mk_ID T, false); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
205 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
206 |
fst (map_of T) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
207 |
end; |
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 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
210 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
211 |
(********************* declaring definitions and theorems *********************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
212 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
213 |
|
35773 | 214 |
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
|
215 |
yield_singleton (Global_Theory.add_defs false) |
35773 | 216 |
((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
|
217 |
|
35773 | 218 |
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
|
219 |
yield_singleton Global_Theory.add_thms |
35773 | 220 |
((Binding.qualified true name dbind, thm), []); |
35650 | 221 |
|
35773 | 222 |
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
|
223 |
yield_singleton Global_Theory.add_thms |
35773 | 224 |
((Binding.qualified true name dbind, thm), [Simplifier.simp_add]); |
35573 | 225 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
226 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
227 |
(************************** defining take functions ***************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
228 |
(******************************************************************************) |
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 define_take_functions |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
231 |
(spec : (binding * iso_info) list) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
232 |
(thy : theory) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
233 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
234 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
235 |
(* retrieve components of spec *) |
35773 | 236 |
val dbinds = map fst spec; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
237 |
val iso_infos = map snd spec; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
238 |
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
239 |
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
240 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
241 |
fun mk_projs [] t = [] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
242 |
| mk_projs (x::[]) t = [(x, t)] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
243 |
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
244 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
245 |
fun mk_cfcomp2 ((rep_const, abs_const), f) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
246 |
mk_cfcomp (abs_const, mk_cfcomp (f, rep_const)); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
247 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
248 |
(* define take functional *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
249 |
val newTs : typ list = map fst dom_eqns; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
250 |
val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
251 |
val copy_arg = Free ("f", copy_arg_type); |
35773 | 252 |
val copy_args = map snd (mk_projs dbinds copy_arg); |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
253 |
fun one_copy_rhs (rep_abs, (lhsT, rhsT)) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
254 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
255 |
val body = map_of_typ thy (newTs ~~ copy_args) rhsT; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
256 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
257 |
mk_cfcomp2 (rep_abs, body) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
258 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
259 |
val take_functional = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
260 |
big_lambda copy_arg |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
261 |
(mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns))); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
262 |
val take_rhss = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
263 |
let |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
264 |
val n = Free ("n", HOLogic.natT); |
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
265 |
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
|
266 |
in |
35773 | 267 |
map (lambda n o snd) (mk_projs dbinds rhs) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
268 |
end; |
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 |
(* define take constants *) |
35773 | 271 |
fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
272 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
273 |
val take_type = HOLogic.natT --> lhsT ->> lhsT; |
35773 | 274 |
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
|
275 |
val (take_const, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
276 |
Sign.declare_const ((take_bind, take_type), NoSyn) thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
277 |
val take_eqn = Logic.mk_equals (take_const, take_rhs); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
278 |
val (take_def_thm, thy) = |
35773 | 279 |
add_qualified_def "take_def" (dbind, take_eqn) thy; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
280 |
in ((take_const, take_def_thm), thy) end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
281 |
val ((take_consts, take_defs), thy) = thy |
35773 | 282 |
|> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
283 |
|>> ListPair.unzip; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
284 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
285 |
(* prove chain_take lemmas *) |
35773 | 286 |
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
|
287 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
288 |
val goal = mk_trp (mk_chain take_const); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
289 |
val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
290 |
val tac = simp_tac (HOL_basic_ss addsimps rules) 1; |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
291 |
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
|
292 |
in |
35773 | 293 |
add_qualified_simp_thm "chain_take" (dbind, thm) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
294 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
295 |
val (chain_take_thms, thy) = |
35773 | 296 |
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
|
297 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
298 |
(* prove take_0 lemmas *) |
35773 | 299 |
fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
300 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
301 |
val lhs = take_const $ @{term "0::nat"}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
302 |
val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
303 |
val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
304 |
val tac = simp_tac (HOL_basic_ss addsimps rules) 1; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
305 |
val take_0_thm = Goal.prove_global thy [] [] goal (K tac); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
306 |
in |
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40015
diff
changeset
|
307 |
add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
308 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
309 |
val (take_0_thms, thy) = |
35773 | 310 |
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
|
311 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
312 |
(* prove take_Suc lemmas *) |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
313 |
val n = Free ("n", natT); |
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
314 |
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
|
315 |
fun prove_take_Suc |
35773 | 316 |
(((take_const, rep_abs), dbind), (lhsT, rhsT)) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
317 |
let |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
318 |
val lhs = take_const $ (@{term Suc} $ n); |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
319 |
val body = map_of_typ thy (newTs ~~ take_is) rhsT; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
320 |
val rhs = mk_cfcomp2 (rep_abs, body); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
321 |
val goal = mk_eqs (lhs, rhs); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
322 |
val simps = @{thms iterate_Suc fst_conv snd_conv} |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
323 |
val rules = take_defs @ simps; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
324 |
val tac = simp_tac (beta_ss addsimps rules) 1; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
325 |
val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
326 |
in |
35773 | 327 |
add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
328 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
329 |
val (take_Suc_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
330 |
fold_map prove_take_Suc |
35773 | 331 |
(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
|
332 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
333 |
(* prove deflation theorems for take functions *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
334 |
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
335 |
val deflation_take_thm = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
336 |
let |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
337 |
val n = Free ("n", natT); |
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
338 |
fun mk_goal take_const = mk_deflation (take_const $ n); |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
339 |
val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts)); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
340 |
val adm_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
341 |
@{thms adm_conj adm_subst [OF _ adm_deflation] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
342 |
cont2cont_fst cont2cont_snd cont_id}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
343 |
val bottom_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
344 |
take_0_thms @ @{thms deflation_UU simp_thms}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
345 |
val deflation_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
346 |
@{thms conjI deflation_ID} |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
347 |
@ deflation_abs_rep_thms |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40016
diff
changeset
|
348 |
@ get_deflation_thms thy; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
349 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
350 |
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
|
351 |
EVERY |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
352 |
[rtac @{thm nat.induct} 1, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
353 |
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
|
354 |
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
|
355 |
REPEAT (etac @{thm conjE} 1 |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
356 |
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
|
357 |
ORELSE atac 1)]) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
358 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
359 |
fun conjuncts [] thm = [] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
360 |
| conjuncts (n::[]) thm = [(n, thm)] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
361 |
| conjuncts (n::ns) thm = let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
362 |
val thmL = thm RS @{thm conjunct1}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
363 |
val thmR = thm RS @{thm conjunct2}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
364 |
in (n, thmL):: conjuncts ns thmR end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
365 |
val (deflation_take_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
366 |
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
|
367 |
(map (apsnd Drule.zero_var_indexes) |
35773 | 368 |
(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
|
369 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
370 |
(* prove strictness of take functions *) |
35773 | 371 |
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
|
372 |
let |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
373 |
val take_strict_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
374 |
Drule.zero_var_indexes |
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
375 |
(@{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
|
376 |
in |
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40015
diff
changeset
|
377 |
add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
378 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
379 |
val (take_strict_thms, thy) = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
380 |
fold_map prove_take_strict |
35773 | 381 |
(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
|
382 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
383 |
(* prove take/take rules *) |
35773 | 384 |
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
|
385 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
386 |
val take_take_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
387 |
Drule.zero_var_indexes |
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
388 |
(@{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
|
389 |
in |
35773 | 390 |
add_qualified_thm "take_take" (dbind, take_take_thm) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
391 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
392 |
val (take_take_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
393 |
fold_map prove_take_take |
35773 | 394 |
(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
|
395 |
|
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
396 |
(* prove take_below rules *) |
35773 | 397 |
fun prove_take_below (deflation_take, dbind) thy = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
398 |
let |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
399 |
val take_below_thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
400 |
Drule.zero_var_indexes |
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
401 |
(@{thm deflation.below} OF [deflation_take]); |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
402 |
in |
35773 | 403 |
add_qualified_thm "take_below" (dbind, take_below_thm) thy |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
404 |
end; |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
405 |
val (take_below_thms, thy) = |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
406 |
fold_map prove_take_below |
35773 | 407 |
(deflation_take_thms ~~ dbinds) thy; |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
408 |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
409 |
(* define finiteness predicates *) |
35773 | 410 |
fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy = |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
411 |
let |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
412 |
val finite_type = lhsT --> boolT; |
35773 | 413 |
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
|
414 |
val (finite_const, thy) = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
415 |
Sign.declare_const ((finite_bind, finite_type), NoSyn) thy; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
416 |
val x = Free ("x", lhsT); |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
417 |
val n = Free ("n", natT); |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
418 |
val finite_rhs = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
419 |
lambda x (HOLogic.exists_const natT $ |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
420 |
(lambda n (mk_eq (mk_capply (take_const $ n, x), x)))); |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
421 |
val finite_eqn = Logic.mk_equals (finite_const, finite_rhs); |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
422 |
val (finite_def_thm, thy) = |
35773 | 423 |
add_qualified_def "finite_def" (dbind, finite_eqn) thy; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
424 |
in ((finite_const, finite_def_thm), thy) end; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
425 |
val ((finite_consts, finite_defs), thy) = thy |
35773 | 426 |
|> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns) |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
427 |
|>> ListPair.unzip; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
428 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
429 |
val result = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
430 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
431 |
take_consts = take_consts, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
432 |
take_defs = take_defs, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
433 |
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
|
434 |
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
|
435 |
take_Suc_thms = take_Suc_thms, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
436 |
deflation_take_thms = deflation_take_thms, |
40015 | 437 |
take_strict_thms = take_strict_thms, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
438 |
finite_consts = finite_consts, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
439 |
finite_defs = finite_defs |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
440 |
}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
441 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
442 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
443 |
(result, thy) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
444 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
445 |
|
35655 | 446 |
fun prove_finite_take_induct |
447 |
(spec : (binding * iso_info) list) |
|
448 |
(take_info : take_info) |
|
449 |
(lub_take_thms : thm list) |
|
450 |
(thy : theory) = |
|
451 |
let |
|
35773 | 452 |
val dbinds = map fst spec; |
35655 | 453 |
val iso_infos = map snd spec; |
454 |
val absTs = map #absT iso_infos; |
|
455 |
val {take_consts, ...} = take_info; |
|
456 |
val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info; |
|
457 |
val {finite_consts, finite_defs, ...} = take_info; |
|
458 |
||
459 |
val decisive_lemma = |
|
460 |
let |
|
37165 | 461 |
fun iso_locale (info : iso_info) = |
35655 | 462 |
@{thm iso.intro} OF [#abs_inverse info, #rep_inverse info]; |
463 |
val iso_locale_thms = map iso_locale iso_infos; |
|
464 |
val decisive_abs_rep_thms = |
|
465 |
map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms; |
|
466 |
val n = Free ("n", @{typ nat}); |
|
467 |
fun mk_decisive t = |
|
468 |
Const (@{const_name decisive}, fastype_of t --> boolT) $ t; |
|
469 |
fun f take_const = mk_decisive (take_const $ n); |
|
470 |
val goal = mk_trp (foldr1 mk_conj (map f take_consts)); |
|
471 |
val rules0 = @{thm decisive_bottom} :: take_0_thms; |
|
472 |
val rules1 = |
|
473 |
take_Suc_thms @ decisive_abs_rep_thms |
|
474 |
@ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}; |
|
475 |
val tac = EVERY [ |
|
476 |
rtac @{thm nat.induct} 1, |
|
477 |
simp_tac (HOL_ss addsimps rules0) 1, |
|
478 |
asm_simp_tac (HOL_ss addsimps rules1) 1]; |
|
479 |
in Goal.prove_global thy [] [] goal (K tac) end; |
|
480 |
fun conjuncts 1 thm = [thm] |
|
481 |
| conjuncts n thm = let |
|
482 |
val thmL = thm RS @{thm conjunct1}; |
|
483 |
val thmR = thm RS @{thm conjunct2}; |
|
484 |
in thmL :: conjuncts (n-1) thmR end; |
|
485 |
val decisive_thms = conjuncts (length spec) decisive_lemma; |
|
486 |
||
487 |
fun prove_finite_thm (absT, finite_const) = |
|
488 |
let |
|
489 |
val goal = mk_trp (finite_const $ Free ("x", absT)); |
|
490 |
val tac = |
|
491 |
EVERY [ |
|
492 |
rewrite_goals_tac finite_defs, |
|
493 |
rtac @{thm lub_ID_finite} 1, |
|
494 |
resolve_tac chain_take_thms 1, |
|
495 |
resolve_tac lub_take_thms 1, |
|
496 |
resolve_tac decisive_thms 1]; |
|
497 |
in |
|
498 |
Goal.prove_global thy [] [] goal (K tac) |
|
499 |
end; |
|
500 |
val finite_thms = |
|
501 |
map prove_finite_thm (absTs ~~ finite_consts); |
|
502 |
||
503 |
fun prove_take_induct ((ch_take, lub_take), decisive) = |
|
504 |
Drule.export_without_context |
|
505 |
(@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]); |
|
506 |
val take_induct_thms = |
|
507 |
map prove_take_induct |
|
508 |
(chain_take_thms ~~ lub_take_thms ~~ decisive_thms); |
|
509 |
||
510 |
val thy = thy |
|
511 |
|> fold (snd oo add_qualified_thm "finite") |
|
35773 | 512 |
(dbinds ~~ finite_thms) |
35655 | 513 |
|> fold (snd oo add_qualified_thm "take_induct") |
35773 | 514 |
(dbinds ~~ take_induct_thms); |
35655 | 515 |
in |
516 |
((finite_thms, take_induct_thms), thy) |
|
517 |
end; |
|
518 |
||
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
519 |
fun add_lub_take_theorems |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
520 |
(spec : (binding * iso_info) list) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
521 |
(take_info : take_info) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
522 |
(lub_take_thms : thm list) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
523 |
(thy : theory) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
524 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
525 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
526 |
(* retrieve components of spec *) |
35773 | 527 |
val dbinds = map fst spec; |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
528 |
val iso_infos = map snd spec; |
35655 | 529 |
val absTs = map #absT iso_infos; |
530 |
val repTs = map #repT iso_infos; |
|
531 |
val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info; |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
532 |
val {chain_take_thms, deflation_take_thms, ...} = take_info; |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
533 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
534 |
(* prove take lemmas *) |
35773 | 535 |
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
|
536 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
537 |
val take_lemma = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
538 |
Drule.export_without_context |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
539 |
(@{thm lub_ID_take_lemma} OF [chain_take, lub_take]); |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
540 |
in |
35773 | 541 |
add_qualified_thm "take_lemma" (dbind, take_lemma) thy |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
542 |
end; |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
543 |
val (take_lemma_thms, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
544 |
fold_map prove_take_lemma |
35773 | 545 |
(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
|
546 |
|
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
547 |
(* prove reach lemmas *) |
35773 | 548 |
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
|
549 |
let |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
550 |
val thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35773
diff
changeset
|
551 |
Drule.zero_var_indexes |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
552 |
(@{thm lub_ID_reach} OF [chain_take, lub_take]); |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
553 |
in |
35773 | 554 |
add_qualified_thm "reach" (dbind, thm) thy |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
555 |
end; |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
556 |
val (reach_thms, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
557 |
fold_map prove_reach_lemma |
35773 | 558 |
(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
|
559 |
|
35655 | 560 |
(* test for finiteness of domain definitions *) |
561 |
local |
|
562 |
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
|
563 |
fun finite d T = if member (op =) absTs T then d else finite' d T |
35655 | 564 |
and finite' d (Type (c, Ts)) = |
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
|
565 |
let val d' = d andalso member (op =) types c; |
35655 | 566 |
in forall (finite d') Ts end |
567 |
| finite' d _ = true; |
|
568 |
in |
|
569 |
val is_finite = forall (finite true) repTs; |
|
570 |
end; |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
571 |
|
35655 | 572 |
val ((finite_thms, take_induct_thms), thy) = |
573 |
if is_finite |
|
574 |
then |
|
575 |
let |
|
576 |
val ((finites, take_inducts), thy) = |
|
577 |
prove_finite_take_induct spec take_info lub_take_thms thy; |
|
578 |
in |
|
579 |
((SOME finites, take_inducts), thy) |
|
580 |
end |
|
581 |
else |
|
582 |
let |
|
583 |
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
|
584 |
Drule.zero_var_indexes |
35655 | 585 |
(@{thm lub_ID_take_induct} OF [chain_take, lub_take]); |
586 |
val take_inducts = |
|
587 |
map prove_take_induct (chain_take_thms ~~ lub_take_thms); |
|
588 |
val thy = fold (snd oo add_qualified_thm "take_induct") |
|
35773 | 589 |
(dbinds ~~ take_inducts) thy; |
35655 | 590 |
in |
591 |
((NONE, take_inducts), thy) |
|
592 |
end; |
|
593 |
||
35656 | 594 |
val result = |
595 |
{ |
|
35659 | 596 |
take_consts = #take_consts take_info, |
597 |
take_defs = #take_defs take_info, |
|
598 |
chain_take_thms = #chain_take_thms take_info, |
|
599 |
take_0_thms = #take_0_thms take_info, |
|
600 |
take_Suc_thms = #take_Suc_thms take_info, |
|
601 |
deflation_take_thms = #deflation_take_thms take_info, |
|
40015 | 602 |
take_strict_thms = #take_strict_thms take_info, |
35659 | 603 |
finite_consts = #finite_consts take_info, |
604 |
finite_defs = #finite_defs take_info, |
|
605 |
lub_take_thms = lub_take_thms, |
|
606 |
reach_thms = reach_thms, |
|
607 |
take_lemma_thms = take_lemma_thms, |
|
608 |
is_finite = is_finite, |
|
609 |
take_induct_thms = take_induct_thms |
|
35656 | 610 |
}; |
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
611 |
in |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
612 |
(result, thy) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
613 |
end; |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35651
diff
changeset
|
614 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
615 |
end; |