89 let fun tag t = |
89 let fun tag t = |
90 let val (c,ts) = strip_comb t |
90 let val (c,ts) = strip_comb t |
91 in case c of |
91 in case c of |
92 Const(@{const_name "op &"}, _) => apply c (map tag ts) |
92 Const(@{const_name "op &"}, _) => apply c (map tag ts) |
93 | Const(@{const_name "op |"}, _) => apply c (map tag ts) |
93 | Const(@{const_name "op |"}, _) => apply c (map tag ts) |
94 | Const(@{const_name "op -->"}, _) => 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 "op ="}, Type ("fun", [T,_])) => |
99 if T = HOLogic.boolT then |
99 if T = HOLogic.boolT then |
185 (*translation of a formula*) |
185 (*translation of a formula*) |
186 and fm pos (Const(@{const_name "op &"}, _) $ p $ q) = |
186 and fm pos (Const(@{const_name "op &"}, _) $ p $ q) = |
187 Buildin("AND", [fm pos p, fm pos q]) |
187 Buildin("AND", [fm pos p, fm pos q]) |
188 | fm pos (Const(@{const_name "op |"}, _) $ p $ q) = |
188 | fm pos (Const(@{const_name "op |"}, _) $ p $ q) = |
189 Buildin("OR", [fm pos p, fm pos q]) |
189 Buildin("OR", [fm pos p, fm pos q]) |
190 | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) = |
190 | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) = |
191 Buildin("=>", [fm (not pos) p, fm pos q]) |
191 Buildin("=>", [fm (not pos) p, fm pos q]) |
192 | fm pos (Const(@{const_name Not}, _) $ p) = |
192 | fm pos (Const(@{const_name Not}, _) $ p) = |
193 Buildin("NOT", [fm (not pos) p]) |
193 Buildin("NOT", [fm (not pos) p]) |
194 | fm pos (Const(@{const_name True}, _)) = TrueExpr |
194 | fm pos (Const(@{const_name True}, _)) = TrueExpr |
195 | fm pos (Const(@{const_name False}, _)) = FalseExpr |
195 | fm pos (Const(@{const_name False}, _)) = FalseExpr |