author  huffman 
Sun, 28 Feb 2010 20:56:28 0800  
changeset 35481  7bb9157507a9 
parent 35476  8e5eb497b042 
child 35482  d756837b708d 
permissions  rwrr 
35444  1 
(* Title: HOLCF/Tools/domain/domain_constructors.ML 
2 
Author: Brian Huffman 

3 

4 
Defines constructor functions for a given domain isomorphism 

5 
and proves related theorems. 

6 
*) 

7 

8 
signature DOMAIN_CONSTRUCTORS = 

9 
sig 

10 
val add_domain_constructors : 

11 
string 

35481
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

12 
> (binding * (bool * binding option * typ) list * mixfix) list 
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

13 
> Domain_Isomorphism.iso_info 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

14 
> thm 
35444  15 
> theory 
16 
> { con_consts : term list, 

35451  17 
con_betas : thm list, 
35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

18 
exhaust : thm, 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

19 
casedist : thm, 
35448
f9f73f0475eb
move proof of compactness rules into domain_constructors.ML
huffman
parents:
35447
diff
changeset

20 
con_compacts : thm list, 
35452
cf8c5a751a9a
move proof of con_rews into domain_constructor.ML
huffman
parents:
35451
diff
changeset

21 
con_rews : thm list, 
35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

22 
inverts : thm list, 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

23 
injects : thm list, 
35458
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

24 
dist_les : thm list, 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

25 
dist_eqs : thm list, 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

26 
cases : thm list, 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

27 
sel_rews : thm list, 
35462
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

28 
dis_rews : thm list, 
35468
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

29 
match_rews : thm list, 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

30 
pat_rews : thm list 
35453  31 
} * theory; 
35444  32 
end; 
33 

34 

35 
structure Domain_Constructors :> DOMAIN_CONSTRUCTORS = 

36 
struct 

37 

35475
979019ab92eb
move common functions into new file holcf_library.ML
huffman
parents:
35472
diff
changeset

38 
open HOLCF_Library; 
35476  39 
infixr 6 >>; 
40 
infix >>; 

35444  41 

35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

42 
(************************** miscellaneous functions ***************************) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

43 

35461
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

44 
val simple_ss = 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

45 
HOL_basic_ss addsimps simp_thms; 
35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

46 

35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

47 
val beta_ss = 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

48 
HOL_basic_ss 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

49 
addsimps simp_thms 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

50 
addsimps [@{thm beta_cfun}] 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

51 
addsimprocs [@{simproc cont_proc}]; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

52 

35444  53 
fun define_consts 
54 
(specs : (binding * term * mixfix) list) 

55 
(thy : theory) 

56 
: (term list * thm list) * theory = 

57 
let 

35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

58 
fun mk_decl (b, t, mx) = (b, fastype_of t, mx); 
35444  59 
val decls = map mk_decl specs; 
60 
val thy = Cont_Consts.add_consts decls thy; 

61 
fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T); 

62 
val consts = map mk_const decls; 

63 
fun mk_def c (b, t, mx) = 

64 
(Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); 

65 
val defs = map2 mk_def consts specs; 

66 
val (def_thms, thy) = 

67 
PureThy.add_defs false (map Thm.no_attributes defs) thy; 

68 
in 

69 
((consts, def_thms), thy) 

70 
end; 

71 

35449  72 
fun prove 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

73 
(thy : theory) 
35449  74 
(defs : thm list) 
35447  75 
(goal : term) 
35449  76 
(tacs : {prems: thm list, context: Proof.context} > tactic list) 
35447  77 
: thm = 
35449  78 
let 
79 
fun tac {prems, context} = 

80 
rewrite_goals_tac defs THEN 

81 
EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) 

82 
in 

83 
Goal.prove_global thy [] [] goal tac 

84 
end; 

35445  85 

86 
(************** generating beta reduction rules from definitions **************) 

35444  87 

35445  88 
local 
89 
fun arglist (Const _ $ Abs (s, T, t)) = 

90 
let 

91 
val arg = Free (s, T); 

92 
val (args, body) = arglist (subst_bound (arg, t)); 

93 
in (arg :: args, body) end 

94 
 arglist t = ([], t); 

95 
in 

96 
fun beta_of_def thy def_thm = 

97 
let 

98 
val (con, lam) = Logic.dest_equals (concl_of def_thm); 

99 
val (args, rhs) = arglist lam; 

35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

100 
val lhs = list_ccomb (con, args); 
35445  101 
val goal = mk_equals (lhs, rhs); 
102 
val cs = ContProc.cont_thms lam; 

103 
val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs; 

104 
in 

35449  105 
prove thy (def_thm::betas) goal (K [rtac reflexive_thm 1]) 
35445  106 
end; 
107 
end; 

35444  108 

35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

109 
(******************************************************************************) 
35453  110 
(************* definitions and theorems for constructor functions *************) 
111 
(******************************************************************************) 

112 

113 
fun add_constructors 

35454
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

114 
(spec : (binding * (bool * typ) list * mixfix) list) 
35453  115 
(abs_const : term) 
116 
(iso_locale : thm) 

117 
(thy : theory) 

118 
= 

119 
let 

120 

121 
(* get theorems about rep and abs *) 

122 
val abs_strict = iso_locale RS @{thm iso.abs_strict}; 

123 

35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

124 
(* get types of type isomorphism *) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

125 
val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

126 

35455  127 
fun vars_of args = 
128 
let 

129 
val Ts = map snd args; 

130 
val ns = Datatype_Prop.make_tnames Ts; 

131 
in 

132 
map Free (ns ~~ Ts) 

133 
end; 

134 

35453  135 
(* define constructor functions *) 
136 
val ((con_consts, con_defs), thy) = 

137 
let 

35454
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

138 
fun one_arg (lazy, T) var = if lazy then mk_up var else var; 
35453  139 
fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args)); 
140 
fun mk_abs t = abs_const ` t; 

141 
val rhss = map mk_abs (mk_sinjects (map one_con spec)); 

142 
fun mk_def (bind, args, mx) rhs = 

143 
(bind, big_lambdas (vars_of args) rhs, mx); 

144 
in 

145 
define_consts (map2 mk_def spec rhss) thy 

146 
end; 

147 

148 
(* prove beta reduction rules for constructors *) 

149 
val con_betas = map (beta_of_def thy) con_defs; 

150 

151 
(* replace bindings with terms in constructor spec *) 

152 
val spec' : (term * (bool * typ) list) list = 

35454
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

153 
let fun one_con con (b, args, mx) = (con, args); 
35453  154 
in map2 one_con con_consts spec end; 
155 

35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

156 
(* prove exhaustiveness of constructors *) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

157 
local 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

158 
fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo}))) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

159 
 arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo})); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

160 
fun args2typ n [] = (n, oneT) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

161 
 args2typ n [arg] = arg2typ n arg 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

162 
 args2typ n (arg::args) = 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

163 
let 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

164 
val (n1, t1) = arg2typ n arg; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

165 
val (n2, t2) = args2typ n1 args 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

166 
in (n2, mk_sprodT (t1, t2)) end; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

167 
fun cons2typ n [] = (n, oneT) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

168 
 cons2typ n [con] = args2typ n (snd con) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

169 
 cons2typ n (con::cons) = 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

170 
let 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

171 
val (n1, t1) = args2typ n (snd con); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

172 
val (n2, t2) = cons2typ n1 cons 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

173 
in (n2, mk_ssumT (t1, t2)) end; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

174 
val ct = ctyp_of thy (snd (cons2typ 1 spec')); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

175 
val thm1 = instantiate' [SOME ct] [] @{thm exh_start}; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

176 
val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

177 
val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

178 

d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

179 
val x = Free ("x", lhsT); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

180 
fun one_con (con, args) = 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

181 
let 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

182 
val Ts = map snd args; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

183 
val ns = Name.variant_list ["x"] (Datatype_Prop.make_tnames Ts); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

184 
val vs = map Free (ns ~~ Ts); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

185 
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

186 
val eqn = mk_eq (x, list_ccomb (con, vs)); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

187 
val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

188 
in Library.foldr mk_ex (vs, conj) end; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

189 
val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec')); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

190 
(* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

191 
val tacs = [ 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

192 
rtac (iso_locale RS @{thm iso.casedist_rule}) 1, 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

193 
rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})], 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

194 
rtac thm3 1]; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

195 
in 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

196 
val exhaust = prove thy con_betas goal (K tacs); 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

197 
val casedist = 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

198 
(exhaust RS @{thm exh_casedist0}) 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

199 
> rewrite_rule @{thms exh_casedists} 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

200 
> Drule.export_without_context; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

201 
end; 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

202 

35453  203 
(* prove compactness rules for constructors *) 
204 
val con_compacts = 

205 
let 

206 
val rules = @{thms compact_sinl compact_sinr compact_spair 

207 
compact_up compact_ONE}; 

208 
val tacs = 

209 
[rtac (iso_locale RS @{thm iso.compact_abs}) 1, 

210 
REPEAT (resolve_tac rules 1 ORELSE atac 1)]; 

211 
fun con_compact (con, args) = 

212 
let 

35455  213 
val vs = vars_of args; 
35453  214 
val con_app = list_ccomb (con, vs); 
215 
val concl = mk_trp (mk_compact con_app); 

216 
val assms = map (mk_trp o mk_compact) vs; 

217 
val goal = Logic.list_implies (assms, concl); 

218 
in 

219 
prove thy con_betas goal (K tacs) 

220 
end; 

221 
in 

222 
map con_compact spec' 

223 
end; 

224 

225 
(* prove strictness rules for constructors *) 

226 
local 

227 
fun con_strict (con, args) = 

228 
let 

229 
val rules = abs_strict :: @{thms con_strict_rules}; 

35455  230 
val vs = vars_of args; 
35453  231 
val nonlazy = map snd (filter_out fst (map fst args ~~ vs)); 
232 
fun one_strict v' = 

233 
let 

35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

234 
val UU = mk_bottom (fastype_of v'); 
35453  235 
val vs' = map (fn v => if v = v' then UU else v) vs; 
236 
val goal = mk_trp (mk_undef (list_ccomb (con, vs'))); 

237 
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; 

238 
in prove thy con_betas goal (K tacs) end; 

239 
in map one_strict nonlazy end; 

240 

241 
fun con_defin (con, args) = 

242 
let 

243 
fun iff_disj (t, []) = HOLogic.mk_not t 

244 
 iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts); 

35455  245 
val vs = vars_of args; 
35453  246 
val nonlazy = map snd (filter_out fst (map fst args ~~ vs)); 
247 
val lhs = mk_undef (list_ccomb (con, vs)); 

248 
val rhss = map mk_undef nonlazy; 

249 
val goal = mk_trp (iff_disj (lhs, rhss)); 

250 
val rule1 = iso_locale RS @{thm iso.abs_defined_iff}; 

251 
val rules = rule1 :: @{thms con_defined_iff_rules}; 

252 
val tacs = [simp_tac (HOL_ss addsimps rules) 1]; 

253 
in prove thy con_betas goal (K tacs) end; 

254 
in 

255 
val con_stricts = maps con_strict spec'; 

256 
val con_defins = map con_defin spec'; 

257 
val con_rews = con_stricts @ con_defins; 

258 
end; 

259 

35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

260 
(* prove injectiveness of constructors *) 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

261 
local 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

262 
fun pgterm rel (con, args) = 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

263 
let 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

264 
fun prime (Free (n, T)) = Free (n^"'", T) 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

265 
 prime t = t; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

266 
val xs = vars_of args; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

267 
val ys = map prime xs; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

268 
val nonlazy = map snd (filter_out (fst o fst) (args ~~ xs)); 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

269 
val lhs = rel (list_ccomb (con, xs), list_ccomb (con, ys)); 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

270 
val rhs = foldr1 mk_conj (ListPair.map rel (xs, ys)); 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

271 
val concl = mk_trp (mk_eq (lhs, rhs)); 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

272 
val zs = case args of [_] => []  _ => nonlazy; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

273 
val assms = map (mk_trp o mk_defined) zs; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

274 
val goal = Logic.list_implies (assms, concl); 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

275 
in prove thy con_betas goal end; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

276 
val cons' = filter (fn (_, args) => not (null args)) spec'; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

277 
in 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

278 
val inverts = 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

279 
let 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

280 
val abs_below = iso_locale RS @{thm iso.abs_below}; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

281 
val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

282 
val rules2 = @{thms up_defined spair_defined ONE_defined} 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

283 
val rules = rules1 @ rules2; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

284 
val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

285 
in map (fn c => pgterm mk_below c (K tacs)) cons' end; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

286 
val injects = 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

287 
let 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

288 
val abs_eq = iso_locale RS @{thm iso.abs_eq}; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

289 
val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

290 
val rules2 = @{thms up_defined spair_defined ONE_defined} 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

291 
val rules = rules1 @ rules2; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

292 
val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

293 
in map (fn c => pgterm mk_eq c (K tacs)) cons' end; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

294 
end; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

295 

35458
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

296 
(* prove distinctness of constructors *) 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

297 
local 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

298 
fun map_dist (f : 'a > 'a > 'b) (xs : 'a list) : 'b list = 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

299 
flat (map_index (fn (i, x) => map (f x) (nth_drop i xs)) xs); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

300 
fun prime (Free (n, T)) = Free (n^"'", T) 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

301 
 prime t = t; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

302 
fun iff_disj (t, []) = mk_not t 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

303 
 iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

304 
fun iff_disj2 (t, [], us) = mk_not t 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

305 
 iff_disj2 (t, ts, []) = mk_not t 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

306 
 iff_disj2 (t, ts, us) = 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

307 
mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

308 
fun dist_le (con1, args1) (con2, args2) = 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

309 
let 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

310 
val vs1 = vars_of args1; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

311 
val vs2 = map prime (vars_of args2); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

312 
val zs1 = map snd (filter_out (fst o fst) (args1 ~~ vs1)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

313 
val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

314 
val rhss = map mk_undef zs1; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

315 
val goal = mk_trp (iff_disj (lhs, rhss)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

316 
val rule1 = iso_locale RS @{thm iso.abs_below}; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

317 
val rules = rule1 :: @{thms con_below_iff_rules}; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

318 
val tacs = [simp_tac (HOL_ss addsimps rules) 1]; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

319 
in prove thy con_betas goal (K tacs) end; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

320 
fun dist_eq (con1, args1) (con2, args2) = 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

321 
let 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

322 
val vs1 = vars_of args1; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

323 
val vs2 = map prime (vars_of args2); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

324 
val zs1 = map snd (filter_out (fst o fst) (args1 ~~ vs1)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

325 
val zs2 = map snd (filter_out (fst o fst) (args2 ~~ vs2)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

326 
val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

327 
val rhss1 = map mk_undef zs1; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

328 
val rhss2 = map mk_undef zs2; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

329 
val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2)); 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

330 
val rule1 = iso_locale RS @{thm iso.abs_eq}; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

331 
val rules = rule1 :: @{thms con_eq_iff_rules}; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

332 
val tacs = [simp_tac (HOL_ss addsimps rules) 1]; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

333 
in prove thy con_betas goal (K tacs) end; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

334 
in 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

335 
val dist_les = map_dist dist_le spec'; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

336 
val dist_eqs = map_dist dist_eq spec'; 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

337 
end; 
35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

338 

35453  339 
val result = 
340 
{ 

341 
con_consts = con_consts, 

342 
con_betas = con_betas, 

35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

343 
exhaust = exhaust, 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

344 
casedist = casedist, 
35453  345 
con_compacts = con_compacts, 
35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

346 
con_rews = con_rews, 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

347 
inverts = inverts, 
35458
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

348 
injects = injects, 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

349 
dist_les = dist_les, 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

350 
dist_eqs = dist_eqs 
35453  351 
}; 
352 
in 

353 
(result, thy) 

354 
end; 

355 

356 
(******************************************************************************) 

35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

357 
(**************** definition and theorems for case combinator *****************) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

358 
(******************************************************************************) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

359 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

360 
fun add_case_combinator 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

361 
(spec : (term * (bool * typ) list) list) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

362 
(lhsT : typ) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

363 
(dname : string) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

364 
(case_def : thm) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

365 
(con_betas : thm list) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

366 
(casedist : thm) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

367 
(iso_locale : thm) 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

368 
(thy : theory) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

369 
: ((typ > term) * thm list) * theory = 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

370 
let 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

371 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

372 
(* prove rep/abs rules *) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

373 
val rep_strict = iso_locale RS @{thm iso.rep_strict}; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

374 
val abs_inverse = iso_locale RS @{thm iso.abs_iso}; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

375 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

376 
(* calculate function arguments of case combinator *) 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

377 
val resultT = TVar (("'t",0), @{sort pcpo}); 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

378 
fun fTs T = map (fn (_, args) => map snd args >> T) spec; 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

379 
val fns = Datatype_Prop.indexify_names (map (K "f") spec); 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

380 
val fs = map Free (fns ~~ fTs resultT); 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

381 
fun caseT T = fTs T >> (lhsT >> T); 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

382 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

383 
(* TODO: move definition of case combinator here *) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

384 
val case_bind = Binding.name (dname ^ "_when"); 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

385 
val case_name = Sign.full_name thy case_bind; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

386 
fun case_const T = Const (case_name, caseT T); 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

387 
val case_app = list_ccomb (case_const resultT, fs); 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

388 

35472
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

389 
(* define syntax for case combinator *) 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

390 
(* TODO: reimplement case syntax using a parse translation *) 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

391 
local 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

392 
open Syntax 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

393 
open Domain_Library 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

394 
fun syntax c = Syntax.mark_const (fst (dest_Const c)); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

395 
fun xconst c = Long_Name.base_name (fst (dest_Const c)); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

396 
fun c_ast authentic con = 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

397 
Constant (if authentic then syntax con else xconst con); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

398 
fun expvar n = Variable ("e" ^ string_of_int n); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

399 
fun argvar n m _ = Variable ("a" ^ string_of_int n ^ "_" ^ string_of_int m); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

400 
fun argvars n args = mapn (argvar n) 1 args; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

401 
fun app s (l, r) = mk_appl (Constant s) [l, r]; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

402 
val cabs = app "_cabs"; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

403 
val capp = app @{const_syntax Rep_CFun}; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

404 
val capps = Library.foldl capp 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

405 
fun con1 authentic n (con,args) = 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

406 
Library.foldl capp (c_ast authentic con, argvars n args); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

407 
fun case1 authentic n c = 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

408 
app "_case1" (con1 authentic n c, expvar n); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

409 
fun arg1 n (con,args) = List.foldr cabs (expvar n) (argvars n args); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

410 
fun when1 n m = if n = m then arg1 n else K (Constant @{const_syntax UU}); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

411 
val case_constant = Constant (syntax (case_const dummyT)); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

412 
fun case_trans authentic = 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

413 
ParsePrintRule 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

414 
(app "_case_syntax" 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

415 
(Variable "x", 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

416 
foldr1 (app "_case2") (mapn (case1 authentic) 1 spec)), 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

417 
capp (capps (case_constant, mapn arg1 1 spec), Variable "x")); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

418 
fun one_abscon_trans authentic n c = 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

419 
ParsePrintRule 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

420 
(cabs (con1 authentic n c, expvar n), 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

421 
capps (case_constant, mapn (when1 n) 1 spec)); 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

422 
fun abscon_trans authentic = 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

423 
mapn (one_abscon_trans authentic) 1 spec; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

424 
val trans_rules : ast Syntax.trrule list = 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

425 
case_trans false :: case_trans true :: 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

426 
abscon_trans false @ abscon_trans true; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

427 
in 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

428 
val thy = Sign.add_trrules_i trans_rules thy; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

429 
end; 
c23b42730b9b
move case combinator syntax to domain_constructors.ML
huffman
parents:
35470
diff
changeset

430 

35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

431 
(* prove beta reduction rule for case combinator *) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

432 
val case_beta = beta_of_def thy case_def; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

433 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

434 
(* prove strictness of case combinator *) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

435 
val case_strict = 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

436 
let 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

437 
val defs = [case_beta, mk_meta_eq rep_strict]; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

438 
val lhs = case_app ` mk_bottom lhsT; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

439 
val goal = mk_trp (mk_eq (lhs, mk_bottom resultT)); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

440 
val tacs = [resolve_tac @{thms sscase1 ssplit1 strictify1} 1]; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

441 
in prove thy defs goal (K tacs) end; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

442 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

443 
(* prove rewrites for case combinator *) 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

444 
local 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

445 
fun one_case (con, args) f = 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

446 
let 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

447 
val Ts = map snd args; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

448 
val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

449 
val vs = map Free (ns ~~ Ts); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

450 
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

451 
val assms = map (mk_trp o mk_defined) nonlazy; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

452 
val lhs = case_app ` list_ccomb (con, vs); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

453 
val rhs = list_ccomb (f, vs); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

454 
val concl = mk_trp (mk_eq (lhs, rhs)); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

455 
val goal = Logic.list_implies (assms, concl); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

456 
val defs = case_beta :: con_betas; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

457 
val rules1 = @{thms sscase2 sscase3 ssplit2 fup2 ID1}; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

458 
val rules2 = @{thms con_defined_iff_rules}; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

459 
val rules = abs_inverse :: rules1 @ rules2; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

460 
val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

461 
in prove thy defs goal (K tacs) end; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

462 
in 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

463 
val case_apps = map2 one_case spec fs; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

464 
end 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

465 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

466 
in 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

467 
((case_const, case_strict :: case_apps), thy) 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

468 
end 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

469 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

470 
(******************************************************************************) 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

471 
(************** definitions and theorems for selector functions ***************) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

472 
(******************************************************************************) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

473 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

474 
fun add_selectors 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

475 
(spec : (term * (bool * binding option * typ) list) list) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

476 
(rep_const : term) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

477 
(abs_inv : thm) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

478 
(rep_strict : thm) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

479 
(rep_strict_iff : thm) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

480 
(con_betas : thm list) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

481 
(thy : theory) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

482 
: thm list * theory = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

483 
let 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

484 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

485 
(* define selector functions *) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

486 
val ((sel_consts, sel_defs), thy) = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

487 
let 
35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

488 
fun rangeT s = snd (dest_cfunT (fastype_of s)); 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

489 
fun mk_outl s = mk_cfcomp (from_sinl (dest_ssumT (rangeT s)), s); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

490 
fun mk_outr s = mk_cfcomp (from_sinr (dest_ssumT (rangeT s)), s); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

491 
fun mk_sfst s = mk_cfcomp (sfst_const (dest_sprodT (rangeT s)), s); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

492 
fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

493 
fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

494 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

495 
fun sels_of_arg s (lazy, NONE, T) = [] 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

496 
 sels_of_arg s (lazy, SOME b, T) = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

497 
[(b, if lazy then mk_down s else s, NoSyn)]; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

498 
fun sels_of_args s [] = [] 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

499 
 sels_of_args s (v :: []) = sels_of_arg s v 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

500 
 sels_of_args s (v :: vs) = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

501 
sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

502 
fun sels_of_cons s [] = [] 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

503 
 sels_of_cons s ((con, args) :: []) = sels_of_args s args 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

504 
 sels_of_cons s ((con, args) :: cs) = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

505 
sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

506 
val sel_eqns : (binding * term * mixfix) list = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

507 
sels_of_cons rep_const spec; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

508 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

509 
define_consts sel_eqns thy 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

510 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

511 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

512 
(* replace bindings with terms in constructor spec *) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

513 
val spec2 : (term * (bool * term option * typ) list) list = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

514 
let 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

515 
fun prep_arg (lazy, NONE, T) sels = ((lazy, NONE, T), sels) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

516 
 prep_arg (lazy, SOME _, T) sels = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

517 
((lazy, SOME (hd sels), T), tl sels); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

518 
fun prep_con (con, args) sels = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

519 
apfst (pair con) (fold_map prep_arg args sels); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

520 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

521 
fst (fold_map prep_con spec sel_consts) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

522 
end; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

523 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

524 
(* prove selector strictness rules *) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

525 
val sel_stricts : thm list = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

526 
let 
35449  527 
val rules = rep_strict :: @{thms sel_strict_rules}; 
528 
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; 

35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

529 
fun sel_strict sel = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

530 
let 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

531 
val goal = mk_trp (mk_strict sel); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

532 
in 
35449  533 
prove thy sel_defs goal (K tacs) 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

534 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

535 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

536 
map sel_strict sel_consts 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

537 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

538 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

539 
(* prove selector application rules *) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

540 
val sel_apps : thm list = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

541 
let 
35449  542 
val defs = con_betas @ sel_defs; 
35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

543 
val rules = abs_inv :: @{thms sel_app_rules}; 
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

544 
val tacs = [asm_simp_tac (simple_ss addsimps rules) 1]; 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

545 
fun sel_apps_of (i, (con, args)) = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

546 
let 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

547 
val Ts : typ list = map #3 args; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

548 
val ns : string list = Datatype_Prop.make_tnames Ts; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

549 
val vs : term list = map Free (ns ~~ Ts); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

550 
val con_app : term = list_ccomb (con, vs); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

551 
val vs' : (bool * term) list = map #1 args ~~ vs; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

552 
fun one_same (n, sel, T) = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

553 
let 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

554 
val xs = map snd (filter_out fst (nth_drop n vs')); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

555 
val assms = map (mk_trp o mk_defined) xs; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

556 
val concl = mk_trp (mk_eq (sel ` con_app, nth vs n)); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

557 
val goal = Logic.list_implies (assms, concl); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

558 
in 
35449  559 
prove thy defs goal (K tacs) 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

560 
end; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

561 
fun one_diff (n, sel, T) = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

562 
let 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

563 
val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T)); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

564 
in 
35449  565 
prove thy defs goal (K tacs) 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

566 
end; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

567 
fun one_con (j, (_, args')) : thm list = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

568 
let 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

569 
fun prep (i, (lazy, NONE, T)) = NONE 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

570 
 prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

571 
val sels : (int * term * typ) list = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

572 
map_filter prep (map_index I args'); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

573 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

574 
if i = j 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

575 
then map one_same sels 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

576 
else map one_diff sels 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

577 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

578 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

579 
flat (map_index one_con spec2) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

580 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

581 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

582 
flat (map_index sel_apps_of spec2) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

583 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

584 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

585 
(* prove selector definedness rules *) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

586 
val sel_defins : thm list = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

587 
let 
35449  588 
val rules = rep_strict_iff :: @{thms sel_defined_iff_rules}; 
589 
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; 

35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

590 
fun sel_defin sel = 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

591 
let 
35456
5356534f880e
move proofs of injects and inverts to domain_constructors.ML
huffman
parents:
35455
diff
changeset

592 
val (T, U) = dest_cfunT (fastype_of sel); 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

593 
val x = Free ("x", T); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

594 
val lhs = mk_eq (sel ` x, mk_bottom U); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

595 
val rhs = mk_eq (x, mk_bottom T); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

596 
val goal = mk_trp (mk_eq (lhs, rhs)); 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

597 
in 
35449  598 
prove thy sel_defs goal (K tacs) 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

599 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

600 
fun one_arg (false, SOME sel, T) = SOME (sel_defin sel) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

601 
 one_arg _ = NONE; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

602 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

603 
case spec2 of 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

604 
[(con, args)] => map_filter one_arg args 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

605 
 _ => [] 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

606 
end; 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

607 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

608 
in 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

609 
(sel_stricts @ sel_defins @ sel_apps, thy) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

610 
end 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

611 

b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

612 
(******************************************************************************) 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

613 
(************ definitions and theorems for discriminator functions ************) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

614 
(******************************************************************************) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

615 

8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

616 
fun add_discriminators 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

617 
(bindings : binding list) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

618 
(spec : (term * (bool * typ) list) list) 
35461
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

619 
(lhsT : typ) 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

620 
(casedist : thm) 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

621 
(case_const : typ > term) 
35461
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

622 
(case_rews : thm list) 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

623 
(thy : theory) = 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

624 
let 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

625 

8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

626 
fun vars_of args = 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

627 
let 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

628 
val Ts = map snd args; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

629 
val ns = Datatype_Prop.make_tnames Ts; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

630 
in 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

631 
map Free (ns ~~ Ts) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

632 
end; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

633 

8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

634 
(* define discriminator functions *) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

635 
local 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

636 
fun dis_fun i (j, (con, args)) = 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

637 
let 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

638 
val Ts = map snd args; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

639 
val ns = Datatype_Prop.make_tnames Ts; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

640 
val vs = map Free (ns ~~ Ts); 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

641 
val tr = if i = j then @{term TT} else @{term FF}; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

642 
in 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

643 
big_lambdas vs tr 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

644 
end; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

645 
fun dis_eqn (i, bind) : binding * term * mixfix = 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

646 
let 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

647 
val dis_bind = Binding.prefix_name "is_" bind; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

648 
val rhs = list_ccomb (case_const trT, map_index (dis_fun i) spec); 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

649 
in 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

650 
(dis_bind, rhs, NoSyn) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

651 
end; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

652 
in 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

653 
val ((dis_consts, dis_defs), thy) = 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

654 
define_consts (map_index dis_eqn bindings) thy 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

655 
end; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

656 

35461
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

657 
(* prove discriminator strictness rules *) 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

658 
local 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

659 
fun dis_strict dis = 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

660 
let val goal = mk_trp (mk_strict dis); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

661 
in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

662 
in 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

663 
val dis_stricts = map dis_strict dis_consts; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

664 
end; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

665 

34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

666 
(* prove discriminator/constructor rules *) 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

667 
local 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

668 
fun dis_app (i, dis) (j, (con, args)) = 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

669 
let 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

670 
val Ts = map snd args; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

671 
val ns = Datatype_Prop.make_tnames Ts; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

672 
val vs = map Free (ns ~~ Ts); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

673 
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

674 
val lhs = dis ` list_ccomb (con, vs); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

675 
val rhs = if i = j then @{term TT} else @{term FF}; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

676 
val assms = map (mk_trp o mk_defined) nonlazy; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

677 
val concl = mk_trp (mk_eq (lhs, rhs)); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

678 
val goal = Logic.list_implies (assms, concl); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

679 
val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

680 
in prove thy dis_defs goal (K tacs) end; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

681 
fun one_dis (i, dis) = 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

682 
map_index (dis_app (i, dis)) spec; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

683 
in 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

684 
val dis_apps = flat (map_index one_dis dis_consts); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

685 
end; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

686 

34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

687 
(* prove discriminator definedness rules *) 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

688 
local 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

689 
fun dis_defin dis = 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

690 
let 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

691 
val x = Free ("x", lhsT); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

692 
val simps = dis_apps @ @{thms dist_eq_tr}; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

693 
val tacs = 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

694 
[rtac @{thm iffI} 1, 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

695 
asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2, 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

696 
rtac casedist 1, atac 1, 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

697 
DETERM_UNTIL_SOLVED (CHANGED 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

698 
(asm_full_simp_tac (simple_ss addsimps simps) 1))]; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

699 
val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)); 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

700 
in prove thy [] goal (K tacs) end; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

701 
in 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

702 
val dis_defins = map dis_defin dis_consts; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

703 
end; 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

704 

35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

705 
in 
35461
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

706 
(dis_stricts @ dis_defins @ dis_apps, thy) 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

707 
end; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

708 

8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

709 
(******************************************************************************) 
35462
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

710 
(*************** definitions and theorems for match combinators ***************) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

711 
(******************************************************************************) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

712 

f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

713 
fun add_match_combinators 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

714 
(bindings : binding list) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

715 
(spec : (term * (bool * typ) list) list) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

716 
(lhsT : typ) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

717 
(casedist : thm) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

718 
(case_const : typ > term) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

719 
(case_rews : thm list) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

720 
(thy : theory) = 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

721 
let 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

722 

f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

723 
(* get a fresh type variable for the result type *) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

724 
val resultT : typ = 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

725 
let 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

726 
val ts : string list = map (fst o dest_TFree) (snd (dest_Type lhsT)); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

727 
val t : string = Name.variant ts "'t"; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

728 
in TFree (t, @{sort pcpo}) end; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

729 

f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

730 
(* define match combinators *) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

731 
local 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

732 
val x = Free ("x", lhsT); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

733 
fun k args = Free ("k", map snd args >> mk_matchT resultT); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

734 
val fail = mk_fail resultT; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

735 
fun mat_fun i (j, (con, args)) = 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

736 
let 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

737 
val Ts = map snd args; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

738 
val ns = Name.variant_list ["x","k"] (Datatype_Prop.make_tnames Ts); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

739 
val vs = map Free (ns ~~ Ts); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

740 
in 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

741 
if i = j then k args else big_lambdas vs fail 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

742 
end; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

743 
fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix = 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

744 
let 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

745 
val mat_bind = Binding.prefix_name "match_" bind; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

746 
val funs = map_index (mat_fun i) spec 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

747 
val body = list_ccomb (case_const (mk_matchT resultT), funs); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

748 
val rhs = big_lambda x (big_lambda (k args) (body ` x)); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

749 
in 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

750 
(mat_bind, rhs, NoSyn) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

751 
end; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

752 
in 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

753 
val ((match_consts, match_defs), thy) = 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

754 
define_consts (map_index mat_eqn (bindings ~~ spec)) thy 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

755 
end; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

756 

35463
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

757 
(* register match combinators with fixrec package *) 
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

758 
local 
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

759 
val con_names = map (fst o dest_Const o fst) spec; 
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

760 
val mat_names = map (fst o dest_Const) match_consts; 
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

761 
in 
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

762 
val thy = Fixrec.add_matchers (con_names ~~ mat_names) thy; 
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

763 
end; 
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

764 

35466
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

765 
(* prove strictness of match combinators *) 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

766 
local 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

767 
fun match_strict mat = 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

768 
let 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

769 
val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

770 
val k = Free ("k", U); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

771 
val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V)); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

772 
val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

773 
in prove thy match_defs goal (K tacs) end; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

774 
in 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

775 
val match_stricts = map match_strict match_consts; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

776 
end; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

777 

9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

778 
(* prove match/constructor rules *) 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

779 
local 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

780 
val fail = mk_fail resultT; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

781 
fun match_app (i, mat) (j, (con, args)) = 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

782 
let 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

783 
val Ts = map snd args; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

784 
val ns = Name.variant_list ["k"] (Datatype_Prop.make_tnames Ts); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

785 
val vs = map Free (ns ~~ Ts); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

786 
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

787 
val (_, (kT, _)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat)); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

788 
val k = Free ("k", kT); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

789 
val lhs = mat ` list_ccomb (con, vs) ` k; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

790 
val rhs = if i = j then list_ccomb (k, vs) else fail; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

791 
val assms = map (mk_trp o mk_defined) nonlazy; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

792 
val concl = mk_trp (mk_eq (lhs, rhs)); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

793 
val goal = Logic.list_implies (assms, concl); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

794 
val tacs = [asm_simp_tac (beta_ss addsimps case_rews) 1]; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

795 
in prove thy match_defs goal (K tacs) end; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

796 
fun one_match (i, mat) = 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

797 
map_index (match_app (i, mat)) spec; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

798 
in 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

799 
val match_apps = flat (map_index one_match match_consts); 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

800 
end; 
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35463
diff
changeset

801 

35462
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

802 
in 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

803 
(match_stricts @ match_apps, thy) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

804 
end; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

805 

f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

806 
(******************************************************************************) 
35468
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

807 
(************** definitions and theorems for pattern combinators **************) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

808 
(******************************************************************************) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

809 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

810 
fun add_pattern_combinators 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

811 
(bindings : binding list) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

812 
(spec : (term * (bool * typ) list) list) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

813 
(lhsT : typ) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

814 
(casedist : thm) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

815 
(case_const : typ > term) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

816 
(case_rews : thm list) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

817 
(thy : theory) = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

818 
let 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

819 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

820 
(* define pattern combinators *) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

821 
local 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

822 
fun mk_pair_pat (p1, p2) = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

823 
let 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

824 
val T1 = fastype_of p1; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

825 
val T2 = fastype_of p2; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

826 
val (U1, V1) = apsnd dest_matchT (dest_cfunT T1); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

827 
val (U2, V2) = apsnd dest_matchT (dest_cfunT T2); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

828 
val pat_typ = [T1, T2] > 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

829 
(mk_prodT (U1, U2) >> mk_matchT (mk_prodT (V1, V2))); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

830 
val pat_const = Const (@{const_name cpair_pat}, pat_typ); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

831 
in 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

832 
pat_const $ p1 $ p2 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

833 
end; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

834 
fun mk_tuple_pat [] = return_const HOLogic.unitT 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

835 
 mk_tuple_pat ps = foldr1 mk_pair_pat ps; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

836 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

837 
val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

838 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

839 
fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

840 
let 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

841 
val pat_bind = Binding.suffix_name "_pat" bind; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

842 
val Ts = map snd args; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

843 
val Vs = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

844 
(map (K "t") args) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

845 
> Datatype_Prop.indexify_names 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

846 
> Name.variant_list tns 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

847 
> map (fn t => TFree (t, @{sort pcpo})); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

848 
val patNs = Datatype_Prop.indexify_names (map (K "pat") args); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

849 
val patTs = map2 (fn T => fn V => T >> mk_matchT V) Ts Vs; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

850 
val pats = map Free (patNs ~~ patTs); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

851 
val fail = mk_fail (mk_tupleT Vs); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

852 
val ns = Name.variant_list patNs (Datatype_Prop.make_tnames Ts); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

853 
val vs = map Free (ns ~~ Ts); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

854 
val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

855 
fun one_fun (j, (_, args')) = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

856 
let 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

857 
val Ts = map snd args'; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

858 
val ns = Name.variant_list patNs (Datatype_Prop.make_tnames Ts); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

859 
val vs' = map Free (ns ~~ Ts); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

860 
in if i = j then rhs else big_lambdas vs' fail end; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

861 
val funs = map_index one_fun spec; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

862 
val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

863 
in 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

864 
(pat_bind, lambdas pats body, NoSyn) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

865 
end; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

866 
in 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

867 
val ((pat_consts, pat_defs), thy) = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

868 
define_consts (map_index pat_eqn (bindings ~~ spec)) thy 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

869 
end; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

870 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

871 
(* syntax translations for pattern combinators *) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

872 
local 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

873 
open Syntax 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

874 
fun syntax c = Syntax.mark_const (fst (dest_Const c)); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

875 
fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r]; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

876 
val capp = app @{const_syntax Rep_CFun}; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

877 
val capps = Library.foldl capp 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

878 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

879 
fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"]; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

880 
fun app_pat x = Syntax.mk_appl (Constant "_pat") [x]; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

881 
fun args_list [] = Constant "_noargs" 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

882 
 args_list xs = foldr1 (app "_args") xs; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

883 
fun one_case_trans (pat, (con, args)) = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

884 
let 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

885 
val cname = Constant (syntax con); 
35470  886 
val pname = Constant (syntax pat); 
35468
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

887 
val ns = 1 upto length args; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

888 
val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

889 
val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

890 
val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

891 
in 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

892 
[ParseRule (app_pat (capps (cname, xs)), 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

893 
mk_appl pname (map app_pat xs)), 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

894 
ParseRule (app_var (capps (cname, xs)), 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

895 
app_var (args_list xs)), 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

896 
PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)), 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

897 
app "_match" (mk_appl pname ps, args_list vs))] 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

898 
end; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

899 
val trans_rules : Syntax.ast Syntax.trrule list = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

900 
maps one_case_trans (pat_consts ~~ spec); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

901 
in 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

902 
val thy = Sign.add_trrules_i trans_rules thy; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

903 
end; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

904 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

905 
in 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

906 
(pat_defs, thy) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

907 
end 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

908 

09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

909 
(******************************************************************************) 
35450
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

910 
(******************************* main function ********************************) 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

911 
(******************************************************************************) 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

912 

e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

913 
fun add_domain_constructors 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

914 
(dname : string) 
35481
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

915 
(spec : (binding * (bool * binding option * typ) list * mixfix) list) 
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

916 
(iso_info : Domain_Isomorphism.iso_info) 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

917 
(case_def : thm) 
35450
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

918 
(thy : theory) = 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

919 
let 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

920 

35481
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

921 
(* retrieve facts about rep/abs *) 
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

922 
val lhsT = #absT iso_info; 
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

923 
val {rep_const, abs_const, ...} = iso_info; 
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

924 
val abs_iso_thm = #abs_inverse iso_info; 
7bb9157507a9
add_domain_constructors takes iso_info record as argument
huffman
parents:
35476
diff
changeset

925 
val rep_iso_thm = #rep_inverse iso_info; 
35450
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

926 
val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm]; 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

927 
val rep_strict = iso_locale RS @{thm iso.rep_strict}; 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

928 
val abs_strict = iso_locale RS @{thm iso.abs_strict}; 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

929 
val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff}; 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

930 
val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff}; 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

931 

e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

932 
(* define constructor functions *) 
35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

933 
val (con_result, thy) = 
35454
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

934 
let 
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

935 
fun prep_arg (lazy, sel, T) = (lazy, T); 
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

936 
fun prep_con (b, args, mx) = (b, map prep_arg args, mx); 
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

937 
val con_spec = map prep_con spec; 
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

938 
in 
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

939 
add_constructors con_spec abs_const iso_locale thy 
cf6ba350b7ca
remove unnecessary stuff from argument to add_constructors function
huffman
parents:
35453
diff
changeset

940 
end; 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

941 
val {con_consts, con_betas, casedist, ...} = con_result; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

942 

3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

943 
(* define case combinator *) 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

944 
val ((case_const : typ > term, cases : thm list), thy) = 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

945 
let 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

946 
fun prep_arg (lazy, sel, T) = (lazy, T); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

947 
fun prep_con c (b, args, mx) = (c, map prep_arg args); 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

948 
val case_spec = map2 prep_con con_consts spec; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

949 
in 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

950 
add_case_combinator case_spec lhsT dname 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

951 
case_def con_betas casedist iso_locale thy 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

952 
end; 
35450
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

953 

35463
b20501588930
register match functions from domain_constructors.ML
huffman
parents:
35462
diff
changeset

954 
(* qualify constants and theorems with domain name *) 
35450
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

955 
(* TODO: enable this earlier *) 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

956 
val thy = Sign.add_path dname thy; 
e9ef2b50ac59
move constructorspecific stuff to a separate function
huffman
parents:
35449
diff
changeset

957 

35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

958 
(* define and prove theorems for selector functions *) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

959 
val (sel_thms : thm list, thy : theory) = 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

960 
let 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

961 
val sel_spec : (term * (bool * binding option * typ) list) list = 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

962 
map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

963 
in 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

964 
add_selectors sel_spec rep_const 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

965 
abs_iso_thm rep_strict rep_defined_iff con_betas thy 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

966 
end; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

967 

8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

968 
(* define and prove theorems for discriminator functions *) 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

969 
val (dis_thms : thm list, thy : theory) = 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

970 
let 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

971 
val bindings = map #1 spec; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

972 
fun prep_arg (lazy, sel, T) = (lazy, T); 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

973 
fun prep_con c (b, args, mx) = (c, map prep_arg args); 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

974 
val dis_spec = map2 prep_con con_consts spec; 
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

975 
in 
35461
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

976 
add_discriminators bindings dis_spec lhsT 
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

977 
casedist case_const cases thy 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

978 
end 
35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

979 

35462
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

980 
(* define and prove theorems for match combinators *) 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

981 
val (match_thms : thm list, thy : theory) = 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

982 
let 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

983 
val bindings = map #1 spec; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

984 
fun prep_arg (lazy, sel, T) = (lazy, T); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

985 
fun prep_con c (b, args, mx) = (c, map prep_arg args); 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

986 
val mat_spec = map2 prep_con con_consts spec; 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

987 
in 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

988 
add_match_combinators bindings mat_spec lhsT 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

989 
casedist case_const cases thy 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

990 
end 
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

991 

35468
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

992 
(* define and prove theorems for pattern combinators *) 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

993 
val (pat_thms : thm list, thy : theory) = 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

994 
let 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

995 
val bindings = map #1 spec; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

996 
fun prep_arg (lazy, sel, T) = (lazy, T); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

997 
fun prep_con c (b, args, mx) = (c, map prep_arg args); 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

998 
val pat_spec = map2 prep_con con_consts spec; 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

999 
in 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

1000 
add_pattern_combinators bindings pat_spec lhsT 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

1001 
casedist case_const cases thy 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

1002 
end 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

1003 

35446
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

1004 
(* restore original signature path *) 
b719dad322fa
rewrite domain package code for selector functions
huffman
parents:
35445
diff
changeset

1005 
val thy = Sign.parent_path thy; 
35444  1006 

1007 
val result = 

1008 
{ con_consts = con_consts, 

35451  1009 
con_betas = con_betas, 
35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

1010 
exhaust = #exhaust con_result, 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

1011 
casedist = casedist, 
35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

1012 
con_compacts = #con_compacts con_result, 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

1013 
con_rews = #con_rews con_result, 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

1014 
inverts = #inverts con_result, 
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

1015 
injects = #injects con_result, 
35458
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

1016 
dist_les = #dist_les con_result, 
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

1017 
dist_eqs = #dist_eqs con_result, 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

1018 
cases = cases, 
35460
8cb42aa19358
move definition of discriminators to domain_constructors.ML
huffman
parents:
35459
diff
changeset

1019 
sel_rews = sel_thms, 
35462
f5461b02d754
move definition of match combinators to domain_constructors.ML
huffman
parents:
35461
diff
changeset

1020 
dis_rews = dis_thms, 
35468
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

1021 
match_rews = match_thms, 
09bc6a2e2296
move definition and syntax of pattern combinators into domain_constructors.ML
huffman
parents:
35466
diff
changeset

1022 
pat_rews = pat_thms }; 
35444  1023 
in 
1024 
(result, thy) 

1025 
end; 

1026 

1027 
end; 