author  huffman 
Fri, 22 May 2009 13:18:59 0700  
changeset 31232  689aa7da48cc 
parent 31227  0aa6afd229d3 
child 31288  67dff9c5b2bd 
permissions  rwrr 
23152  1 
(* Title: HOLCF/Tools/domain/domain_axioms.ML 
2 
Author: David von Oheimb 

3 

4 
Syntax generator for domain command. 

5 
*) 

6 

30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

7 
signature DOMAIN_AXIOMS = 
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

8 
sig 
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

9 
val copy_of_dtyp : (int > term) > DatatypeAux.dtyp > term 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

10 

31227  11 
val calc_axioms : 
12 
string > Domain_Library.eq list > int > Domain_Library.eq > 

13 
string * (string * term) list * (string * term) list 

14 

15 
val add_axioms : 

16 
bstring > Domain_Library.eq list > theory > theory 

30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

17 
end; 
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

18 

dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

19 

31023  20 
structure Domain_Axioms :> DOMAIN_AXIOMS = 
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30912
diff
changeset

21 
struct 
23152  22 

31227  23 
open Domain_Library; 
23152  24 

25 
infixr 0 ===>;infixr 0 ==>;infix 0 == ; 

26 
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; 

27 
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; 

28 

31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

29 
(* FIXME: use theory data for this *) 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

30 
val copy_tab : string Symtab.table = 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

31 
Symtab.make [(@{type_name ">"}, @{const_name "cfun_fun"}), 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

32 
(@{type_name "++"}, @{const_name "ssum_fun"}), 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

33 
(@{type_name "**"}, @{const_name "sprod_fun"}), 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

34 
(@{type_name "*"}, @{const_name "cprod_fun"}), 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

35 
(@{type_name "u"}, @{const_name "u_fun"})]; 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

36 

689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

37 
fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

38 
and copy r (DatatypeAux.DtRec i) = r i 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

39 
 copy r (DatatypeAux.DtTFree a) = ID 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

40 
 copy r (DatatypeAux.DtType (c, ds)) = 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

41 
case Symtab.lookup copy_tab c of 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

42 
SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds) 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

43 
 NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

44 

31227  45 
fun calc_axioms 
46 
(comp_dname : string) 

47 
(eqs : eq list) 

48 
(n : int) 

31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

49 
(eqn as ((dname,_),cons) : eq) 
31227  50 
: string * (string * term) list * (string * term) list = 
51 
let 

23152  52 

31227  53 
(*  axioms and definitions concerning the isomorphism  *) 
23152  54 

31227  55 
val dc_abs = %%:(dname^"_abs"); 
56 
val dc_rep = %%:(dname^"_rep"); 

57 
val x_name'= "x"; 

58 
val x_name = idx_name eqs x_name' (n+1); 

59 
val dnam = Long_Name.base_name dname; 

60 

61 
val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); 

62 
val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); 

23152  63 

31227  64 
val when_def = ("when_def",%%:(dname^"_when") == 
65 
List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => 

66 
Bound(1+length cons+xy)))`(dc_rep`Bound 0))) (when_funs cons)); 

67 

31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

68 
val copy_def = 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

69 
let fun r i = cproj (Bound 0) eqs i; 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

70 
in ("copy_def", %%:(dname^"_copy") == 
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31227
diff
changeset

71 
/\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end; 
23152  72 

31227  73 
(*  definitions concerning the constructors, discriminators and selectors  *) 
23152  74 

31227  75 
fun con_def m n (_,args) = let 
76 
fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(zx)); 

77 
fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); 

78 
fun inj y 1 _ = y 

79 
 inj y _ 0 = mk_sinl y 

80 
 inj y i j = mk_sinr (inj y (i1) (j1)); 

81 
in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; 

82 

83 
val con_defs = mapn (fn n => fn (con,args) => 

84 
(extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; 

85 

86 
val dis_defs = let 

87 
fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 

88 
list_ccomb(%%:(dname^"_when"),map 

89 
(fn (con',args) => (List.foldr /\# 

26012  90 
(if con'=con then TT else FF) args)) cons)) 
23152  91 
in map ddef cons end; 
92 

31227  93 
val mat_defs = 
94 
let 

95 
fun mdef (con,_) = 

96 
let 

97 
val k = Bound 0 

98 
val x = Bound 1 

99 
fun one_con (con', args') = 

100 
if con'=con then k else List.foldr /\# mk_fail args' 

101 
val w = list_ccomb(%%:(dname^"_when"), map one_con cons) 

102 
val rhs = /\ "x" (/\ "k" (w ` x)) 

103 
in (mat_name con ^"_def", %%:(mat_name con) == rhs) end 

104 
in map mdef cons end; 

23152  105 

31227  106 
val pat_defs = 
107 
let 

108 
fun pdef (con,args) = 

109 
let 

110 
val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; 

111 
val xs = map (bound_arg args) args; 

112 
val r = Bound (length args); 

113 
val rhs = case args of [] => mk_return HOLogic.unit 

114 
 _ => mk_ctuple_pat ps ` mk_ctuple xs; 

115 
fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; 

116 
in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 

117 
list_ccomb(%%:(dname^"_when"), map one_con cons)) 

118 
end 

119 
in map pdef cons end; 

23152  120 

31227  121 
val sel_defs = let 
122 
fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 

123 
list_ccomb(%%:(dname^"_when"),map 

124 
(fn (con',args) => if con'<>con then UU else 

125 
List.foldr /\# (Bound (length args  n)) args) cons))) (sel_of arg); 

23152  126 
in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; 
127 

128 

31227  129 
(*  axiom and definitions concerning induction  *) 
23152  130 

31227  131 
val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n 
132 
`%x_name === %:x_name)); 

133 
val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj 

134 
(mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); 

135 
val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name, 

136 
mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); 

23152  137 

31227  138 
in (dnam, 
139 
[abs_iso_ax, rep_iso_ax, reach_ax], 

140 
[when_def, copy_def] @ 

141 
con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ 

142 
[take_def, finite_def]) 

143 
end; (* let (calc_axioms) *) 

23152  144 

30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

145 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

146 
(* legacy type inference *) 
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

147 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

148 
fun legacy_infer_term thy t = 
31227  149 
singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); 
30483
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

150 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

151 
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); 
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

152 

0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

153 
fun infer_props thy = map (apsnd (legacy_infer_prop thy)); 
0c398040969c
added legacy type inference (from fixrec_package.ML);
wenzelm
parents:
30364
diff
changeset

154 

23152  155 

29585  156 
fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x); 
23152  157 
fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; 
158 

29585  159 
fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); 
23152  160 
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; 
161 

30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

162 
fun add_matchers (((dname,_),cons) : eq) thy = 
31227  163 
let 
164 
val con_names = map fst cons; 

165 
val mat_names = map mat_name con_names; 

166 
fun qualify n = Sign.full_name thy (Binding.name n); 

167 
val ms = map qualify con_names ~~ map qualify mat_names; 

168 
in FixrecPackage.add_matchers ms thy end; 

23152  169 

31227  170 
fun add_axioms comp_dnam (eqs : eq list) thy' = 
23152  171 
let 
31227  172 
val comp_dname = Sign.full_bname thy' comp_dnam; 
173 
val dnames = map (fst o fst) eqs; 

174 
val x_name = idx_name dnames "x"; 

175 
fun copy_app dname = %%:(dname^"_copy")`Bound 0; 

176 
val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == 

177 
/\ "f"(mk_ctuple (map copy_app dnames))); 

23152  178 

31227  179 
fun one_con (con,args) = let 
180 
val nonrec_args = filter_out is_rec args; 

181 
val rec_args = List.filter is_rec args; 

182 
val recs_cnt = length rec_args; 

183 
val allargs = nonrec_args @ rec_args 

184 
@ map (upd_vname (fn s=> s^"'")) rec_args; 

185 
val allvns = map vname allargs; 

186 
fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; 

187 
val vns1 = map (vname_arg "" ) args; 

188 
val vns2 = map (vname_arg "'") args; 

189 
val allargs_cnt = length nonrec_args + 2*recs_cnt; 

190 
val rec_idxs = (recs_cnt1) downto 0; 

191 
val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) 

192 
(allargs~~((allargs_cnt1) downto 0))); 

193 
fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 

194 
Bound (2*recs_cnti) $ Bound (recs_cnti); 

195 
val capps = 

196 
List.foldr mk_conj 

197 
(mk_conj( 

198 
Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), 

199 
Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) 

200 
(mapn rel_app 1 rec_args); 

201 
in List.foldr mk_ex 

202 
(Library.foldr mk_conj 

203 
(map (defined o Bound) nonlazy_idxs,capps)) allvns 

204 
end; 

205 
fun one_comp n (_,cons) = 

206 
mk_all(x_name(n+1), 

207 
mk_all(x_name(n+1)^"'", 

208 
mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0, 

209 
foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) 

210 
::map one_con cons)))); 

211 
val bisim_def = 

212 
("bisim_def", 

213 
%%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); 

214 

215 
fun add_one (thy,(dnam,axs,dfs)) = 

216 
thy > Sign.add_path dnam 

217 
> add_defs_infer dfs 

218 
> add_axioms_infer axs 

219 
> Sign.parent_path; 

220 

221 
val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); 

222 

223 
in thy > Sign.add_path comp_dnam 

224 
> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) 

225 
> Sign.parent_path 

226 
> fold add_matchers eqs 

227 
end; (* let (add_axioms) *) 

228 

23152  229 
end; (* struct *) 