29 |
29 |
30 val abs_iso_ax = ("abs_iso" ,mk_trp(dc_rep`(dc_abs`%x_name')=== %:x_name')); |
30 val abs_iso_ax = ("abs_iso" ,mk_trp(dc_rep`(dc_abs`%x_name')=== %:x_name')); |
31 val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %:x_name')); |
31 val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %:x_name')); |
32 |
32 |
33 val when_def = ("when_def",%%:(dname^"_when") == |
33 val when_def = ("when_def",%%:(dname^"_when") == |
34 foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) => |
34 Library.foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) => |
35 Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); |
35 Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); |
36 |
36 |
37 fun con_def outer recu m n (_,args) = let |
37 fun con_def outer recu m n (_,args) = let |
38 fun idxs z x arg = (if is_lazy arg then fn t => %%:"up"`t else Id) |
38 fun idxs z x arg = (if is_lazy arg then fn t => %%:"up"`t else Id) |
39 (if recu andalso is_rec arg then (cproj (Bound z) eqs |
39 (if recu andalso is_rec arg then (cproj (Bound z) eqs |
41 fun parms [] = %%:"ONE" |
41 fun parms [] = %%:"ONE" |
42 | parms vs = foldr'(fn(x,t)=> %%:"spair"`x`t)(mapn (idxs(length vs))1 vs); |
42 | parms vs = foldr'(fn(x,t)=> %%:"spair"`x`t)(mapn (idxs(length vs))1 vs); |
43 fun inj y 1 _ = y |
43 fun inj y 1 _ = y |
44 | inj y _ 0 = %%:"sinl"`y |
44 | inj y _ 0 = %%:"sinl"`y |
45 | inj y i j = %%:"sinr"`(inj y (i-1) (j-1)); |
45 | inj y i j = %%:"sinr"`(inj y (i-1) (j-1)); |
46 in foldr /\# (args, outer (inj (parms args) m n)) end; |
46 in Library.foldr /\# (args, outer (inj (parms args) m n)) end; |
47 |
47 |
48 val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo |
48 val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo |
49 foldl (op `) (%%:(dname^"_when") , |
49 Library.foldl (op `) (%%:(dname^"_when") , |
50 mapn (con_def Id true (length cons)) 0 cons))); |
50 mapn (con_def Id true (length cons)) 0 cons))); |
51 |
51 |
52 (* -- definitions concerning the constructors, discriminators and selectors - *) |
52 (* -- definitions concerning the constructors, discriminators and selectors - *) |
53 |
53 |
54 val con_defs = mapn (fn n => fn (con,args) => (extern_name con ^"_def", |
54 val con_defs = mapn (fn n => fn (con,args) => (extern_name con ^"_def", |
55 %%:con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons; |
55 %%:con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons; |
56 |
56 |
57 val dis_defs = let |
57 val dis_defs = let |
58 fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == |
58 fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == |
59 mk_cRep_CFun(%%:(dname^"_when"),map |
59 mk_cRep_CFun(%%:(dname^"_when"),map |
60 (fn (con',args) => (foldr /\# |
60 (fn (con',args) => (Library.foldr /\# |
61 (args,if con'=con then %%:"TT" else %%:"FF"))) cons)) |
61 (args,if con'=con then %%:"TT" else %%:"FF"))) cons)) |
62 in map ddef cons end; |
62 in map ddef cons end; |
63 |
63 |
64 val sel_defs = let |
64 val sel_defs = let |
65 fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) == |
65 fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) == |
66 mk_cRep_CFun(%%:(dname^"_when"),map |
66 mk_cRep_CFun(%%:(dname^"_when"),map |
67 (fn (con',args) => if con'<>con then %%:"UU" else |
67 (fn (con',args) => if con'<>con then %%:"UU" else |
68 foldr /\# (args,Bound (length args - n))) cons)); |
68 Library.foldr /\# (args,Bound (length args - n))) cons)); |
69 in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; |
69 in List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; |
70 |
70 |
71 |
71 |
72 (* ----- axiom and definitions concerning induction ------------------------- *) |
72 (* ----- axiom and definitions concerning induction ------------------------- *) |
73 |
73 |
74 val reach_ax = ("reach", mk_trp(cproj (%%:"fix"`%%(comp_dname^"_copy")) eqs n |
74 val reach_ax = ("reach", mk_trp(cproj (%%:"fix"`%%(comp_dname^"_copy")) eqs n |
98 /\"f"(foldr' cpair (map copy_app dnames))); |
98 /\"f"(foldr' cpair (map copy_app dnames))); |
99 val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R", |
99 val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R", |
100 let |
100 let |
101 fun one_con (con,args) = let |
101 fun one_con (con,args) = let |
102 val nonrec_args = filter_out is_rec args; |
102 val nonrec_args = filter_out is_rec args; |
103 val rec_args = filter is_rec args; |
103 val rec_args = List.filter is_rec args; |
104 val recs_cnt = length rec_args; |
104 val recs_cnt = length rec_args; |
105 val allargs = nonrec_args @ rec_args |
105 val allargs = nonrec_args @ rec_args |
106 @ map (upd_vname (fn s=> s^"'")) rec_args; |
106 @ map (upd_vname (fn s=> s^"'")) rec_args; |
107 val allvns = map vname allargs; |
107 val allvns = map vname allargs; |
108 fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; |
108 fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; |
112 val rec_idxs = (recs_cnt-1) downto 0; |
112 val rec_idxs = (recs_cnt-1) downto 0; |
113 val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) |
113 val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) |
114 (allargs~~((allargs_cnt-1) downto 0))); |
114 (allargs~~((allargs_cnt-1) downto 0))); |
115 fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ |
115 fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ |
116 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); |
116 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); |
117 val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj( |
117 val capps = Library.foldr mk_conj (mapn rel_app 1 rec_args, mk_conj( |
118 Bound(allargs_cnt+1)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns1), |
118 Bound(allargs_cnt+1)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns1), |
119 Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2))); |
119 Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2))); |
120 in foldr mk_ex (allvns, foldr mk_conj |
120 in Library.foldr mk_ex (allvns, Library.foldr mk_conj |
121 (map (defined o Bound) nonlazy_idxs,capps)) end; |
121 (map (defined o Bound) nonlazy_idxs,capps)) end; |
122 fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( |
122 fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( |
123 proj (Bound 2) eqs n $ Bound 1 $ Bound 0, |
123 proj (Bound 2) eqs n $ Bound 1 $ Bound 0, |
124 foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
124 foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
125 ::map one_con cons)))); |
125 ::map one_con cons)))); |
127 fun add_one (thy,(dnam,axs,dfs)) = thy |
127 fun add_one (thy,(dnam,axs,dfs)) = thy |
128 |> Theory.add_path dnam |
128 |> Theory.add_path dnam |
129 |> add_axioms_i (infer_types thy' dfs)(*add_defs_i*) |
129 |> add_axioms_i (infer_types thy' dfs)(*add_defs_i*) |
130 |> add_axioms_i (infer_types thy' axs) |
130 |> add_axioms_i (infer_types thy' axs) |
131 |> Theory.parent_path; |
131 |> Theory.parent_path; |
132 val thy = foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); |
132 val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); |
133 in thy |> Theory.add_path comp_dnam |
133 in thy |> Theory.add_path comp_dnam |
134 |> add_axioms_i (infer_types thy' |
134 |> add_axioms_i (infer_types thy' |
135 (bisim_def::(if length eqs>1 then [copy_def] else []))) |
135 (bisim_def::(if length eqs>1 then [copy_def] else []))) |
136 |> Theory.parent_path |
136 |> Theory.parent_path |
137 end; |
137 end; |