93 | Const(@{const_name HOL.disj}, _) => apply c (map tag ts) |
93 | Const(@{const_name HOL.disj}, _) => apply c (map tag ts) |
94 | Const(@{const_name HOL.implies}, _) => apply c (map tag ts) |
94 | Const(@{const_name HOL.implies}, _) => apply c (map tag ts) |
95 | Const(@{const_name Not}, _) => apply c (map tag ts) |
95 | Const(@{const_name Not}, _) => apply c (map tag ts) |
96 | Const(@{const_name True}, _) => (c, false) |
96 | Const(@{const_name True}, _) => (c, false) |
97 | Const(@{const_name False}, _) => (c, false) |
97 | Const(@{const_name False}, _) => (c, false) |
98 | Const(@{const_name "op ="}, Type ("fun", [T,_])) => |
98 | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) => |
99 if T = HOLogic.boolT then |
99 if T = HOLogic.boolT then |
100 (*biconditional: with int/nat comparisons below?*) |
100 (*biconditional: with int/nat comparisons below?*) |
101 let val [t1,t2] = ts |
101 let val [t1,t2] = ts |
102 val (u1,b1) = tag t1 |
102 val (u1,b1) = tag t1 |
103 and (u2,b2) = tag t2 |
103 and (u2,b2) = tag t2 |
198 Buildin("=", [fm pos p, fm pos q]) |
198 Buildin("=", [fm pos p, fm pos q]) |
199 | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = |
199 | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = |
200 Buildin("AND", (*unfolding uses both polarities*) |
200 Buildin("AND", (*unfolding uses both polarities*) |
201 [Buildin("=>", [fm (not pos) p, fm pos q]), |
201 [Buildin("=>", [fm (not pos) p, fm pos q]), |
202 Buildin("=>", [fm (not pos) q, fm pos p])]) |
202 Buildin("=>", [fm (not pos) q, fm pos p])]) |
203 | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) = |
203 | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) = |
204 let val tx = tm x and ty = tm y |
204 let val tx = tm x and ty = tm y |
205 in if pos orelse T = HOLogic.realT then |
205 in if pos orelse T = HOLogic.realT then |
206 Buildin("=", [tx, ty]) |
206 Buildin("=", [tx, ty]) |
207 else if is_intnat T then |
207 else if is_intnat T then |
208 Buildin("AND", |
208 Buildin("AND", |