49 |
49 |
50 (*** Abstract syntax operations on the meta-connectives ***) |
50 (*** Abstract syntax operations on the meta-connectives ***) |
51 |
51 |
52 (** equality **) |
52 (** equality **) |
53 |
53 |
54 (*Make an equality. DOES NOT CHECK TYPE OF u! *) |
54 (*Make an equality.*) |
55 fun mk_equals(t,u) = equals(type_of t) $ t $ u; |
55 fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; |
56 |
56 |
57 fun dest_equals (Const("==",_) $ t $ u) = (t,u) |
57 fun dest_equals (Const("==",_) $ t $ u) = (t,u) |
58 | dest_equals t = raise TERM("dest_equals", [t]); |
58 | dest_equals t = raise TERM("dest_equals", [t]); |
59 |
59 |
60 (** implies **) |
60 (** implies **) |
90 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) |
90 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) |
91 | count_prems (_,n) = n; |
91 | count_prems (_,n) = n; |
92 |
92 |
93 (** flex-flex constraints **) |
93 (** flex-flex constraints **) |
94 |
94 |
95 (*Make a constraint. DOES NOT CHECK TYPE OF u! *) |
95 (*Make a constraint.*) |
96 fun mk_flexpair(t,u) = flexpair(type_of t) $ t $ u; |
96 fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; |
97 |
97 |
98 fun dest_flexpair (Const("=?=",_) $ t $ u) = (t,u) |
98 fun dest_flexpair (Const("=?=",_) $ t $ u) = (t,u) |
99 | dest_flexpair t = raise TERM("dest_flexpair", [t]); |
99 | dest_flexpair t = raise TERM("dest_flexpair", [t]); |
100 |
100 |
101 (*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C ) |
101 (*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C ) |