35 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) => |
36 Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); |
36 Bound(1+length cons+x-y)))`(dc_rep`Bound 0)))); |
37 |
37 |
38 fun con_def outer recu m n (_,args) = let |
38 fun con_def outer recu m n (_,args) = let |
39 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) |
40 (if recu andalso is_rec arg then (cproj (Bound z) |
40 (if recu andalso is_rec arg then (cproj (Bound z) eqs |
41 (length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x)); |
41 (rec_of arg))`Bound(z-x) else Bound(z-x)); |
42 fun parms [] = %%"ONE" |
42 fun parms [] = %%"ONE" |
43 | parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs); |
43 | parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs); |
44 fun inj y 1 _ = y |
44 fun inj y 1 _ = y |
45 | inj y _ 0 = %%"sinl"`y |
45 | inj y _ 0 = %%"sinl"`y |
46 | inj y i j = %%"sinr"`(inj y (i-1) (j-1)); |
46 | inj y i j = %%"sinr"`(inj y (i-1) (j-1)); |
70 in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; |
70 in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; |
71 |
71 |
72 |
72 |
73 (* ----- axiom and definitions concerning induction ------------------------- *) |
73 (* ----- axiom and definitions concerning induction ------------------------- *) |
74 |
74 |
75 fun cproj' T = cproj T (length eqs) n; |
75 val reach_ax = ("reach", mk_trp(cproj (%%"fix"`%%(comp_dname^"_copy")) eqs n |
76 val reach_ax = ("reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy")) |
|
77 `%x_name === %x_name)); |
76 `%x_name === %x_name)); |
78 val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj' |
77 val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj' |
79 (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU"))); |
78 (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU") eqs n)); |
80 val finite_def = ("finite_def",%%(dname^"_finite") == mk_lam(x_name, |
79 val finite_def = ("finite_def",%%(dname^"_finite") == mk_lam(x_name, |
81 mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
80 mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); |
82 |
81 |
83 in (dnam, |
82 in (dnam, |
84 [abs_iso_ax, rep_iso_ax, reach_ax], |
83 [abs_iso_ax, rep_iso_ax, reach_ax], |
111 val vns2 = map (vname_arg "'") args; |
110 val vns2 = map (vname_arg "'") args; |
112 val allargs_cnt = length nonrec_args + 2*recs_cnt; |
111 val allargs_cnt = length nonrec_args + 2*recs_cnt; |
113 val rec_idxs = (recs_cnt-1) downto 0; |
112 val rec_idxs = (recs_cnt-1) downto 0; |
114 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) |
115 (allargs~~((allargs_cnt-1) downto 0))); |
114 (allargs~~((allargs_cnt-1) downto 0))); |
116 fun rel_app i ra = proj (Bound(allargs_cnt+2)) (length eqs) (rec_of ra) $ |
115 fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ |
117 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); |
116 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); |
118 val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj( |
117 val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj( |
119 Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1), |
118 Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1), |
120 Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2))); |
119 Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2))); |
121 in foldr mk_ex (allvns, foldr mk_conj |
120 in foldr mk_ex (allvns, foldr mk_conj |
122 (map (defined o Bound) nonlazy_idxs,capps)) end; |
121 (map (defined o Bound) nonlazy_idxs,capps)) end; |
123 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( |
124 proj (Bound 2) (length eqs) n $ Bound 1 $ Bound 0, |
123 proj (Bound 2) eqs n $ Bound 1 $ Bound 0, |
125 foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
124 foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
126 ::map one_con cons)))); |
125 ::map one_con cons)))); |
127 in foldr' mk_conj (mapn one_comp 0 eqs)end )); |
126 in foldr' mk_conj (mapn one_comp 0 eqs)end )); |
128 fun add_one (thy,(dnam,axs,dfs)) = thy |
127 fun add_one (thy,(dnam,axs,dfs)) = thy |
129 |> Theory.add_path dnam |
128 |> Theory.add_path dnam |