author | huffman |
Fri, 05 Mar 2010 13:55:36 -0800 | |
changeset 35594 | 47d68e33ca29 |
parent 35573 | bd8b50e76e94 |
child 35650 | 64fff18d7f08 |
permissions | -rw-r--r-- |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
1 |
(* Title: HOLCF/Tools/domain/domain_take_proofs.ML |
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 |
} |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
19 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
20 |
val define_take_functions : |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
21 |
(binding * iso_info) list -> theory -> |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
22 |
{ take_consts : term list, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
23 |
take_defs : thm list, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
24 |
chain_take_thms : thm list, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
25 |
take_0_thms : thm list, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
26 |
take_Suc_thms : thm list, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
27 |
deflation_take_thms : thm list, |
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 |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
30 |
} * theory |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
31 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
32 |
val map_of_typ : |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
33 |
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
|
34 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
35 |
val add_map_function : |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
36 |
(string * string * thm) -> theory -> theory |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
37 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
38 |
val get_map_tab : theory -> string Symtab.table |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
39 |
val get_deflation_thms : theory -> thm list |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
40 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
41 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
42 |
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
|
43 |
struct |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
44 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
45 |
type iso_info = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
46 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
47 |
absT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
48 |
repT : typ, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
49 |
abs_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
50 |
rep_const : term, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
51 |
abs_inverse : thm, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
52 |
rep_inverse : thm |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
53 |
}; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
54 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
55 |
val beta_ss = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
56 |
HOL_basic_ss |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
57 |
addsimps simp_thms |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
58 |
addsimps [@{thm beta_cfun}] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
59 |
addsimprocs [@{simproc cont_proc}]; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
60 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
61 |
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
|
62 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
63 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
64 |
(******************************** theory data *********************************) |
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 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
67 |
structure MapData = Theory_Data |
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 |
(* constant names like "foo_map" *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
70 |
type T = string Symtab.table; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
71 |
val empty = Symtab.empty; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
72 |
val extend = I; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
73 |
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
|
74 |
); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
75 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
76 |
structure DeflMapData = Theory_Data |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
77 |
( |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
78 |
(* theorems like "deflation a ==> deflation (foo_map$a)" *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
79 |
type T = thm list; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
80 |
val empty = []; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
81 |
val extend = I; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
82 |
val merge = Thm.merge_thms; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
83 |
); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
84 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
85 |
fun add_map_function (tname, map_name, deflation_map_thm) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
86 |
MapData.map (Symtab.insert (K true) (tname, map_name)) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
87 |
#> DeflMapData.map (Thm.add_thm deflation_map_thm); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
88 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
89 |
val get_map_tab = MapData.get; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
90 |
val get_deflation_thms = DeflMapData.get; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
91 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
92 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
93 |
(************************** building types and terms **************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
94 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
95 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
96 |
open HOLCF_Library; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
97 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
98 |
infixr 6 ->>; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
99 |
infix -->>; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
100 |
infix 9 `; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
101 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
102 |
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
|
103 |
(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
|
104 |
| mapT T = T ->> T; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
105 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
106 |
fun mk_deflation t = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
107 |
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
|
108 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
109 |
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
|
110 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
111 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
112 |
(****************************** isomorphism info ******************************) |
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 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
115 |
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
|
116 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
117 |
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
|
118 |
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
|
119 |
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
|
120 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
121 |
Drule.export_without_context thm |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
122 |
end |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
123 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
124 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
125 |
(********************* building map functions over types **********************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
126 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
127 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
128 |
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
|
129 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
130 |
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
|
131 |
fun auto T = T ->> T; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
132 |
fun map_of T = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
133 |
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
|
134 |
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
|
135 |
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
|
136 |
(case Symtab.lookup map_tab c of |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
137 |
SOME map_name => |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
138 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
139 |
val map_type = map auto Ts -->> auto T; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
140 |
val (ms, bs) = map_split map_of Ts; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
141 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
142 |
if exists I bs |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
143 |
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
|
144 |
else (mk_ID T, false) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
145 |
end |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
146 |
| NONE => (mk_ID T, false)) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
147 |
| 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
|
148 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
149 |
fst (map_of T) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
150 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
151 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
152 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
153 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
154 |
(********************* declaring definitions and theorems *********************) |
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 |
fun define_const |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
158 |
(bind : binding, rhs : term) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
159 |
(thy : theory) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
160 |
: (term * thm) * theory = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
161 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
162 |
val typ = Term.fastype_of rhs; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
163 |
val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
164 |
val eqn = Logic.mk_equals (const, rhs); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
165 |
val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
166 |
val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
167 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
168 |
((const, def_thm), thy) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
169 |
end; |
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 add_qualified_thm name (path, thm) thy = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
172 |
thy |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
173 |
|> Sign.add_path path |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
174 |
|> yield_singleton PureThy.add_thms |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
175 |
(Thm.no_attributes (Binding.name name, thm)) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
176 |
||> Sign.parent_path; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
177 |
|
35573 | 178 |
fun add_qualified_simp_thm name (path, thm) thy = |
179 |
thy |
|
180 |
|> Sign.add_path path |
|
181 |
|> yield_singleton PureThy.add_thms |
|
182 |
((Binding.name name, thm), [Simplifier.simp_add]) |
|
183 |
||> Sign.parent_path; |
|
184 |
||
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
185 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
186 |
(************************** defining take functions ***************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
187 |
(******************************************************************************) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
188 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
189 |
fun define_take_functions |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
190 |
(spec : (binding * iso_info) list) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
191 |
(thy : theory) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
192 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
193 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
194 |
(* retrieve components of spec *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
195 |
val dom_binds = map fst spec; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
196 |
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
|
197 |
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
|
198 |
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
|
199 |
val dnames = map Binding.name_of dom_binds; |
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 |
(* get table of map functions *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
202 |
val map_tab = MapData.get thy; |
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 mk_projs [] t = [] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
205 |
| 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
|
206 |
| 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
|
207 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
208 |
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
|
209 |
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
|
210 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
211 |
(* define take functional *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
212 |
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
|
213 |
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
|
214 |
val copy_arg = Free ("f", copy_arg_type); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
215 |
val copy_args = map snd (mk_projs dom_binds copy_arg); |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
216 |
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
|
217 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
218 |
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
|
219 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
220 |
mk_cfcomp2 (rep_abs, body) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
221 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
222 |
val take_functional = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
223 |
big_lambda copy_arg |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
224 |
(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
|
225 |
val take_rhss = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
226 |
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
|
227 |
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
|
228 |
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
|
229 |
in |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
230 |
map (lambda n o snd) (mk_projs dom_binds rhs) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
231 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
232 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
233 |
(* define take constants *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
234 |
fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
235 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
236 |
val take_type = HOLogic.natT --> lhsT ->> lhsT; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
237 |
val take_bind = Binding.suffix_name "_take" tbind; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
238 |
val (take_const, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
239 |
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
|
240 |
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
|
241 |
val (take_def_thm, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
242 |
thy |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
243 |
|> Sign.add_path (Binding.name_of tbind) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
244 |
|> yield_singleton |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
245 |
(PureThy.add_defs false o map Thm.no_attributes) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
246 |
(Binding.name "take_def", take_eqn) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
247 |
||> Sign.parent_path; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
248 |
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
|
249 |
val ((take_consts, take_defs), thy) = thy |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
250 |
|> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
251 |
|>> ListPair.unzip; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
252 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
253 |
(* prove chain_take lemmas *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
254 |
fun prove_chain_take (take_const, dname) thy = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
255 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
256 |
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
|
257 |
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
|
258 |
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
|
259 |
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
|
260 |
in |
35573 | 261 |
add_qualified_simp_thm "chain_take" (dname, thm) thy |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
262 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
263 |
val (chain_take_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
264 |
fold_map prove_chain_take (take_consts ~~ dnames) thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
265 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
266 |
(* prove take_0 lemmas *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
267 |
fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
268 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
269 |
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
|
270 |
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
|
271 |
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
|
272 |
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
|
273 |
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
|
274 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
275 |
add_qualified_thm "take_0" (dname, take_0_thm) thy |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
276 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
277 |
val (take_0_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
278 |
fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
279 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
280 |
(* 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
|
281 |
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
|
282 |
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
|
283 |
fun prove_take_Suc |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
284 |
(((take_const, rep_abs), dname), (lhsT, rhsT)) thy = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
285 |
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
|
286 |
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
|
287 |
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
|
288 |
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
|
289 |
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
|
290 |
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
|
291 |
val rules = take_defs @ simps; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
292 |
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
|
293 |
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
|
294 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
295 |
add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
296 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
297 |
val (take_Suc_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
298 |
fold_map prove_take_Suc |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
299 |
(take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
300 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
301 |
(* 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
|
302 |
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
|
303 |
val deflation_take_thm = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
304 |
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
|
305 |
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
|
306 |
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
|
307 |
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
|
308 |
val adm_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
309 |
@{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
|
310 |
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
|
311 |
val bottom_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
312 |
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
|
313 |
val deflation_rules = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
314 |
@{thms conjI deflation_ID} |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
315 |
@ deflation_abs_rep_thms |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
316 |
@ DeflMapData.get thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
317 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
318 |
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
|
319 |
EVERY |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
320 |
[rtac @{thm nat.induct} 1, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
321 |
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
|
322 |
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
|
323 |
REPEAT (etac @{thm conjE} 1 |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
324 |
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
|
325 |
ORELSE atac 1)]) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
326 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
327 |
fun conjuncts [] thm = [] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
328 |
| conjuncts (n::[]) thm = [(n, thm)] |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
329 |
| conjuncts (n::ns) thm = let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
330 |
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
|
331 |
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
|
332 |
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
|
333 |
val (deflation_take_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
334 |
fold_map (add_qualified_thm "deflation_take") |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
335 |
(map (apsnd Drule.export_without_context) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
336 |
(conjuncts dnames deflation_take_thm)) thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
337 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
338 |
(* prove strictness of take functions *) |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
339 |
fun prove_take_strict (deflation_take, dname) thy = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
340 |
let |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
341 |
val take_strict_thm = |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
342 |
Drule.export_without_context |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
343 |
(@{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
|
344 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
345 |
add_qualified_thm "take_strict" (dname, take_strict_thm) thy |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
346 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
347 |
val (take_strict_thms, thy) = |
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
348 |
fold_map prove_take_strict |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
349 |
(deflation_take_thms ~~ dnames) thy; |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
350 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
351 |
(* prove take/take rules *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
352 |
fun prove_take_take ((chain_take, deflation_take), dname) thy = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
353 |
let |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
354 |
val take_take_thm = |
35557
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
355 |
Drule.export_without_context |
5da670d57118
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents:
35555
diff
changeset
|
356 |
(@{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
|
357 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
358 |
add_qualified_thm "take_take" (dname, take_take_thm) thy |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
359 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
360 |
val (take_take_thms, thy) = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
361 |
fold_map prove_take_take |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
362 |
(chain_take_thms ~~ deflation_take_thms ~~ dnames) thy; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
363 |
|
35572
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
364 |
(* prove take_below rules *) |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
365 |
fun prove_take_below (deflation_take, dname) thy = |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
366 |
let |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
367 |
val take_below_thm = |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
368 |
Drule.export_without_context |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
369 |
(@{thm deflation.below} OF [deflation_take]); |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
370 |
in |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
371 |
add_qualified_thm "take_below" (dname, take_below_thm) thy |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
372 |
end; |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
373 |
val (take_below_thms, thy) = |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
374 |
fold_map prove_take_below |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
375 |
(deflation_take_thms ~~ dnames) thy; |
44eeda8cb708
generate lemma take_below, declare chain_take [simp]
huffman
parents:
35557
diff
changeset
|
376 |
|
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
377 |
(* define finiteness predicates *) |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
378 |
fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
379 |
let |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
380 |
val finite_type = lhsT --> boolT; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
381 |
val finite_bind = Binding.suffix_name "_finite" tbind; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
382 |
val (finite_const, thy) = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
383 |
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
|
384 |
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
|
385 |
val n = Free ("n", natT); |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
386 |
val finite_rhs = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
387 |
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
|
388 |
(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
|
389 |
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
|
390 |
val (finite_def_thm, thy) = |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
391 |
thy |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
392 |
|> Sign.add_path (Binding.name_of tbind) |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
393 |
|> yield_singleton |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
394 |
(PureThy.add_defs false o map Thm.no_attributes) |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
395 |
(Binding.name "finite_def", finite_eqn) |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
396 |
||> Sign.parent_path; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
397 |
in ((finite_const, finite_def_thm), thy) end; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
398 |
val ((finite_consts, finite_defs), thy) = thy |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
399 |
|> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns) |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
400 |
|>> ListPair.unzip; |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
401 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
402 |
val result = |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
403 |
{ |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
404 |
take_consts = take_consts, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
405 |
take_defs = take_defs, |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
406 |
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
|
407 |
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
|
408 |
take_Suc_thms = take_Suc_thms, |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
409 |
deflation_take_thms = deflation_take_thms, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
410 |
finite_consts = finite_consts, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
411 |
finite_defs = finite_defs |
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 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
414 |
in |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
415 |
(result, thy) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
416 |
end; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
417 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff
changeset
|
418 |
end; |