24 |
24 |
25 val dc_abs = %%(dname^"_abs"); |
25 val dc_abs = %%(dname^"_abs"); |
26 val dc_rep = %%(dname^"_rep"); |
26 val dc_rep = %%(dname^"_rep"); |
27 val x_name'= "x"; |
27 val x_name'= "x"; |
28 val x_name = idx_name eqs x_name' (n+1); |
28 val x_name = idx_name eqs x_name' (n+1); |
|
29 val dnam = Sign.base_name dname; |
29 |
30 |
30 val ax_abs_iso=(dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name')); |
31 val ax_abs_iso=(dnam^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name')); |
31 val ax_rep_iso=(dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name')); |
32 val ax_rep_iso=(dnam^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name')); |
32 |
33 |
33 val ax_when_def = (dname^"_when_def",%%(dname^"_when") == |
34 val ax_when_def = (dnam^"_when_def",%%(dname^"_when") == |
34 foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) => |
35 foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) => |
35 Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); |
36 Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); |
36 |
37 |
37 fun con_def outer recu m n (_,args) = let |
38 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) |
39 fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id) |
43 fun inj y 1 _ = y |
44 fun inj y 1 _ = y |
44 | inj y _ 0 = %%"sinl"`y |
45 | inj y _ 0 = %%"sinl"`y |
45 | inj y i j = %%"sinr"`(inj y (i-1) (j-1)); |
46 | inj y i j = %%"sinr"`(inj y (i-1) (j-1)); |
46 in foldr /\# (args, outer (inj (parms args) m n)) end; |
47 in foldr /\# (args, outer (inj (parms args) m n)) end; |
47 |
48 |
48 val ax_copy_def = (dname^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo |
49 val ax_copy_def = (dnam^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo |
49 foldl (op `) (%%(dname^"_when") , |
50 foldl (op `) (%%(dname^"_when") , |
50 mapn (con_def Id true (length cons)) 0 cons))); |
51 mapn (con_def Id true (length cons)) 0 cons))); |
51 |
52 |
52 (* -- definitions concerning the constructors, discriminators and selectors - *) |
53 (* -- definitions concerning the constructors, discriminators and selectors - *) |
53 |
54 |
70 |
71 |
71 |
72 |
72 (* ----- axiom and definitions concerning induction ------------------------- *) |
73 (* ----- axiom and definitions concerning induction ------------------------- *) |
73 |
74 |
74 fun cproj' T = cproj T (length eqs) n; |
75 fun cproj' T = cproj T (length eqs) n; |
75 val ax_reach = (dname^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy")) |
76 val ax_reach = (dnam^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy")) |
76 `%x_name === %x_name)); |
77 `%x_name === %x_name)); |
77 val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",cproj' |
78 val ax_take_def = (dnam^"_take_def",%%(dname^"_take") == mk_lam("n",cproj' |
78 (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU"))); |
79 (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU"))); |
79 val ax_finite_def = (dname^"_finite_def",%%(dname^"_finite") == mk_lam(x_name, |
80 val ax_finite_def = (dnam^"_finite_def",%%(dname^"_finite") == mk_lam(x_name, |
80 mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
81 mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
81 |
82 |
82 in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @ |
83 in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @ |
83 axs_con_def @ axs_dis_def @ axs_sel_def @ |
84 axs_con_def @ axs_dis_def @ axs_sel_def @ |
84 [ax_reach, ax_take_def, ax_finite_def] |
85 [ax_reach, ax_take_def, ax_finite_def] |
85 end; (* let *) |
86 end; (* let *) |
86 |
87 |
87 |
88 |
88 in (* local *) |
89 in (* local *) |
89 |
90 |
90 fun add_axioms (comp_dname, eqs : eq list) thy' = let |
91 fun add_axioms (comp_dnam, eqs : eq list) thy' = let |
|
92 val comp_dname = Sign.full_name (sign_of thy') comp_dnam; |
91 val dnames = map (fst o fst) eqs; |
93 val dnames = map (fst o fst) eqs; |
92 val x_name = idx_name dnames "x"; |
94 val x_name = idx_name dnames "x"; |
93 fun copy_app dname = %%(dname^"_copy")`Bound 0; |
95 fun copy_app dname = %%(dname^"_copy")`Bound 0; |
94 val ax_copy_def =(comp_dname^"_copy_def" , %%(comp_dname^"_copy") == |
96 val ax_copy_def =(comp_dnam^"_copy_def" , %%(comp_dname^"_copy") == |
95 /\"f"(foldr' cpair (map copy_app dnames))); |
97 /\"f"(foldr' cpair (map copy_app dnames))); |
96 val ax_bisim_def=(comp_dname^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R", |
98 val ax_bisim_def=(comp_dnam^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R", |
97 let |
99 let |
98 fun one_con (con,args) = let |
100 fun one_con (con,args) = let |
99 val nonrec_args = filter_out is_rec args; |
101 val nonrec_args = filter_out is_rec args; |
100 val rec_args = filter is_rec args; |
102 val rec_args = filter is_rec args; |
101 val recs_cnt = length rec_args; |
103 val recs_cnt = length rec_args; |