author | oheimb |
Thu, 30 Oct 1997 14:17:33 +0100 | |
changeset 4041 | 4df7f385fe9f |
parent 4008 | 2444085532c6 |
child 4043 | 35766855f344 |
permissions | -rw-r--r-- |
2453 | 1 |
(* Title: HOLCF/domain/axioms.ML |
2 |
ID: $Id$ |
|
3 |
Author : David von Oheimb |
|
4 |
Copyright 1995, 1996 TU Muenchen |
|
5 |
||
6 |
syntax generator for domain section |
|
1274 | 7 |
*) |
8 |
||
9 |
structure Domain_Axioms = struct |
|
10 |
||
11 |
local |
|
12 |
||
13 |
open Domain_Library; |
|
14 |
infixr 0 ===>;infixr 0 ==>;infix 0 == ; |
|
15 |
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
|
16 |
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
|
17 |
||
18 |
fun infer_types thy' = map (inferT_axm (sign_of thy')); |
|
19 |
||
20 |
fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= |
|
21 |
let |
|
22 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
23 |
(* ----- axioms and definitions concerning the isomorphism ------------------ *) |
1274 | 24 |
|
25 |
val dc_abs = %%(dname^"_abs"); |
|
26 |
val dc_rep = %%(dname^"_rep"); |
|
27 |
val x_name'= "x"; |
|
28 |
val x_name = idx_name eqs x_name' (n+1); |
|
4008 | 29 |
val dnam = Sign.base_name dname; |
1274 | 30 |
|
4008 | 31 |
val ax_abs_iso=(dnam^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name')); |
32 |
val ax_rep_iso=(dnam^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name')); |
|
1274 | 33 |
|
4008 | 34 |
val ax_when_def = (dnam^"_when_def",%%(dname^"_when") == |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
35 |
foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) => |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
36 |
Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); |
1274 | 37 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
38 |
fun con_def outer recu m n (_,args) = let |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
39 |
fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
40 |
(if recu andalso is_rec arg then (cproj (Bound z) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
41 |
(length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x)); |
2641
533a84b3bedd
using types one = unit lift and translations causes troubles between
slotosch
parents:
2453
diff
changeset
|
42 |
fun parms [] = %%"ONE" |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
43 |
| parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
44 |
fun inj y 1 _ = y |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
45 |
| inj y _ 0 = %%"sinl"`y |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
46 |
| inj y i j = %%"sinr"`(inj y (i-1) (j-1)); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
47 |
in foldr /\# (args, outer (inj (parms args) m n)) end; |
1274 | 48 |
|
4008 | 49 |
val ax_copy_def = (dnam^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
50 |
foldl (op `) (%%(dname^"_when") , |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
51 |
mapn (con_def Id true (length cons)) 0 cons))); |
1274 | 52 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
53 |
(* -- definitions concerning the constructors, discriminators and selectors - *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
54 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
55 |
val axs_con_def = mapn (fn n => fn (con,args) => (extern_name con ^"_def", |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
56 |
%%con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons; |
1274 | 57 |
|
58 |
val axs_dis_def = let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
59 |
fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
60 |
mk_cfapp(%%(dname^"_when"),map |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
61 |
(fn (con',args) => (foldr /\# |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
62 |
(args,if con'=con then %%"TT" else %%"FF"))) cons)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
63 |
in map ddef cons end; |
1274 | 64 |
|
65 |
val axs_sel_def = let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
66 |
fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
67 |
mk_cfapp(%%(dname^"_when"),map |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
68 |
(fn (con',args) => if con'<>con then %%"UU" else |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
69 |
foldr /\# (args,Bound (length args - n))) cons)); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
70 |
in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; |
1274 | 71 |
|
72 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
73 |
(* ----- axiom and definitions concerning induction ------------------------- *) |
1274 | 74 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
75 |
fun cproj' T = cproj T (length eqs) n; |
4008 | 76 |
val ax_reach = (dnam^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy")) |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
77 |
`%x_name === %x_name)); |
4008 | 78 |
val ax_take_def = (dnam^"_take_def",%%(dname^"_take") == mk_lam("n",cproj' |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
79 |
(%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU"))); |
4008 | 80 |
val ax_finite_def = (dnam^"_finite_def",%%(dname^"_finite") == mk_lam(x_name, |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
81 |
mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
1274 | 82 |
|
83 |
in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @ |
|
84 |
axs_con_def @ axs_dis_def @ axs_sel_def @ |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
85 |
[ax_reach, ax_take_def, ax_finite_def] |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
86 |
end; (* let *) |
1274 | 87 |
|
88 |
||
89 |
in (* local *) |
|
90 |
||
4008 | 91 |
fun add_axioms (comp_dnam, eqs : eq list) thy' = let |
92 |
val comp_dname = Sign.full_name (sign_of thy') comp_dnam; |
|
1274 | 93 |
val dnames = map (fst o fst) eqs; |
94 |
val x_name = idx_name dnames "x"; |
|
95 |
fun copy_app dname = %%(dname^"_copy")`Bound 0; |
|
4008 | 96 |
val ax_copy_def =(comp_dnam^"_copy_def" , %%(comp_dname^"_copy") == |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
97 |
/\"f"(foldr' cpair (map copy_app dnames))); |
4008 | 98 |
val ax_bisim_def=(comp_dnam^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R", |
1274 | 99 |
let |
100 |
fun one_con (con,args) = let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
101 |
val nonrec_args = filter_out is_rec args; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
102 |
val rec_args = filter is_rec args; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
103 |
val recs_cnt = length rec_args; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
104 |
val allargs = nonrec_args @ rec_args |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
105 |
@ map (upd_vname (fn s=> s^"'")) rec_args; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
106 |
val allvns = map vname allargs; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
107 |
fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
108 |
val vns1 = map (vname_arg "" ) args; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
109 |
val vns2 = map (vname_arg "'") args; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
110 |
val allargs_cnt = length nonrec_args + 2*recs_cnt; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
111 |
val rec_idxs = (recs_cnt-1) downto 0; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
112 |
val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
113 |
(allargs~~((allargs_cnt-1) downto 0))); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
114 |
fun rel_app i ra = proj (Bound(allargs_cnt+2)) (length eqs) (rec_of ra) $ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
115 |
Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
116 |
val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj( |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
117 |
Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1), |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
118 |
Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2))); |
1274 | 119 |
in foldr mk_ex (allvns, foldr mk_conj |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
120 |
(map (defined o Bound) nonlazy_idxs,capps)) end; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
121 |
fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
122 |
proj (Bound 2) (length eqs) n $ Bound 1 $ Bound 0, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
123 |
foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
124 |
::map one_con cons)))); |
1274 | 125 |
in foldr' mk_conj (mapn one_comp 0 eqs)end )); |
126 |
val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @ |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
127 |
(if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def]; |
3771 | 128 |
in thy' |> Theory.add_axioms_i (infer_types thy' thy_axs) end; |
1274 | 129 |
|
130 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
131 |
fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
132 |
fun P_name typ = "P"^(if typs = [typ] then "" |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
133 |
else string_of_int(1 + find(typ,typs))); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
134 |
fun lift_adm t = lift (fn typ => %%"adm" $ %(P_name typ)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
135 |
(if finite then [] else typs,t); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
136 |
fun lift_pred_UU t = lift (fn typ => %(P_name typ) $ UU) (typs,t); |
1274 | 137 |
fun one_cnstr (cnstr,vns,(args,res)) = let |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
138 |
val rec_args = filter (fn (_,typ) => typ mem typs)(vns~~args); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
139 |
val app = mk_cfapp(%%cnstr,map (bound_arg vns) vns); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
140 |
in foldr mk_All (vns, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
141 |
lift (fn (vn,typ) => %(P_name typ) $ bound_arg vns vn) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
142 |
(rec_args,defined app ==> %(P_name res)$app)) end; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
143 |
fun one_conc typ = let val pn = P_name typ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
144 |
in %pn $ %("x"^implode(tl(explode pn))) end; |
1274 | 145 |
val concl = mk_trp(foldr' mk_conj (map one_conc typs)); |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
146 |
val induct = (tname^"_induct",lift_adm(lift_pred_UU( |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
147 |
foldr (op ===>) (map one_cnstr cnstrs,concl)))); |
3771 | 148 |
in thy' |> Theory.add_axioms_i (infer_types thy' [induct]) end; |
1274 | 149 |
|
150 |
end; (* local *) |
|
151 |
end; (* struct *) |