author | wenzelm |
Tue, 10 Feb 2015 14:48:26 +0100 | |
changeset 59498 | 50b60f501b05 |
parent 58957 | c9e744ea8a38 |
child 59936 | b8ffc3dc9e24 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/Domain/domain_isomorphism.ML |
33774 | 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, |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
23 |
map_cont_thm : thm, |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
24 |
deflation_map_thms : thm list |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
25 |
} |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
26 |
* theory |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
27 |
|
35489 | 28 |
val domain_isomorphism_cmd : |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
29 |
(string list * binding * mixfix * string * (binding * binding) option) list |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
30 |
-> theory -> theory |
40832 | 31 |
end |
33774 | 32 |
|
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
33 |
structure Domain_Isomorphism : DOMAIN_ISOMORPHISM = |
33774 | 34 |
struct |
35 |
||
40833
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
36 |
val beta_ss = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
37 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
38 |
addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
39 |
|
40832 | 40 |
fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo}) |
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
41 |
|
33791 | 42 |
|
43 |
(******************************************************************************) |
|
35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35474
diff
changeset
|
44 |
(************************** building types and terms **************************) |
33774 | 45 |
(******************************************************************************) |
46 |
||
40832 | 47 |
open HOLCF_Library |
33774 | 48 |
|
40832 | 49 |
infixr 6 ->> |
50 |
infixr -->> |
|
33774 | 51 |
|
40832 | 52 |
val udomT = @{typ udom} |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40833
diff
changeset
|
53 |
val deflT = @{typ "udom defl"} |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
54 |
val udeflT = @{typ "udom u defl"} |
33774 | 55 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
56 |
fun mk_DEFL T = |
40832 | 57 |
Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T |
33774 | 58 |
|
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
59 |
fun dest_DEFL (Const (@{const_name defl}, _) $ t) = Logic.dest_type t |
40832 | 60 |
| dest_DEFL t = raise TERM ("dest_DEFL", [t]) |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
61 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
62 |
fun mk_LIFTDEFL T = |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
63 |
Const (@{const_name liftdefl}, Term.itselfT T --> udeflT) $ Logic.mk_type T |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
64 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
65 |
fun dest_LIFTDEFL (Const (@{const_name liftdefl}, _) $ t) = Logic.dest_type t |
40832 | 66 |
| dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t]) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
67 |
|
40832 | 68 |
fun mk_u_defl t = mk_capply (@{const "u_defl"}, t) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
69 |
|
40832 | 70 |
fun emb_const T = Const (@{const_name emb}, T ->> udomT) |
71 |
fun prj_const T = Const (@{const_name prj}, udomT ->> T) |
|
72 |
fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T) |
|
33778 | 73 |
|
33788 | 74 |
fun isodefl_const T = |
40832 | 75 |
Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT) |
33788 | 76 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
77 |
fun isodefl'_const T = |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
78 |
Const (@{const_name isodefl'}, (T ->> T) --> udeflT --> HOLogic.boolT) |
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
79 |
|
35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset
|
80 |
fun mk_deflation t = |
40832 | 81 |
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t |
35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset
|
82 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
83 |
(* splits a cterm into the right and lefthand sides of equality *) |
40832 | 84 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
85 |
|
40832 | 86 |
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
87 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
88 |
(******************************************************************************) |
35489 | 89 |
(****************************** isomorphism info ******************************) |
90 |
(******************************************************************************) |
|
91 |
||
35514
a2cfa413eaab
move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35498
diff
changeset
|
92 |
fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm = |
35489 | 93 |
let |
40832 | 94 |
val abs_iso = #abs_inverse info |
95 |
val rep_iso = #rep_inverse info |
|
96 |
val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso] |
|
35489 | 97 |
in |
36241
2a4cec6bcae2
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents:
35842
diff
changeset
|
98 |
Drule.zero_var_indexes thm |
35489 | 99 |
end |
100 |
||
101 |
(******************************************************************************) |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
102 |
(*************** fixed-point definitions and unfolding theorems ***************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
103 |
(******************************************************************************) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
104 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
105 |
fun mk_projs [] _ = [] |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
106 |
| mk_projs (x::[]) t = [(x, t)] |
40832 | 107 |
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
108 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
109 |
fun add_fixdefs |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
110 |
(spec : (binding * term) list) |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
111 |
(thy : theory) : (thm list * thm list * thm) * theory = |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
112 |
let |
40832 | 113 |
val binds = map fst spec |
114 |
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec) |
|
115 |
val functional = lambda_tuple lhss (mk_tuple rhss) |
|
116 |
val fixpoint = mk_fix (mk_cabs functional) |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
117 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
118 |
(* project components of fixpoint *) |
40832 | 119 |
val projs = mk_projs lhss fixpoint |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
120 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
121 |
(* convert parameters to lambda abstractions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
122 |
fun mk_eqn (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
123 |
case lhs of |
40327 | 124 |
Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) => |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
125 |
mk_eqn (f, big_lambda x rhs) |
56243 | 126 |
| f $ Const (@{const_name Pure.type}, T) => |
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
127 |
mk_eqn (f, Abs ("t", T, rhs)) |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
128 |
| Const _ => Logic.mk_equals (lhs, rhs) |
40832 | 129 |
| _ => raise TERM ("lhs not of correct form", [lhs, rhs]) |
130 |
val eqns = map mk_eqn projs |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
131 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
132 |
(* register constant definitions *) |
33777 | 133 |
val (fixdef_thms, thy) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
134 |
(Global_Theory.add_defs false o map Thm.no_attributes) |
46909 | 135 |
(map Thm.def_binding binds ~~ eqns) thy |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
136 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
137 |
(* prove applied version of definitions *) |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
138 |
fun prove_proj (lhs, rhs) = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
139 |
let |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
140 |
fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN |
54895 | 141 |
(simp_tac (put_simpset beta_ss ctxt)) 1 |
40832 | 142 |
val goal = Logic.mk_equals (lhs, rhs) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
143 |
in Goal.prove_global thy [] [] goal (tac o #context) end |
40832 | 144 |
val proj_thms = map prove_proj projs |
33775
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 |
(* mk_tuple lhss == fixpoint *) |
40832 | 147 |
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2] |
148 |
val tuple_fixdef_thm = foldr1 pair_equalI proj_thms |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
149 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
150 |
val cont_thm = |
40833
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
151 |
let |
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
152 |
val prop = mk_trp (mk_cont functional) |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
153 |
val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont} |
58957 | 154 |
fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1 |
40833
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
155 |
in |
58957 | 156 |
Goal.prove_global thy [] [] prop (tac o #context) |
40833
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
157 |
end |
4f130bd9e17e
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
huffman
parents:
40832
diff
changeset
|
158 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
159 |
val tuple_unfold_thm = |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
160 |
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) |
42361 | 161 |
|> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv} |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
162 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
163 |
fun mk_unfold_thms [] _ = [] |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
164 |
| mk_unfold_thms (n::[]) thm = [(n, thm)] |
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
165 |
| mk_unfold_thms (n::ns) thm = let |
40832 | 166 |
val thmL = thm RS @{thm Pair_eqD1} |
167 |
val thmR = thm RS @{thm Pair_eqD2} |
|
168 |
in (n, thmL) :: mk_unfold_thms ns thmR end |
|
169 |
val unfold_binds = map (Binding.suffix_name "_unfold") binds |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
170 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
171 |
(* register unfold theorems *) |
33777 | 172 |
val (unfold_thms, thy) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
173 |
(Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
40832 | 174 |
(mk_unfold_thms unfold_binds tuple_unfold_thm) thy |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
175 |
in |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
176 |
((proj_thms, unfold_thms, cont_thm), thy) |
40832 | 177 |
end |
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
178 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
179 |
|
33774 | 180 |
(******************************************************************************) |
33790 | 181 |
(****************** deflation combinators and map functions *******************) |
182 |
(******************************************************************************) |
|
33774 | 183 |
|
184 |
fun defl_of_typ |
|
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
185 |
(thy : theory) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
186 |
(tab1 : (typ * term) list) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
187 |
(tab2 : (typ * term) list) |
33774 | 188 |
(T : typ) : term = |
189 |
let |
|
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
190 |
val defl_simps = |
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
191 |
Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps} |
57954
c52223cd1003
clarified order of rules for match_tac/resolve_tac;
wenzelm
parents:
57945
diff
changeset
|
192 |
val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) (rev defl_simps) |
40832 | 193 |
val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2 |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
194 |
fun proc1 t = |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
195 |
(case dest_DEFL t of |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
196 |
TFree (a, _) => SOME (Free ("d" ^ Library.unprefix "'" a, deflT)) |
40832 | 197 |
| _ => NONE) handle TERM _ => NONE |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
198 |
fun proc2 t = |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
199 |
(case dest_LIFTDEFL t of |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
200 |
TFree (a, _) => SOME (Free ("p" ^ Library.unprefix "'" a, udeflT)) |
40832 | 201 |
| _ => NONE) handle TERM _ => NONE |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
202 |
in |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
203 |
Pattern.rewrite_term thy (rules @ rules') [proc1, proc2] (mk_DEFL T) |
40832 | 204 |
end |
33774 | 205 |
|
206 |
(******************************************************************************) |
|
35477 | 207 |
(********************* declaring definitions and theorems *********************) |
208 |
(******************************************************************************) |
|
209 |
||
210 |
fun define_const |
|
211 |
(bind : binding, rhs : term) |
|
212 |
(thy : theory) |
|
213 |
: (term * thm) * theory = |
|
214 |
let |
|
40832 | 215 |
val typ = Term.fastype_of rhs |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
216 |
val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy |
40832 | 217 |
val eqn = Logic.mk_equals (const, rhs) |
46909 | 218 |
val def = Thm.no_attributes (Thm.def_binding bind, eqn) |
40832 | 219 |
val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy |
35477 | 220 |
in |
221 |
((const, def_thm), thy) |
|
40832 | 222 |
end |
35477 | 223 |
|
35773 | 224 |
fun add_qualified_thm name (dbind, thm) = |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
225 |
yield_singleton Global_Theory.add_thms |
40832 | 226 |
((Binding.qualified true name dbind, thm), []) |
35489 | 227 |
|
228 |
(******************************************************************************) |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
229 |
(*************************** defining map functions ***************************) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
230 |
(******************************************************************************) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
231 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
232 |
fun define_map_functions |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
233 |
(spec : (binding * Domain_Take_Proofs.iso_info) list) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
234 |
(thy : theory) = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
235 |
let |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
236 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
237 |
(* retrieve components of spec *) |
40832 | 238 |
val dbinds = map fst spec |
239 |
val iso_infos = map snd spec |
|
240 |
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos |
|
241 |
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
242 |
|
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
243 |
fun mapT (T as Type (_, Ts)) = |
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
244 |
(map (fn T => T ->> T) (filter (is_cpo thy) Ts)) -->> (T ->> T) |
40832 | 245 |
| mapT T = T ->> T |
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
246 |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
247 |
(* declare map functions *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
248 |
fun declare_map_const (tbind, (lhsT, _)) thy = |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
249 |
let |
40832 | 250 |
val map_type = mapT lhsT |
251 |
val map_bind = Binding.suffix_name "_map" tbind |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
252 |
in |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
253 |
Sign.declare_const_global ((map_bind, map_type), NoSyn) thy |
40832 | 254 |
end |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
255 |
val (map_consts, thy) = thy |> |
40832 | 256 |
fold_map declare_map_const (dbinds ~~ dom_eqns) |
35791
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 |
(* defining equations for map functions *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
259 |
local |
40832 | 260 |
fun unprime a = Library.unprefix "'" a |
261 |
fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T) |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
262 |
fun map_lhs (map_const, lhsT) = |
40832 | 263 |
(lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (snd (dest_Type lhsT))))) |
264 |
val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns) |
|
265 |
val Ts = (snd o dest_Type o fst o hd) dom_eqns |
|
266 |
val tab = (Ts ~~ map mapvar Ts) @ tab1 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
267 |
fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) = |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
268 |
let |
40832 | 269 |
val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT |
270 |
val body = Domain_Take_Proofs.map_of_typ thy tab rhsT |
|
271 |
val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const)) |
|
272 |
in mk_eqs (lhs, rhs) end |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
273 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
274 |
val map_specs = |
40832 | 275 |
map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns) |
276 |
end |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
277 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
278 |
(* register recursive definition of map functions *) |
40832 | 279 |
val map_binds = map (Binding.suffix_name "_map") dbinds |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
280 |
val ((map_apply_thms, map_unfold_thms, map_cont_thm), thy) = |
40832 | 281 |
add_fixdefs (map_binds ~~ map_specs) thy |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
282 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
283 |
(* prove deflation theorems for map functions *) |
40832 | 284 |
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
285 |
val deflation_map_thm = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
286 |
let |
40832 | 287 |
fun unprime a = Library.unprefix "'" a |
288 |
fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T) |
|
289 |
fun mk_assm T = mk_trp (mk_deflation (mk_f T)) |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
290 |
fun mk_goal (map_const, (lhsT, _)) = |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
291 |
let |
40832 | 292 |
val (_, Ts) = dest_Type lhsT |
293 |
val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts)) |
|
294 |
in mk_deflation map_term end |
|
295 |
val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns |
|
296 |
val goals = map mk_goal (map_consts ~~ dom_eqns) |
|
297 |
val goal = mk_trp (foldr1 HOLogic.mk_conj goals) |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
298 |
val adm_rules = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
299 |
@{thms adm_conj adm_subst [OF _ adm_deflation] |
40832 | 300 |
cont2cont_fst cont2cont_snd cont_id} |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
301 |
val bottom_rules = |
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41324
diff
changeset
|
302 |
@{thms fst_strict snd_strict deflation_bottom simp_thms} |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
303 |
val tuple_rules = |
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
304 |
@{thms split_def fst_conv snd_conv} |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
305 |
val deflation_rules = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
306 |
@{thms conjI deflation_ID} |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
307 |
@ deflation_abs_rep_thms |
40832 | 308 |
@ Domain_Take_Proofs.get_deflation_thms thy |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
309 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
310 |
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
311 |
EVERY |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
312 |
[rewrite_goals_tac ctxt map_apply_thms, |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
313 |
rtac (map_cont_thm RS @{thm cont_fix_ind}) 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
314 |
REPEAT (resolve_tac ctxt adm_rules 1), |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
315 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
316 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1, |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
317 |
REPEAT (etac @{thm conjE} 1), |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
318 |
REPEAT (resolve_tac ctxt (deflation_rules @ prems) 1 ORELSE atac 1)]) |
40832 | 319 |
end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
320 |
fun conjuncts [] _ = [] |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
321 |
| conjuncts (n::[]) thm = [(n, thm)] |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
322 |
| conjuncts (n::ns) thm = let |
40832 | 323 |
val thmL = thm RS @{thm conjunct1} |
324 |
val thmR = thm RS @{thm conjunct2} |
|
325 |
in (n, thmL):: conjuncts ns thmR end |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
326 |
val deflation_map_binds = dbinds |> |
40832 | 327 |
map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map") |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
328 |
val (deflation_map_thms, thy) = thy |> |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
329 |
(Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
40832 | 330 |
(conjuncts deflation_map_binds deflation_map_thm) |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
331 |
|
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40575
diff
changeset
|
332 |
(* register indirect recursion in theory data *) |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
333 |
local |
40737
2037021f034f
remove map function names from domain package theory data
huffman
parents:
40575
diff
changeset
|
334 |
fun register_map (dname, args) = |
40832 | 335 |
Domain_Take_Proofs.add_rec_type (dname, args) |
336 |
val dnames = map (fst o dest_Type o fst) dom_eqns |
|
337 |
fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => [] |
|
338 |
val argss = map args dom_eqns |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
339 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
340 |
val thy = |
40832 | 341 |
fold register_map (dnames ~~ argss) thy |
342 |
end |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
343 |
|
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40037
diff
changeset
|
344 |
(* register deflation theorems *) |
40832 | 345 |
val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy |
40216
366309dfaf60
use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents:
40037
diff
changeset
|
346 |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
347 |
val result = |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
348 |
{ |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
349 |
map_consts = map_consts, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
350 |
map_apply_thms = map_apply_thms, |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
351 |
map_unfold_thms = map_unfold_thms, |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
352 |
map_cont_thm = map_cont_thm, |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
353 |
deflation_map_thms = deflation_map_thms |
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 |
in |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
356 |
(result, thy) |
40832 | 357 |
end |
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
358 |
|
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
359 |
(******************************************************************************) |
35477 | 360 |
(******************************* main function ********************************) |
361 |
(******************************************************************************) |
|
33774 | 362 |
|
363 |
fun read_typ thy str sorts = |
|
364 |
let |
|
42361 | 365 |
val ctxt = Proof_Context.init_global thy |
40832 | 366 |
|> fold (Variable.declare_typ o TFree) sorts |
367 |
val T = Syntax.read_typ ctxt str |
|
368 |
in (T, Term.add_tfreesT T sorts) end |
|
33774 | 369 |
|
370 |
fun cert_typ sign raw_T sorts = |
|
371 |
let |
|
372 |
val T = Type.no_tvars (Sign.certify_typ sign raw_T) |
|
40832 | 373 |
handle TYPE (msg, _, _) => error msg |
374 |
val sorts' = Term.add_tfreesT T sorts |
|
33774 | 375 |
val _ = |
376 |
case duplicates (op =) (map fst sorts') of |
|
377 |
[] => () |
|
378 |
| dups => error ("Inconsistent sort constraints for " ^ commas dups) |
|
40832 | 379 |
in (T, sorts') end |
33774 | 380 |
|
381 |
fun gen_domain_isomorphism |
|
382 |
(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
|
383 |
(doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list) |
33774 | 384 |
(thy: theory) |
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
385 |
: (Domain_Take_Proofs.iso_info list |
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset
|
386 |
* Domain_Take_Proofs.take_induct_info) * theory = |
33774 | 387 |
let |
388 |
(* this theory is used just for parsing *) |
|
389 |
val tmp_thy = thy |> |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
390 |
Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) => |
40832 | 391 |
(tbind, length tvs, mx)) doms_raw) |
33774 | 392 |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
393 |
fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts = |
33774 | 394 |
let val (typ, sorts') = prep_typ thy typ_raw sorts |
40832 | 395 |
in ((vs, t, mx, typ, morphs), sorts') end |
33774 | 396 |
|
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
397 |
val (doms : (string list * binding * mixfix * typ * (binding * binding) option) list, |
33774 | 398 |
sorts : (string * sort) list) = |
40832 | 399 |
fold_map (prep_dom tmp_thy) doms_raw [] |
33774 | 400 |
|
40486 | 401 |
(* lookup function for sorts of type variables *) |
40832 | 402 |
fun the_sort v = the (AList.lookup (op =) sorts v) |
40486 | 403 |
|
40490
05be0c37db1d
add bifiniteness check for domain_isomorphism command
huffman
parents:
40489
diff
changeset
|
404 |
(* declare arities in temporary theory *) |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
405 |
val tmp_thy = |
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
406 |
let |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
407 |
fun arity (vs, tbind, _, _, _) = |
40832 | 408 |
(Sign.full_name thy tbind, map the_sort vs, @{sort "domain"}) |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
409 |
in |
56941
952833323c99
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
wenzelm
parents:
56249
diff
changeset
|
410 |
fold Axclass.arity_axiomatization (map arity doms) tmp_thy |
40832 | 411 |
end |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
412 |
|
40490
05be0c37db1d
add bifiniteness check for domain_isomorphism command
huffman
parents:
40489
diff
changeset
|
413 |
(* check bifiniteness of right-hand sides *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
414 |
fun check_rhs (_, _, _, rhs, _) = |
40497 | 415 |
if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then () |
416 |
else error ("Type not of sort domain: " ^ |
|
40832 | 417 |
quote (Syntax.string_of_typ_global tmp_thy rhs)) |
418 |
val _ = map check_rhs doms |
|
40490
05be0c37db1d
add bifiniteness check for domain_isomorphism command
huffman
parents:
40489
diff
changeset
|
419 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
420 |
(* domain equations *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
421 |
fun mk_dom_eqn (vs, tbind, _, rhs, _) = |
40832 | 422 |
let fun arg v = TFree (v, the_sort v) |
423 |
in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end |
|
424 |
val dom_eqns = map mk_dom_eqn doms |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
425 |
|
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
426 |
(* check for valid type parameters *) |
40832 | 427 |
val (tyvars, _, _, _, _) = hd doms |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
428 |
val _ = map (fn (tvs, tname, _, _, _) => |
33774 | 429 |
let val full_tname = Sign.full_name tmp_thy tname |
430 |
in |
|
431 |
(case duplicates (op =) tvs of |
|
432 |
[] => |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
433 |
if eq_set (op =) (tyvars, tvs) then (full_tname, tvs) |
33774 | 434 |
else error ("Mutually recursive domains must have same type parameters") |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42375
diff
changeset
|
435 |
| dups => error ("Duplicate parameter(s) for domain " ^ Binding.print tname ^ |
33774 | 436 |
" : " ^ commas dups)) |
40832 | 437 |
end) doms |
438 |
val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms |
|
439 |
val morphs = map (fn (_, _, _, _, morphs) => morphs) doms |
|
33774 | 440 |
|
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
441 |
(* determine deflation combinator arguments *) |
40832 | 442 |
val lhsTs : typ list = map fst dom_eqns |
443 |
val defl_rec = Free ("t", mk_tupleT (map (K deflT) lhsTs)) |
|
444 |
val defl_recs = mk_projs lhsTs defl_rec |
|
445 |
val defl_recs' = map (apsnd mk_u_defl) defl_recs |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
446 |
fun defl_body (_, _, _, rhsT, _) = |
40832 | 447 |
defl_of_typ tmp_thy defl_recs defl_recs' rhsT |
448 |
val functional = Term.lambda defl_rec (mk_tuple (map defl_body doms)) |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
449 |
|
40832 | 450 |
val tfrees = map fst (Term.add_tfrees functional []) |
451 |
val frees = map fst (Term.add_frees functional []) |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
452 |
fun get_defl_flags (vs, _, _, _, _) = |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
453 |
let |
40832 | 454 |
fun argT v = TFree (v, the_sort v) |
455 |
fun mk_d v = "d" ^ Library.unprefix "'" v |
|
456 |
fun mk_p v = "p" ^ Library.unprefix "'" v |
|
457 |
val args = maps (fn v => [(mk_d v, mk_DEFL (argT v)), (mk_p v, mk_LIFTDEFL (argT v))]) vs |
|
458 |
val typeTs = map argT (filter (member (op =) tfrees) vs) |
|
459 |
val defl_args = map snd (filter (member (op =) frees o fst) args) |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
460 |
in |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
461 |
(typeTs, defl_args) |
40832 | 462 |
end |
463 |
val defl_flagss = map get_defl_flags doms |
|
40218
f7d4d023a899
make domain package work with non-cpo argument types
huffman
parents:
40216
diff
changeset
|
464 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
465 |
(* declare deflation combinator constants *) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
466 |
fun declare_defl_const ((typeTs, defl_args), (_, tbind, _, _, _)) thy = |
33774 | 467 |
let |
40832 | 468 |
val defl_bind = Binding.suffix_name "_defl" tbind |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
469 |
val defl_type = |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
470 |
map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT |
33774 | 471 |
in |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
472 |
Sign.declare_const_global ((defl_bind, defl_type), NoSyn) thy |
40832 | 473 |
end |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
474 |
val (defl_consts, thy) = |
40832 | 475 |
fold_map declare_defl_const (defl_flagss ~~ doms) thy |
33774 | 476 |
|
33775
7a1518c42c56
cleaned up; factored out fixed-point definition code
huffman
parents:
33774
diff
changeset
|
477 |
(* defining equations for type combinators *) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
478 |
fun mk_defl_term (defl_const, (typeTs, defl_args)) = |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
479 |
let |
40832 | 480 |
val type_args = map Logic.mk_type typeTs |
40487
1320a0747974
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman
parents:
40486
diff
changeset
|
481 |
in |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
482 |
list_ccomb (list_comb (defl_const, type_args), defl_args) |
40832 | 483 |
end |
484 |
val defl_terms = map mk_defl_term (defl_consts ~~ defl_flagss) |
|
485 |
val defl_tab = map fst dom_eqns ~~ defl_terms |
|
486 |
val defl_tab' = map fst dom_eqns ~~ map mk_u_defl defl_terms |
|
33776 | 487 |
fun mk_defl_spec (lhsT, rhsT) = |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
488 |
mk_eqs (defl_of_typ tmp_thy defl_tab defl_tab' lhsT, |
40832 | 489 |
defl_of_typ tmp_thy defl_tab defl_tab' rhsT) |
490 |
val defl_specs = map mk_defl_spec dom_eqns |
|
33774 | 491 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33782
diff
changeset
|
492 |
(* register recursive definition of deflation combinators *) |
40832 | 493 |
val defl_binds = map (Binding.suffix_name "_defl") dbinds |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
494 |
val ((defl_apply_thms, defl_unfold_thms, defl_cont_thm), thy) = |
40832 | 495 |
add_fixdefs (defl_binds ~~ defl_specs) thy |
33774 | 496 |
|
33776 | 497 |
(* define types using deflation combinators *) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
498 |
fun make_repdef ((vs, tbind, mx, _, _), defl) thy = |
33774 | 499 |
let |
40832 | 500 |
val spec = (tbind, map (rpair dummyS) vs, mx) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
501 |
val ((_, _, _, {DEFL, ...}), thy) = |
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
46961
diff
changeset
|
502 |
Domaindef.add_domaindef spec defl NONE thy |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
503 |
(* declare domain_defl_simps rules *) |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
504 |
val thy = |
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
505 |
Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_defl_simps} DEFL) thy |
33774 | 506 |
in |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
507 |
(DEFL, thy) |
40832 | 508 |
end |
509 |
val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_terms) thy |
|
33776 | 510 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
511 |
(* prove DEFL equations *) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
512 |
fun mk_DEFL_eq_thm (lhsT, rhsT) = |
33776 | 513 |
let |
40832 | 514 |
val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT) |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
515 |
val DEFL_simps = |
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
516 |
Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps} |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
517 |
fun tac ctxt = |
57958 | 518 |
rewrite_goals_tac ctxt (map mk_meta_eq (rev DEFL_simps)) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
519 |
THEN TRY (resolve_tac ctxt defl_unfold_thms 1) |
33776 | 520 |
in |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
521 |
Goal.prove_global thy [] [] goal (tac o #context) |
40832 | 522 |
end |
523 |
val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns |
|
33782 | 524 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
525 |
(* register DEFL equations *) |
40832 | 526 |
val DEFL_eq_binds = map (Binding.prefix_name "DEFL_eq_") dbinds |
33782 | 527 |
val (_, thy) = thy |> |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
528 |
(Global_Theory.add_thms o map Thm.no_attributes) |
40832 | 529 |
(DEFL_eq_binds ~~ DEFL_eq_thms) |
33776 | 530 |
|
33778 | 531 |
(* define rep/abs functions *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
532 |
fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy = |
33778 | 533 |
let |
40832 | 534 |
val rep_bind = Binding.suffix_name "_rep" tbind |
535 |
val abs_bind = Binding.suffix_name "_abs" tbind |
|
35477 | 536 |
val ((rep_const, rep_def), thy) = |
40832 | 537 |
define_const (rep_bind, coerce_const (lhsT, rhsT)) thy |
35477 | 538 |
val ((abs_const, abs_def), thy) = |
40832 | 539 |
define_const (abs_bind, coerce_const (rhsT, lhsT)) thy |
33778 | 540 |
in |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
541 |
(((rep_const, abs_const), (rep_def, abs_def)), thy) |
40832 | 542 |
end |
33785
2f2d9eb37084
automate definition of map functions; remove unused code
huffman
parents:
33784
diff
changeset
|
543 |
val ((rep_abs_consts, rep_abs_defs), thy) = thy |
35773 | 544 |
|> fold_map mk_rep_abs (dbinds ~~ morphs ~~ dom_eqns) |
40832 | 545 |
|>> ListPair.unzip |
33782 | 546 |
|
547 |
(* prove isomorphism and isodefl rules *) |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
548 |
fun mk_iso_thms ((tbind, DEFL_eq), (rep_def, abs_def)) thy = |
33782 | 549 |
let |
35773 | 550 |
fun make thm = |
40832 | 551 |
Drule.zero_var_indexes (thm OF [DEFL_eq, abs_def, rep_def]) |
552 |
val rep_iso_thm = make @{thm domain_rep_iso} |
|
553 |
val abs_iso_thm = make @{thm domain_abs_iso} |
|
554 |
val isodefl_thm = make @{thm isodefl_abs_rep} |
|
35773 | 555 |
val thy = thy |
556 |
|> snd o add_qualified_thm "rep_iso" (tbind, rep_iso_thm) |
|
557 |
|> snd o add_qualified_thm "abs_iso" (tbind, abs_iso_thm) |
|
40832 | 558 |
|> snd o add_qualified_thm "isodefl_abs_rep" (tbind, isodefl_thm) |
33782 | 559 |
in |
560 |
(((rep_iso_thm, abs_iso_thm), isodefl_thm), thy) |
|
40832 | 561 |
end |
35489 | 562 |
val ((iso_thms, isodefl_abs_rep_thms), thy) = |
35480
7a1f285cad25
domain_isomorphism package proves deflation rules for map functions
huffman
parents:
35479
diff
changeset
|
563 |
thy |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
564 |
|> fold_map mk_iso_thms (dbinds ~~ DEFL_eq_thms ~~ rep_abs_defs) |
40832 | 565 |
|>> ListPair.unzip |
33778 | 566 |
|
35467
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
567 |
(* 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
|
568 |
val iso_infos : Domain_Take_Proofs.iso_info list = |
35467
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
569 |
let |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
570 |
fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) = |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
571 |
{ |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
572 |
repT = rhsT, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
573 |
absT = lhsT, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
574 |
rep_const = repC, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
575 |
abs_const = absC, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
576 |
rep_inverse = rep_iso, |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
577 |
abs_inverse = abs_iso |
40832 | 578 |
} |
35467
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
579 |
in |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
580 |
map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms) |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
581 |
end |
561d8e98d9d3
domain_isomorphism function returns iso_info record
huffman
parents:
35021
diff
changeset
|
582 |
|
35791
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
583 |
(* definitions and proofs related to map functions *) |
dc175fe29326
separate map-related code into new function define_map_functions
huffman
parents:
35773
diff
changeset
|
584 |
val (map_info, thy) = |
40832 | 585 |
define_map_functions (dbinds ~~ iso_infos) thy |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
586 |
val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info |
33788 | 587 |
|
588 |
(* prove isodefl rules for map functions *) |
|
589 |
val isodefl_thm = |
|
590 |
let |
|
40832 | 591 |
fun unprime a = Library.unprefix "'" a |
592 |
fun mk_d T = Free ("d" ^ unprime (fst (dest_TFree T)), deflT) |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
593 |
fun mk_p T = Free ("p" ^ unprime (fst (dest_TFree T)), udeflT) |
40832 | 594 |
fun mk_f T = Free ("f" ^ unprime (fst (dest_TFree T)), T ->> T) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
595 |
fun mk_assm t = |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
596 |
case try dest_LIFTDEFL t of |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41287
diff
changeset
|
597 |
SOME T => mk_trp (isodefl'_const T $ mk_f T $ mk_p T) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
598 |
| NONE => |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
599 |
let val T = dest_DEFL t |
40832 | 600 |
in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
601 |
fun mk_goal (map_const, (T, _)) = |
33788 | 602 |
let |
40832 | 603 |
val (_, Ts) = dest_Type T |
604 |
val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts)) |
|
605 |
val defl_term = defl_of_typ thy (Ts ~~ map mk_d Ts) (Ts ~~ map mk_p Ts) T |
|
606 |
in isodefl_const T $ map_term $ defl_term end |
|
607 |
val assms = (map mk_assm o snd o hd) defl_flagss |
|
608 |
val goals = map mk_goal (map_consts ~~ dom_eqns) |
|
609 |
val goal = mk_trp (foldr1 HOLogic.mk_conj goals) |
|
33788 | 610 |
val adm_rules = |
40832 | 611 |
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id} |
33788 | 612 |
val bottom_rules = |
40832 | 613 |
@{thms fst_strict snd_strict isodefl_bottom simp_thms} |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
614 |
val tuple_rules = |
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
615 |
@{thms split_def fst_conv snd_conv} |
40832 | 616 |
val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy |
617 |
val map_ID_simps = map (fn th => th RS sym) map_ID_thms |
|
33788 | 618 |
val isodefl_rules = |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40490
diff
changeset
|
619 |
@{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL} |
33791 | 620 |
@ isodefl_abs_rep_thms |
57958 | 621 |
@ rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl}) |
33845 | 622 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
623 |
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => |
33845 | 624 |
EVERY |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset
|
625 |
[rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms), |
41324
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
626 |
rtac (@{thm cont_parallel_fix_ind} |
1383653efec3
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents:
41292
diff
changeset
|
627 |
OF [defl_cont_thm, map_cont_thm]) 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
628 |
REPEAT (resolve_tac ctxt adm_rules 1), |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
629 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
630 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
631 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1, |
33788 | 632 |
REPEAT (etac @{thm conjE} 1), |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
633 |
REPEAT (resolve_tac ctxt (isodefl_rules @ prems) 1 ORELSE atac 1)]) |
40832 | 634 |
end |
635 |
val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
636 |
fun conjuncts [] _ = [] |
33789 | 637 |
| conjuncts (n::[]) thm = [(n, thm)] |
638 |
| conjuncts (n::ns) thm = let |
|
40832 | 639 |
val thmL = thm RS @{thm conjunct1} |
640 |
val thmR = thm RS @{thm conjunct2} |
|
641 |
in (n, thmL):: conjuncts ns thmR end |
|
33789 | 642 |
val (isodefl_thms, thy) = thy |> |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
37744
diff
changeset
|
643 |
(Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) |
40832 | 644 |
(conjuncts isodefl_binds isodefl_thm) |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
645 |
val thy = |
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
646 |
fold (Context.theory_map o Named_Theorems.add_thm @{named_theorems domain_isodefl}) |
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56941
diff
changeset
|
647 |
isodefl_thms thy |
33793 | 648 |
|
649 |
(* prove map_ID theorems *) |
|
650 |
fun prove_map_ID_thm |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
651 |
(((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) = |
33793 | 652 |
let |
40832 | 653 |
val Ts = snd (dest_Type lhsT) |
654 |
fun is_cpo T = Sign.of_sort thy (T, @{sort cpo}) |
|
655 |
val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts)) |
|
656 |
val goal = mk_eqs (lhs, mk_ID lhsT) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
657 |
fun tac ctxt = EVERY |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39974
diff
changeset
|
658 |
[rtac @{thm isodefl_DEFL_imp_ID} 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
659 |
stac ctxt DEFL_thm 1, |
33793 | 660 |
rtac isodefl_thm 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
661 |
REPEAT (resolve_tac ctxt @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)] |
33793 | 662 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58957
diff
changeset
|
663 |
Goal.prove_global thy [] [] goal (tac o #context) |
40832 | 664 |
end |
665 |
val map_ID_binds = map (Binding.suffix_name "_map_ID") dbinds |
|
33793 | 666 |
val map_ID_thms = |
667 |
map prove_map_ID_thm |
|
40832 | 668 |
(map_consts ~~ dom_eqns ~~ DEFL_thms ~~ isodefl_thms) |
33793 | 669 |
val (_, thy) = thy |> |
40489 | 670 |
(Global_Theory.add_thms o map (rpair [Domain_Take_Proofs.map_ID_add])) |
40832 | 671 |
(map_ID_binds ~~ map_ID_thms) |
33802
48ce3a1063f2
domain_isomorphism package defines copy functions
huffman
parents:
33801
diff
changeset
|
672 |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
673 |
(* 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
|
674 |
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
|
675 |
Domain_Take_Proofs.define_take_functions |
40832 | 676 |
(dbinds ~~ iso_infos) thy |
40015 | 677 |
val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} = |
40832 | 678 |
take_info |
33807
ce8d2e8bca21
domain_isomorphism package defines combined copy function
huffman
parents:
33802
diff
changeset
|
679 |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
680 |
(* 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
|
681 |
val lub_take_lemma = |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
682 |
let |
40832 | 683 |
val lhs = mk_tuple (map mk_lub take_consts) |
684 |
fun is_cpo T = Sign.of_sort thy (T, @{sort cpo}) |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
685 |
fun mk_map_ID (map_const, (lhsT, _)) = |
40832 | 686 |
list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT)))) |
687 |
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns)) |
|
688 |
val goal = mk_trp (mk_eq (lhs, rhs)) |
|
689 |
val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
690 |
val start_rules = |
40771 | 691 |
@{thms lub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
692 |
@ @{thms pair_collapse split_def} |
40832 | 693 |
@ map_apply_thms @ map_ID_thms |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
694 |
val rules0 = |
40832 | 695 |
@{thms iterate_0 Pair_strict} @ take_0_thms |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
696 |
val rules1 = |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42381
diff
changeset
|
697 |
@{thms iterate_Suc prod_eq_iff fst_conv snd_conv} |
40832 | 698 |
@ take_Suc_thms |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
699 |
fun tac ctxt = |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
700 |
EVERY |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
701 |
[simp_tac (put_simpset HOL_basic_ss ctxt addsimps start_rules) 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
702 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms fix_def2}) 1, |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
703 |
rtac @{thm lub_eq} 1, |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
704 |
rtac @{thm nat.induct} 1, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
705 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules0) 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
706 |
asm_full_simp_tac (put_simpset beta_ss ctxt addsimps rules1) 1] |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
707 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51685
diff
changeset
|
708 |
Goal.prove_global thy [] [] goal (tac o #context) |
40832 | 709 |
end |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
710 |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
711 |
(* prove lub of take equals ID *) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44066
diff
changeset
|
712 |
fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy = |
33809
033831fd9ef3
store map_ID thms in theory data; automate proofs of reach lemmas
huffman
parents:
33807
diff
changeset
|
713 |
let |
40832 | 714 |
val n = Free ("n", natT) |
715 |
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
|
716 |
val tac = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
717 |
EVERY |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
718 |
[rtac @{thm trans} 1, rtac map_ID_thm 2, |
46708
b138dee7bed3
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents:
45654
diff
changeset
|
719 |
cut_tac lub_take_lemma 1, |
40832 | 720 |
REPEAT (etac @{thm Pair_inject} 1), atac 1] |
721 |
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
|
722 |
in |
35773 | 723 |
add_qualified_thm "lub_take" (dbind, lub_take_thm) thy |
40832 | 724 |
end |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
725 |
val (lub_take_thms, thy) = |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35490
diff
changeset
|
726 |
fold_map prove_lub_take |
40832 | 727 |
(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
|
728 |
|
35654
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35640
diff
changeset
|
729 |
(* prove additional take theorems *) |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35640
diff
changeset
|
730 |
val (take_info2, thy) = |
7a15e181bf3b
move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents:
35640
diff
changeset
|
731 |
Domain_Take_Proofs.add_lub_take_theorems |
40832 | 732 |
(dbinds ~~ iso_infos) take_info lub_take_thms thy |
33774 | 733 |
in |
35659 | 734 |
((iso_infos, take_info2), thy) |
40832 | 735 |
end |
33774 | 736 |
|
40832 | 737 |
val domain_isomorphism = gen_domain_isomorphism cert_typ |
738 |
val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ |
|
33774 | 739 |
|
740 |
(******************************************************************************) |
|
741 |
(******************************** outer syntax ********************************) |
|
742 |
(******************************************************************************) |
|
743 |
||
744 |
local |
|
745 |
||
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
746 |
val parse_domain_iso : |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
747 |
(string list * binding * mixfix * string * (binding * binding) option) |
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
748 |
parser = |
46949 | 749 |
(Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- |
750 |
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))) |
|
40832 | 751 |
>> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)) |
33774 | 752 |
|
40832 | 753 |
val parse_domain_isos = Parse.and_list1 parse_domain_iso |
33774 | 754 |
|
755 |
in |
|
756 |
||
757 |
val _ = |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
758 |
Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)" |
40832 | 759 |
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd)) |
33774 | 760 |
|
40832 | 761 |
end |
33774 | 762 |
|
40832 | 763 |
end |