equal
deleted
inserted
replaced
12 val read_cterm: Sign.sg -> string -> cterm |
12 val read_cterm: Sign.sg -> string -> cterm |
13 val boolN: string |
13 val boolN: string |
14 val boolT: typ |
14 val boolT: typ |
15 val false_const: term |
15 val false_const: term |
16 val true_const: term |
16 val true_const: term |
17 val not_const: term |
|
18 val mk_setT: typ -> typ |
17 val mk_setT: typ -> typ |
19 val dest_setT: typ -> typ |
18 val dest_setT: typ -> typ |
20 val Trueprop: term |
19 val Trueprop: term |
21 val mk_Trueprop: term -> term |
20 val mk_Trueprop: term -> term |
22 val dest_Trueprop: term -> term |
21 val dest_Trueprop: term -> term |
25 val imp: term |
24 val imp: term |
26 val Not: term |
25 val Not: term |
27 val mk_conj: term * term -> term |
26 val mk_conj: term * term -> term |
28 val mk_disj: term * term -> term |
27 val mk_disj: term * term -> term |
29 val mk_imp: term * term -> term |
28 val mk_imp: term * term -> term |
|
29 val mk_not: term -> term |
30 val dest_conj: term -> term list |
30 val dest_conj: term -> term list |
31 val dest_disj: term -> term list |
31 val dest_disj: term -> term list |
32 val dest_imp: term -> term * term |
32 val dest_imp: term -> term * term |
33 val dest_not: term -> term |
33 val dest_not: term -> term |
34 val dest_concls: term -> term list |
34 val dest_concls: term -> term list |
106 val boolN = "bool"; |
106 val boolN = "bool"; |
107 val boolT = Type (boolN, []); |
107 val boolT = Type (boolN, []); |
108 |
108 |
109 val true_const = Const ("True", boolT); |
109 val true_const = Const ("True", boolT); |
110 val false_const = Const ("False", boolT); |
110 val false_const = Const ("False", boolT); |
111 val not_const = Const ("Not", boolT --> boolT); |
|
112 |
111 |
113 fun mk_setT T = Type ("set", [T]); |
112 fun mk_setT T = Type ("set", [T]); |
114 |
113 |
115 fun dest_setT (Type ("set", [T])) = T |
114 fun dest_setT (Type ("set", [T])) = T |
116 | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); |
115 | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); |
131 and imp = Const ("op -->", [boolT, boolT] ---> boolT) |
130 and imp = Const ("op -->", [boolT, boolT] ---> boolT) |
132 and Not = Const ("Not", boolT --> boolT); |
131 and Not = Const ("Not", boolT --> boolT); |
133 |
132 |
134 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
133 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
135 and mk_disj (t1, t2) = disj $ t1 $ t2 |
134 and mk_disj (t1, t2) = disj $ t1 $ t2 |
136 and mk_imp (t1, t2) = imp $ t1 $ t2; |
135 and mk_imp (t1, t2) = imp $ t1 $ t2 |
|
136 and mk_not t = Not $ t; |
137 |
137 |
138 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t' |
138 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t' |
139 | dest_conj t = [t]; |
139 | dest_conj t = [t]; |
140 |
140 |
141 fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t' |
141 fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t' |