30 handle TERM _ => error "i_of_term: unknown term"); |
30 handle TERM _ => error "i_of_term: unknown term"); |
31 |
31 |
32 fun qf_of_term ps vs t = case t |
32 fun qf_of_term ps vs t = case t |
33 of Const("True",_) => T |
33 of Const("True",_) => T |
34 | Const("False",_) => F |
34 | Const("False",_) => F |
35 | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
35 | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
36 | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
36 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
37 | Const(@{const_name "Divides.dvd"},_)$t1$t2 => |
37 | Const(@{const_name "Divides.dvd"},_)$t1$t2 => |
38 (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd") |
38 (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd") |
39 | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
39 | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
40 | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2) |
40 | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2) |
41 | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |
41 | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |