28 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
28 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
29 fun mk_all_imp (A,P) = |
29 fun mk_all_imp (A,P) = |
30 let val T = dest_setT (fastype_of A) |
30 let val T = dest_setT (fastype_of A) |
31 in all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0)) |
31 in all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0)) |
32 end; |
32 end; |
33 |
|
34 (** Cartesian product type **) |
|
35 |
|
36 val unitT = Type("unit",[]); |
|
37 |
|
38 fun mk_prod (T1,T2) = Type("*", [T1,T2]); |
|
39 |
|
40 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*) |
|
41 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2 |
|
42 | factors T = [T]; |
|
43 |
|
44 (*Make a correctly typed ordered pair*) |
|
45 fun mk_Pair (t1,t2) = |
|
46 let val T1 = fastype_of t1 |
|
47 and T2 = fastype_of t2 |
|
48 in Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2 end; |
|
49 |
|
50 fun split_const(Ta,Tb,Tc) = |
|
51 Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc); |
|
52 |
|
53 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
|
54 with result type T. The call creates a new term expecting one argument |
|
55 of type S.*) |
|
56 fun ap_split (Type("*", [T1,T2])) T3 u = |
|
57 split_const(T1,T2,T3) $ |
|
58 Abs("v", T1, |
|
59 ap_split T2 T3 |
|
60 ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ |
|
61 Bound 0)) |
|
62 | ap_split T T3 u = u; |
|
63 |
|
64 (*Makes a nested tuple from a list, following the product type structure*) |
|
65 fun mk_tuple (Type("*", [T1,T2])) tms = |
|
66 mk_Pair (mk_tuple T1 tms, |
|
67 mk_tuple T2 (drop (length (factors T1), tms))) |
|
68 | mk_tuple T (t::_) = t; |
|
69 |
|
70 (*Attempts to remove occurrences of split, and pair-valued parameters*) |
|
71 val remove_split = rewrite_rule [split RS eq_reflection] o |
|
72 rule_by_tactic (ALLGOALS split_all_tac); |
|
73 |
|
74 (*Uncurries any Var of function type in the rule*) |
|
75 fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) = |
|
76 let val T' = factors T1 ---> T2 |
|
77 val newt = ap_split T1 T2 (Var(v,T')) |
|
78 val cterm = Thm.cterm_of (#sign(rep_thm rl)) |
|
79 in |
|
80 remove_split (instantiate ([], [(cterm t, cterm newt)]) rl) |
|
81 end |
|
82 | split_rule_var (t,rl) = rl; |
|
83 |
|
84 (*Uncurries ALL function variables occurring in a rule's conclusion*) |
|
85 fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl) |
|
86 |> standard; |
|
87 |
|
88 |
33 |
89 (** Disjoint sum type **) |
34 (** Disjoint sum type **) |
90 |
35 |
91 fun mk_sum (T1,T2) = Type("+", [T1,T2]); |
36 fun mk_sum (T1,T2) = Type("+", [T1,T2]); |
92 val Inl = Const("Inl", dummyT) |
37 val Inl = Const("Inl", dummyT) |