author | huffman |
Sat, 22 May 2010 08:30:40 -0700 | |
changeset 37078 | a1656804fcad |
parent 36960 | 01594f816e3a |
child 37744 | 3daaf23b9ab4 |
permissions | -rw-r--r-- |
33774 | 1 |
(* Title: HOLCF/Tools/domain/domain_isomorphism.ML |
2 |
Author: Brian Huffman |
|
3 |
||
4 |
Defines new types satisfying the given domain equations. |
|
5 |
*) |
|
6 |
||
7 |
signature DOMAIN_ISOMORPHISM = |
|
8 |
sig |
|
35489 | 9 |
val domain_isomorphism : |
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
10 |
(string list * binding * mixfix * typ |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
11 |
* (binding * binding) option) list -> |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
12 |
theory -> |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
13 |
(Domain_Take_Proofs.iso_info list |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
14 |
* Domain_Take_Proofs.take_induct_info) * theory |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
15 |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
16 |
val define_map_functions : |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
17 |
(binding * Domain_Take_Proofs.iso_info) list -> |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
18 |
theory -> |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
19 |
{ |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
20 |
map_consts : term list, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
21 |
map_apply_thms : thm list, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
22 |
map_unfold_thms : thm list, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
23 |
deflation_map_thms : thm list |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
24 |
} |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
25 |
* theory |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
26 |
|
35489 | 27 |
val domain_isomorphism_cmd : |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
28 |
(string list * binding * mixfix * string * (binding * binding) option) list |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
29 |
-> theory -> theory |
35489 | 30 |
val add_type_constructor : |
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35478
diff
changeset
|
31 |
(string * term * string * thm * thm * thm * thm) -> theory -> theory |
33774 | 32 |
end; |
33 |
||
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
34 |
structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = |
33774 | 35 |
struct |
36 |
||
37078
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36960
diff
changeset
|
37 |
val beta_rules = |
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36960
diff
changeset
|
38 |
@{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ |
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36960
diff
changeset
|
39 |
@{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_split'}; |
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36960
diff
changeset
|
40 |
|
a1656804fcad
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
huffman
parents:
36960
diff
changeset
|
41 |
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
42 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
43 |
val beta_tac = simp_tac beta_ss; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
44 |
|
33774 | 45 |
(******************************************************************************) |
33791 | 46 |
(******************************** theory data *********************************) |
47 |
(******************************************************************************) |
|
48 |
||
49 |
structure DeflData = Theory_Data |
|
50 |
( |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
51 |
(* terms like "foo_defl" *) |
33791 | 52 |
type T = term Symtab.table; |
53 |
val empty = Symtab.empty; |
|
54 |
val extend = I; |
|
55 |
fun merge data = Symtab.merge (K true) data; |
|
56 |
); |
|
57 |
||
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
58 |
structure RepData = Theory_Data |
33791 | 59 |
( |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
60 |
(* theorems like "REP('a foo) = foo_defl$REP('a)" *) |
33791 | 61 |
type T = thm list; |
62 |
val empty = []; |
|
63 |
val extend = I; |
|
64 |
val merge = Thm.merge_thms; |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
65 |
); |
33791 | 66 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
67 |
structure MapIdData = Theory_Data |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
68 |
( |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
69 |
(* theorems like "foo_map$ID = ID" *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
70 |
type T = thm list; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
71 |
val empty = []; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
72 |
val extend = I; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
73 |
val merge = Thm.merge_thms; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
74 |
); |
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35478
diff
changeset
|
75 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
76 |
structure IsodeflData = Theory_Data |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
77 |
( |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
78 |
(* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *) |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
79 |
type T = thm list; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
80 |
val empty = []; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
81 |
val extend = I; |
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
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:
35498
diff
changeset
|
83 |
); |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
84 |
|
33791 | 85 |
fun add_type_constructor |
35479
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35478
diff
changeset
|
86 |
(tname, defl_const, map_name, REP_thm, |
dffffe36344a
store deflation thms for map functions in theory data
huffman
parents:
35478
diff
changeset
|
87 |
isodefl_thm, map_ID_thm, defl_map_thm) = |
33791 | 88 |
DeflData.map (Symtab.insert (K true) (tname, defl_const)) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
89 |
#> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm) |
33791 | 90 |
#> RepData.map (Thm.add_thm REP_thm) |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
91 |
#> IsodeflData.map (Thm.add_thm isodefl_thm) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
92 |
#> MapIdData.map (Thm.add_thm map_ID_thm); |
33791 | 93 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
94 |
|
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
95 |
(* val get_map_tab = MapData.get; *) |
33801 | 96 |
|
33791 | 97 |
|
98 |
(******************************************************************************) |
|
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
99 |
(************************** building types and terms **************************) |
33774 | 100 |
(******************************************************************************) |
101 |
||
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
102 |
open HOLCF_Library; |
33774 | 103 |
|
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
104 |
infixr 6 ->>; |
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
105 |
infix -->>; |
33774 | 106 |
|
107 |
val deflT = @{typ "udom alg_defl"}; |
|
108 |
||
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
109 |
fun mapT (T as Type (_, Ts)) = |
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
110 |
(map (fn T => T ->> T) Ts) -->> (T ->> T) |
35474 | 111 |
| mapT T = T ->> T; |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
112 |
|
33774 | 113 |
fun mk_Rep_of T = |
114 |
Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; |
|
115 |
||
33778 | 116 |
fun coerce_const T = Const (@{const_name coerce}, T); |
117 |
||
33788 | 118 |
fun isodefl_const T = |
119 |
Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); |
|
120 |
||
35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset
|
121 |
fun mk_deflation t = |
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset
|
122 |
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t; |
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset
|
123 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
124 |
(* splits a cterm into the right and lefthand sides of equality *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
125 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
126 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
127 |
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
128 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
129 |
(******************************************************************************) |
35489 | 130 |
(****************************** isomorphism info ******************************) |
131 |
(******************************************************************************) |
|
132 |
||
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
133 |
fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm = |
35489 | 134 |
let |
135 |
val abs_iso = #abs_inverse info; |
|
136 |
val rep_iso = #rep_inverse info; |
|
137 |
val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso]; |
|
138 |
in |
|
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35842
diff
changeset
|
139 |
Drule.zero_var_indexes thm |
35489 | 140 |
end |
141 |
||
142 |
(******************************************************************************) |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
143 |
(*************** fixed-point definitions and unfolding theorems ***************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
144 |
(******************************************************************************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
145 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
146 |
fun add_fixdefs |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
147 |
(spec : (binding * term) list) |
33788 | 148 |
(thy : theory) : (thm list * thm list) * theory = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
149 |
let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
150 |
val binds = map fst spec; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
151 |
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
152 |
val functional = lambda_tuple lhss (mk_tuple rhss); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
153 |
val fixpoint = mk_fix (mk_cabs functional); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
154 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
155 |
(* project components of fixpoint *) |
35474 | 156 |
fun mk_projs [] t = [] |
157 |
| mk_projs (x::[]) t = [(x, t)] |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
158 |
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
159 |
val projs = mk_projs lhss fixpoint; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
160 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
161 |
(* convert parameters to lambda abstractions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
162 |
fun mk_eqn (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
163 |
case lhs of |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
164 |
Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) => |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
165 |
mk_eqn (f, big_lambda x rhs) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
166 |
| Const _ => Logic.mk_equals (lhs, rhs) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
167 |
| _ => raise TERM ("lhs not of correct form", [lhs, rhs]); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
168 |
val eqns = map mk_eqn projs; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
169 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
170 |
(* register constant definitions *) |
33777 | 171 |
val (fixdef_thms, thy) = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
172 |
(PureThy.add_defs false o map Thm.no_attributes) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
173 |
(map (Binding.suffix_name "_def") binds ~~ eqns) thy; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
174 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
175 |
(* prove applied version of definitions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
176 |
fun prove_proj (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
177 |
let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
178 |
val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
179 |
val goal = Logic.mk_equals (lhs, rhs); |
33777 | 180 |
in Goal.prove_global thy [] [] goal (K tac) end; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
181 |
val proj_thms = map prove_proj projs; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
182 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
183 |
(* mk_tuple lhss == fixpoint *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
184 |
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
185 |
val tuple_fixdef_thm = foldr1 pair_equalI proj_thms; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
186 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
187 |
val cont_thm = |
33777 | 188 |
Goal.prove_global thy [] [] (mk_trp (mk_cont functional)) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
189 |
(K (beta_tac 1)); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
190 |
val tuple_unfold_thm = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
191 |
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36241
diff
changeset
|
192 |
|> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv}; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
193 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
194 |
fun mk_unfold_thms [] thm = [] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
195 |
| mk_unfold_thms (n::[]) thm = [(n, thm)] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
196 |
| mk_unfold_thms (n::ns) thm = let |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
197 |
val thmL = thm RS @{thm Pair_eqD1}; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
198 |
val thmR = thm RS @{thm Pair_eqD2}; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
199 |
in (n, thmL) :: mk_unfold_thms ns thmR end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
200 |
val unfold_binds = map (Binding.suffix_name "_unfold") binds; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
201 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
202 |
(* register unfold theorems *) |
33777 | 203 |
val (unfold_thms, thy) = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35842
diff
changeset
|
204 |
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
33777 | 205 |
(mk_unfold_thms unfold_binds tuple_unfold_thm) thy; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
206 |
in |
33788 | 207 |
((proj_thms, unfold_thms), thy) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
208 |
end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
209 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
210 |
|
33774 | 211 |
(******************************************************************************) |
33790 | 212 |
(****************** deflation combinators and map functions *******************) |
213 |
(******************************************************************************) |
|
33774 | 214 |
|
215 |
fun defl_of_typ |
|
216 |
(tab : term Symtab.table) |
|
217 |
(T : typ) : term = |
|
218 |
let |
|
219 |
fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts |
|
220 |
| is_closed_typ _ = false; |
|
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
221 |
fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT) |
33774 | 222 |
| defl_of (TVar _) = error ("defl_of_typ: TVar") |
223 |
| defl_of (T as Type (c, Ts)) = |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
224 |
case Symtab.lookup tab c of |
35478 | 225 |
SOME t => list_ccomb (t, map defl_of Ts) |
33774 | 226 |
| NONE => if is_closed_typ T |
227 |
then mk_Rep_of T |
|
228 |
else error ("defl_of_typ: type variable under unsupported type constructor " ^ c); |
|
229 |
in defl_of T end; |
|
230 |
||
231 |
||
232 |
(******************************************************************************) |
|
35477 | 233 |
(********************* declaring definitions and theorems *********************) |
234 |
(******************************************************************************) |
|
235 |
||
236 |
fun define_const |
|
237 |
(bind : binding, rhs : term) |
|
238 |
(thy : theory) |
|
239 |
: (term * thm) * theory = |
|
240 |
let |
|
241 |
val typ = Term.fastype_of rhs; |
|
242 |
val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy; |
|
243 |
val eqn = Logic.mk_equals (const, rhs); |
|
244 |
val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn); |
|
245 |
val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy; |
|
246 |
in |
|
247 |
((const, def_thm), thy) |
|
248 |
end; |
|
249 |
||
35773 | 250 |
fun add_qualified_thm name (dbind, thm) = |
251 |
yield_singleton PureThy.add_thms |
|
252 |
((Binding.qualified true name dbind, thm), []); |
|
35489 | 253 |
|
254 |
(******************************************************************************) |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
255 |
(*************************** defining map functions ***************************) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
256 |
(******************************************************************************) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
257 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
258 |
fun define_map_functions |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
259 |
(spec : (binding * Domain_Take_Proofs.iso_info) list) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
260 |
(thy : theory) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
261 |
let |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
262 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
263 |
(* retrieve components of spec *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
264 |
val dbinds = map fst spec; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
265 |
val iso_infos = map snd spec; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
266 |
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
267 |
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
268 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
269 |
(* declare map functions *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
270 |
fun declare_map_const (tbind, (lhsT, rhsT)) thy = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
271 |
let |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
272 |
val map_type = mapT lhsT; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
273 |
val map_bind = Binding.suffix_name "_map" tbind; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
274 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
275 |
Sign.declare_const ((map_bind, map_type), NoSyn) thy |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
276 |
end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
277 |
val (map_consts, thy) = thy |> |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
278 |
fold_map declare_map_const (dbinds ~~ dom_eqns); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
279 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
280 |
(* defining equations for map functions *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
281 |
local |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
282 |
fun unprime a = Library.unprefix "'" a; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
283 |
fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
284 |
fun map_lhs (map_const, lhsT) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
285 |
(lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT)))); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
286 |
val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
287 |
val Ts = (snd o dest_Type o fst o hd) dom_eqns; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
288 |
val tab = (Ts ~~ map mapvar Ts) @ tab1; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
289 |
fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
290 |
let |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
291 |
val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
292 |
val body = Domain_Take_Proofs.map_of_typ thy tab rhsT; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
293 |
val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
294 |
in mk_eqs (lhs, rhs) end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
295 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
296 |
val map_specs = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
297 |
map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
298 |
end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
299 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
300 |
(* register recursive definition of map functions *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
301 |
val map_binds = map (Binding.suffix_name "_map") dbinds; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
302 |
val ((map_apply_thms, map_unfold_thms), thy) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
303 |
add_fixdefs (map_binds ~~ map_specs) thy; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
304 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
305 |
(* prove deflation theorems for map functions *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
306 |
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
307 |
val deflation_map_thm = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
308 |
let |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
309 |
fun unprime a = Library.unprefix "'" a; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
310 |
fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
311 |
fun mk_assm T = mk_trp (mk_deflation (mk_f T)); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
312 |
fun mk_goal (map_const, (lhsT, rhsT)) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
313 |
let |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
314 |
val (_, Ts) = dest_Type lhsT; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
315 |
val map_term = list_ccomb (map_const, map mk_f Ts); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
316 |
in mk_deflation map_term end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
317 |
val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
318 |
val goals = map mk_goal (map_consts ~~ dom_eqns); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
319 |
val goal = mk_trp (foldr1 HOLogic.mk_conj goals); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
320 |
val start_thms = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
321 |
@{thm split_def} :: map_apply_thms; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
322 |
val adm_rules = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
323 |
@{thms adm_conj adm_subst [OF _ adm_deflation] |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
324 |
cont2cont_fst cont2cont_snd cont_id}; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
325 |
val bottom_rules = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
326 |
@{thms fst_strict snd_strict deflation_UU simp_thms}; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
327 |
val deflation_rules = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
328 |
@{thms conjI deflation_ID} |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
329 |
@ deflation_abs_rep_thms |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
330 |
@ Domain_Take_Proofs.get_deflation_thms thy; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
331 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
332 |
Goal.prove_global thy [] assms goal (fn {prems, ...} => |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
333 |
EVERY |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
334 |
[simp_tac (HOL_basic_ss addsimps start_thms) 1, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
335 |
rtac @{thm fix_ind} 1, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
336 |
REPEAT (resolve_tac adm_rules 1), |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
337 |
simp_tac (HOL_basic_ss addsimps bottom_rules) 1, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
338 |
simp_tac beta_ss 1, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
339 |
simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
340 |
REPEAT (etac @{thm conjE} 1), |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
341 |
REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)]) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
342 |
end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
343 |
fun conjuncts [] thm = [] |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
344 |
| conjuncts (n::[]) thm = [(n, thm)] |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
345 |
| conjuncts (n::ns) thm = let |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
346 |
val thmL = thm RS @{thm conjunct1}; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
347 |
val thmR = thm RS @{thm conjunct2}; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
348 |
in (n, thmL):: conjuncts ns thmR end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
349 |
val deflation_map_binds = dbinds |> |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
350 |
map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map"); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
351 |
val (deflation_map_thms, thy) = thy |> |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35842
diff
changeset
|
352 |
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
353 |
(conjuncts deflation_map_binds deflation_map_thm); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
354 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
355 |
(* register map functions in theory data *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
356 |
local |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
357 |
fun register_map ((dname, map_name), defl_thm) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
358 |
Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm); |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
359 |
val dnames = map (fst o dest_Type o fst) dom_eqns; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
360 |
val map_names = map (fst o dest_Const) map_consts; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
361 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
362 |
val thy = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
363 |
fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
364 |
end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
365 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
366 |
val result = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
367 |
{ |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
368 |
map_consts = map_consts, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
369 |
map_apply_thms = map_apply_thms, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
370 |
map_unfold_thms = map_unfold_thms, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
371 |
deflation_map_thms = deflation_map_thms |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
372 |
} |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
373 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
374 |
(result, thy) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
375 |
end; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
376 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
377 |
(******************************************************************************) |
35477 | 378 |
(******************************* main function ********************************) |
379 |
(******************************************************************************) |
|
33774 | 380 |
|
381 |
fun read_typ thy str sorts = |
|
382 |
let |
|
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36241
diff
changeset
|
383 |
val ctxt = ProofContext.init_global thy |
33774 | 384 |
|> fold (Variable.declare_typ o TFree) sorts; |
385 |
val T = Syntax.read_typ ctxt str; |
|
386 |
in (T, Term.add_tfreesT T sorts) end; |
|
387 |
||
388 |
fun cert_typ sign raw_T sorts = |
|
389 |
let |
|
390 |
val T = Type.no_tvars (Sign.certify_typ sign raw_T) |
|
391 |
handle TYPE (msg, _, _) => error msg; |
|
392 |
val sorts' = Term.add_tfreesT T sorts; |
|
393 |
val _ = |
|
394 |
case duplicates (op =) (map fst sorts') of |
|
395 |
[] => () |
|
396 |
| dups => error ("Inconsistent sort constraints for " ^ commas dups) |
|
397 |
in (T, sorts') end; |
|
398 |
||
399 |
fun gen_domain_isomorphism |
|
400 |
(prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list) |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
401 |
(doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list) |
33774 | 402 |
(thy: theory) |
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
403 |
: (Domain_Take_Proofs.iso_info list |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
404 |
* Domain_Take_Proofs.take_induct_info) * theory = |
33774 | 405 |
let |
33792 | 406 |
val _ = Theory.requires thy "Representable" "domain isomorphisms"; |
33774 | 407 |
|
408 |
(* this theory is used just for parsing *) |
|
409 |
val tmp_thy = thy |> |
|
410 |
Theory.copy |> |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
411 |
Sign.add_types (map (fn (tvs, tname, mx, _, morphs) => |
33774 | 412 |
(tname, length tvs, mx)) doms_raw); |
413 |
||
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
414 |
fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts = |
33774 | 415 |
let val (typ, sorts') = prep_typ thy typ_raw sorts |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
416 |
in ((vs, t, mx, typ, morphs), sorts') end; |
33774 | 417 |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
418 |
val (doms : (string list * binding * mixfix * typ * (binding * binding) option) list, |
33774 | 419 |
sorts : (string * sort) list) = |
420 |
fold_map (prep_dom tmp_thy) doms_raw []; |
|
421 |
||
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
422 |
(* domain equations *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
423 |
fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
424 |
let fun arg v = TFree (v, the (AList.lookup (op =) sorts v)); |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
425 |
in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
426 |
val dom_eqns = map mk_dom_eqn doms; |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
427 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
428 |
(* check for valid type parameters *) |
35474 | 429 |
val (tyvars, _, _, _, _) = hd doms; |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
430 |
val new_doms = map (fn (tvs, tname, mx, _, _) => |
33774 | 431 |
let val full_tname = Sign.full_name tmp_thy tname |
432 |
in |
|
433 |
(case duplicates (op =) tvs of |
|
434 |
[] => |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
435 |
if eq_set (op =) (tyvars, tvs) then (full_tname, tvs) |
33774 | 436 |
else error ("Mutually recursive domains must have same type parameters") |
437 |
| dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^ |
|
438 |
" : " ^ commas dups)) |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
439 |
end) doms; |
35773 | 440 |
val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms; |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
441 |
val morphs = map (fn (_, _, _, _, morphs) => morphs) doms; |
33774 | 442 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
443 |
(* declare deflation combinator constants *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
444 |
fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy = |
33774 | 445 |
let |
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
446 |
val defl_type = map (K deflT) vs -->> deflT; |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
447 |
val defl_bind = Binding.suffix_name "_defl" tbind; |
33774 | 448 |
in |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
449 |
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy |
33774 | 450 |
end; |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
451 |
val (defl_consts, thy) = fold_map declare_defl_const doms thy; |
33774 | 452 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
453 |
(* defining equations for type combinators *) |
33790 | 454 |
val defl_tab1 = DeflData.get thy; |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
455 |
val defl_tab2 = |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
456 |
Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts); |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
457 |
val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2); |
33790 | 458 |
val thy = DeflData.put defl_tab' thy; |
33776 | 459 |
fun mk_defl_spec (lhsT, rhsT) = |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
460 |
mk_eqs (defl_of_typ defl_tab' lhsT, |
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
461 |
defl_of_typ defl_tab' rhsT); |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
462 |
val defl_specs = map mk_defl_spec dom_eqns; |
33774 | 463 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
464 |
(* register recursive definition of deflation combinators *) |
35773 | 465 |
val defl_binds = map (Binding.suffix_name "_defl") dbinds; |
33788 | 466 |
val ((defl_apply_thms, defl_unfold_thms), thy) = |
467 |
add_fixdefs (defl_binds ~~ defl_specs) thy; |
|
33774 | 468 |
|
33776 | 469 |
(* define types using deflation combinators *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
470 |
fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy = |
33774 | 471 |
let |
472 |
fun tfree a = TFree (a, the (AList.lookup (op =) sorts a)) |
|
473 |
val reps = map (mk_Rep_of o tfree) vs; |
|
35478 | 474 |
val defl = list_ccomb (defl_const, reps); |
33777 | 475 |
val ((_, _, _, {REP, ...}), thy) = |
35842 | 476 |
Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy; |
33774 | 477 |
in |
33777 | 478 |
(REP, thy) |
33774 | 479 |
end; |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
480 |
val (REP_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy; |
33791 | 481 |
val thy = RepData.map (fold Thm.add_thm REP_thms) thy; |
33776 | 482 |
|
483 |
(* prove REP equations *) |
|
33782 | 484 |
fun mk_REP_eq_thm (lhsT, rhsT) = |
33776 | 485 |
let |
486 |
val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT); |
|
33791 | 487 |
val REP_simps = RepData.get thy; |
33776 | 488 |
val tac = |
35589
a76cce4ad320
fix proof script so qdomain_isomorphism foo = foo' works
huffman
parents:
35557
diff
changeset
|
489 |
rewrite_goals_tac (map mk_meta_eq REP_simps) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
490 |
THEN resolve_tac defl_unfold_thms 1; |
33776 | 491 |
in |
33777 | 492 |
Goal.prove_global thy [] [] goal (K tac) |
33776 | 493 |
end; |
33782 | 494 |
val REP_eq_thms = map mk_REP_eq_thm dom_eqns; |
495 |
||
496 |
(* register REP equations *) |
|
35773 | 497 |
val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds; |
33782 | 498 |
val (_, thy) = thy |> |
499 |
(PureThy.add_thms o map Thm.no_attributes) |
|
500 |
(REP_eq_binds ~~ REP_eq_thms); |
|
33776 | 501 |
|
33778 | 502 |
(* define rep/abs functions *) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
503 |
fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy = |
33778 | 504 |
let |
505 |
val rep_bind = Binding.suffix_name "_rep" tbind; |
|
506 |
val abs_bind = Binding.suffix_name "_abs" tbind; |
|
35477 | 507 |
val ((rep_const, rep_def), thy) = |
508 |
define_const (rep_bind, coerce_const (lhsT ->> rhsT)) thy; |
|
509 |
val ((abs_const, abs_def), thy) = |
|
510 |
define_const (abs_bind, coerce_const (rhsT ->> lhsT)) thy; |
|
33778 | 511 |
in |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
512 |
(((rep_const, abs_const), (rep_def, abs_def)), thy) |
33778 | 513 |
end; |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
514 |
val ((rep_abs_consts, rep_abs_defs), thy) = thy |
35773 | 515 |
|> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns) |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
516 |
|>> ListPair.unzip; |
33782 | 517 |
|
518 |
(* prove isomorphism and isodefl rules *) |
|
519 |
fun mk_iso_thms ((tbind, REP_eq), (rep_def, abs_def)) thy = |
|
520 |
let |
|
35773 | 521 |
fun make thm = |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35842
diff
changeset
|
522 |
Drule.zero_var_indexes (thm OF [REP_eq, abs_def, rep_def]); |
33782 | 523 |
val rep_iso_thm = make @{thm domain_rep_iso}; |
524 |
val abs_iso_thm = make @{thm domain_abs_iso}; |
|
525 |
val isodefl_thm = make @{thm isodefl_abs_rep}; |
|
35773 | 526 |
val thy = thy |
527 |
|> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm) |
|
528 |
|> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm) |
|
529 |
|> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm); |
|
33782 | 530 |
in |
531 |
(((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) |
|
532 |
end; |
|
35489 | 533 |
val ((iso_thms, isodefl_abs_rep_thms), thy) = |
35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset
|
534 |
thy |
35773 | 535 |
|> fold_map mk_iso_thms (dbinds ~~ REP_eq_thms ~~ rep_abs_defs) |
33782 | 536 |
|>> ListPair.unzip; |
33778 | 537 |
|
35467
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
538 |
(* collect info about rep/abs *) |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
539 |
val iso_infos : Domain_Take_Proofs.iso_info list = |
35467
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
540 |
let |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
541 |
fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) = |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
542 |
{ |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
543 |
repT = rhsT, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
544 |
absT = lhsT, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
545 |
rep_const = repC, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
546 |
abs_const = absC, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
547 |
rep_inverse = rep_iso, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
548 |
abs_inverse = abs_iso |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
549 |
}; |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
550 |
in |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
551 |
map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms) |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
552 |
end |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
553 |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
554 |
(* definitions and proofs related to map functions *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
555 |
val (map_info, thy) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
556 |
define_map_functions (dbinds ~~ iso_infos) thy; |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
557 |
val { map_consts, map_apply_thms, map_unfold_thms, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
558 |
deflation_map_thms } = map_info; |
33788 | 559 |
|
560 |
(* prove isodefl rules for map functions *) |
|
561 |
val isodefl_thm = |
|
562 |
let |
|
563 |
fun unprime a = Library.unprefix "'" a; |
|
35474 | 564 |
fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT); |
565 |
fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T); |
|
33788 | 566 |
fun mk_assm T = mk_trp (isodefl_const T $ mk_f T $ mk_d T); |
35474 | 567 |
fun mk_goal ((map_const, defl_const), (T, rhsT)) = |
33788 | 568 |
let |
35474 | 569 |
val (_, Ts) = dest_Type T; |
35478 | 570 |
val map_term = list_ccomb (map_const, map mk_f Ts); |
571 |
val defl_term = list_ccomb (defl_const, map mk_d Ts); |
|
33788 | 572 |
in isodefl_const T $ map_term $ defl_term end; |
573 |
val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns; |
|
574 |
val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns); |
|
575 |
val goal = mk_trp (foldr1 HOLogic.mk_conj goals); |
|
576 |
val start_thms = |
|
577 |
@{thm split_def} :: defl_apply_thms @ map_apply_thms; |
|
578 |
val adm_rules = |
|
579 |
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}; |
|
580 |
val bottom_rules = |
|
581 |
@{thms fst_strict snd_strict isodefl_bottom simp_thms}; |
|
35640
9617aeca7147
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
huffman
parents:
35624
diff
changeset
|
582 |
val REP_simps = map (fn th => th RS sym) (RepData.get thy); |
33788 | 583 |
val isodefl_rules = |
33791 | 584 |
@{thms conjI isodefl_ID_REP} |
585 |
@ isodefl_abs_rep_thms |
|
586 |
@ IsodeflData.get thy; |
|
33845 | 587 |
in |
588 |
Goal.prove_global thy [] assms goal (fn {prems, ...} => |
|
589 |
EVERY |
|
33788 | 590 |
[simp_tac (HOL_basic_ss addsimps start_thms) 1, |
33791 | 591 |
(* FIXME: how reliable is unification here? *) |
592 |
(* Maybe I should instantiate the rule. *) |
|
33788 | 593 |
rtac @{thm parallel_fix_ind} 1, |
594 |
REPEAT (resolve_tac adm_rules 1), |
|
595 |
simp_tac (HOL_basic_ss addsimps bottom_rules) 1, |
|
596 |
simp_tac beta_ss 1, |
|
597 |
simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, |
|
35640
9617aeca7147
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
huffman
parents:
35624
diff
changeset
|
598 |
simp_tac (HOL_basic_ss addsimps REP_simps) 1, |
33788 | 599 |
REPEAT (etac @{thm conjE} 1), |
33845 | 600 |
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)]) |
33788 | 601 |
end; |
35773 | 602 |
val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds; |
33789 | 603 |
fun conjuncts [] thm = [] |
604 |
| conjuncts (n::[]) thm = [(n, thm)] |
|
605 |
| conjuncts (n::ns) thm = let |
|
606 |
val thmL = thm RS @{thm conjunct1}; |
|
607 |
val thmR = thm RS @{thm conjunct2}; |
|
608 |
in (n, thmL):: conjuncts ns thmR end; |
|
609 |
val (isodefl_thms, thy) = thy |> |
|
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35842
diff
changeset
|
610 |
(PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
33789 | 611 |
(conjuncts isodefl_binds isodefl_thm); |
33791 | 612 |
val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy; |
33793 | 613 |
|
614 |
(* prove map_ID theorems *) |
|
615 |
fun prove_map_ID_thm |
|
616 |
(((map_const, (lhsT, _)), REP_thm), isodefl_thm) = |
|
617 |
let |
|
618 |
val Ts = snd (dest_Type lhsT); |
|
35478 | 619 |
val lhs = list_ccomb (map_const, map mk_ID Ts); |
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
620 |
val goal = mk_eqs (lhs, mk_ID lhsT); |
33793 | 621 |
val tac = EVERY |
622 |
[rtac @{thm isodefl_REP_imp_ID} 1, |
|
623 |
stac REP_thm 1, |
|
624 |
rtac isodefl_thm 1, |
|
625 |
REPEAT (rtac @{thm isodefl_ID_REP} 1)]; |
|
626 |
in |
|
627 |
Goal.prove_global thy [] [] goal (K tac) |
|
628 |
end; |
|
35773 | 629 |
val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds; |
33793 | 630 |
val map_ID_thms = |
631 |
map prove_map_ID_thm |
|
632 |
(map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms); |
|
633 |
val (_, thy) = thy |> |
|
634 |
(PureThy.add_thms o map Thm.no_attributes) |
|
635 |
(map_ID_binds ~~ map_ID_thms); |
|
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
636 |
val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy; |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
637 |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
638 |
(* definitions and proofs related to take functions *) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
639 |
val (take_info, thy) = |
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
640 |
Domain_Take_Proofs.define_take_functions |
35773 | 641 |
(dbinds ~~ iso_infos) thy; |
35515
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
642 |
val { take_consts, take_defs, chain_take_thms, take_0_thms, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
643 |
take_Suc_thms, deflation_take_thms, |
d631dc53ede0
move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents:
35514
diff
changeset
|
644 |
finite_consts, finite_defs } = take_info; |
33807
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
645 |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
646 |
(* least-upper-bound lemma for take functions *) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
647 |
val lub_take_lemma = |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
648 |
let |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
649 |
val lhs = mk_tuple (map mk_lub take_consts); |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
650 |
fun mk_map_ID (map_const, (lhsT, rhsT)) = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
651 |
list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT))); |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
652 |
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)); |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
653 |
val goal = mk_trp (mk_eq (lhs, rhs)); |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
654 |
val start_rules = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
655 |
@{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
656 |
@ @{thms pair_collapse split_def} |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
657 |
@ map_apply_thms @ MapIdData.get thy; |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
658 |
val rules0 = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
659 |
@{thms iterate_0 Pair_strict} @ take_0_thms; |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
660 |
val rules1 = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
661 |
@{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv} |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
662 |
@ take_Suc_thms; |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
663 |
val tac = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
664 |
EVERY |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
665 |
[simp_tac (HOL_basic_ss addsimps start_rules) 1, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
666 |
simp_tac (HOL_basic_ss addsimps @{thms fix_def2}) 1, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
667 |
rtac @{thm lub_eq} 1, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
668 |
rtac @{thm nat.induct} 1, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
669 |
simp_tac (HOL_basic_ss addsimps rules0) 1, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
670 |
asm_full_simp_tac (beta_ss addsimps rules1) 1]; |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
671 |
in |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
672 |
Goal.prove_global thy [] [] goal (K tac) |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
673 |
end; |
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
674 |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
675 |
(* prove lub of take equals ID *) |
35773 | 676 |
fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy = |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
677 |
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
|
678 |
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
|
679 |
val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT); |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
680 |
val tac = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
681 |
EVERY |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
682 |
[rtac @{thm trans} 1, rtac map_ID_thm 2, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
683 |
cut_facts_tac [lub_take_lemma] 1, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
684 |
REPEAT (etac @{thm Pair_inject} 1), atac 1]; |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
685 |
val lub_take_thm = Goal.prove_global thy [] [] goal (K tac); |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
686 |
in |
35773 | 687 |
add_qualified_thm "lub_take" (dbind, lub_take_thm) thy |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
688 |
end; |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
689 |
val (lub_take_thms, thy) = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
690 |
fold_map prove_lub_take |
35773 | 691 |
(dbinds ~~ take_consts ~~ map_ID_thms ~~ dom_eqns) thy; |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
692 |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35640
diff
changeset
|
693 |
(* prove additional take theorems *) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35640
diff
changeset
|
694 |
val (take_info2, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35640
diff
changeset
|
695 |
Domain_Take_Proofs.add_lub_take_theorems |
35773 | 696 |
(dbinds ~~ iso_infos) take_info lub_take_thms thy; |
33774 | 697 |
in |
35659 | 698 |
((iso_infos, take_info2), thy) |
33774 | 699 |
end; |
700 |
||
701 |
val domain_isomorphism = gen_domain_isomorphism cert_typ; |
|
35467
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
702 |
val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ; |
33774 | 703 |
|
704 |
(******************************************************************************) |
|
705 |
(******************************** outer syntax ********************************) |
|
706 |
(******************************************************************************) |
|
707 |
||
708 |
local |
|
709 |
||
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
710 |
val parse_domain_iso : |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
711 |
(string list * binding * mixfix * string * (binding * binding) option) |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
712 |
parser = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
713 |
(Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
714 |
Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))) |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
715 |
>> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)); |
33774 | 716 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
717 |
val parse_domain_isos = Parse.and_list1 parse_domain_iso; |
33774 | 718 |
|
719 |
in |
|
720 |
||
721 |
val _ = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
722 |
Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
723 |
Keyword.thy_decl |
33774 | 724 |
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)); |
725 |
||
726 |
end; |
|
727 |
||
728 |
end; |