78 if term_of x aconv y then Lt (Thm.dest_arg ct) |
78 if term_of x aconv y then Lt (Thm.dest_arg ct) |
79 else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox |
79 else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox |
80 | Const (@{const_name HOL.less_eq}, _) $ y $ z => |
80 | Const (@{const_name HOL.less_eq}, _) $ y $ z => |
81 if term_of x aconv y then Le (Thm.dest_arg ct) |
81 if term_of x aconv y then Le (Thm.dest_arg ct) |
82 else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox |
82 else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox |
83 | Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) => |
83 | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) => |
84 if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox |
84 if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox |
85 | Const (@{const_name Not},_) $ (Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) => |
85 | Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) => |
86 if term_of x aconv y then |
86 if term_of x aconv y then |
87 NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox |
87 NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox |
88 | _ => Nox) |
88 | _ => Nox) |
89 handle CTERM _ => Nox; |
89 handle CTERM _ => Nox; |
90 |
90 |
221 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = |
221 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = |
222 lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s) |
222 lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s) |
223 | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = |
223 | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = |
224 lin vs (Const (@{const_name HOL.less}, T) $ t $ s) |
224 lin vs (Const (@{const_name HOL.less}, T) $ t $ s) |
225 | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t) |
225 | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t) |
226 | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) = |
226 | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) = |
227 HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t) |
227 HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t) |
228 | lin (vs as x::_) ((b as Const("op =",_))$s$t) = |
228 | lin (vs as x::_) ((b as Const("op =",_))$s$t) = |
229 (case lint vs (subC$t$s) of |
229 (case lint vs (subC$t$s) of |
230 (t as a$(m$c$y)$r) => |
230 (t as a$(m$c$y)$r) => |
231 if x <> y then b$zero$t |
231 if x <> y then b$zero$t |
232 else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r |
232 else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r |
250 fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT |
250 fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT |
251 | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT |
251 | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT |
252 | is_intrel _ = false; |
252 | is_intrel _ = false; |
253 |
253 |
254 fun linearize_conv ctxt vs ct = case term_of ct of |
254 fun linearize_conv ctxt vs ct = case term_of ct of |
255 Const(@{const_name Divides.dvd},_)$d$t => |
255 Const(@{const_name Ring_and_Field.dvd},_)$d$t => |
256 let |
256 let |
257 val th = binop_conv (lint_conv ctxt vs) ct |
257 val th = binop_conv (lint_conv ctxt vs) ct |
258 val (d',t') = Thm.dest_binop (Thm.rhs_of th) |
258 val (d',t') = Thm.dest_binop (Thm.rhs_of th) |
259 val (dt',tt') = (term_of d', term_of t') |
259 val (dt',tt') = (term_of d', term_of t') |
260 in if is_numeral dt' andalso is_numeral tt' |
260 in if is_numeral dt' andalso is_numeral tt' |
275 (Thm.transitive dth (inst' [d'',t'] dvd_uminus')) |
275 (Thm.transitive dth (inst' [d'',t'] dvd_uminus')) |
276 else dth end |
276 else dth end |
277 | _ => dth |
277 | _ => dth |
278 end |
278 end |
279 end |
279 end |
280 | Const (@{const_name Not},_)$(Const(@{const_name Divides.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct |
280 | Const (@{const_name Not},_)$(Const(@{const_name Ring_and_Field.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct |
281 | t => if is_intrel t |
281 | t => if is_intrel t |
282 then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop)) |
282 then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop)) |
283 RS eq_reflection |
283 RS eq_reflection |
284 else reflexive ct; |
284 else reflexive ct; |
285 |
285 |
298 then (ins (dest_numeral c) acc,dacc) else (acc,dacc) |
298 then (ins (dest_numeral c) acc,dacc) else (acc,dacc) |
299 | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => |
299 | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => |
300 if x aconv y andalso member (op =) |
300 if x aconv y andalso member (op =) |
301 [@{const_name HOL.less}, @{const_name HOL.less_eq}] s |
301 [@{const_name HOL.less}, @{const_name HOL.less_eq}] s |
302 then (ins (dest_numeral c) acc, dacc) else (acc,dacc) |
302 then (ins (dest_numeral c) acc, dacc) else (acc,dacc) |
303 | Const(@{const_name Divides.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) => |
303 | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) => |
304 if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) |
304 if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) |
305 | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
305 | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
306 | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
306 | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
307 | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) |
307 | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) |
308 | _ => (acc, dacc) |
308 | _ => (acc, dacc) |
338 then cv (l div dest_numeral c) t else Thm.reflexive t |
338 then cv (l div dest_numeral c) t else Thm.reflexive t |
339 | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => |
339 | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => |
340 if x=y andalso member (op =) |
340 if x=y andalso member (op =) |
341 [@{const_name HOL.less}, @{const_name HOL.less_eq}] s |
341 [@{const_name HOL.less}, @{const_name HOL.less_eq}] s |
342 then cv (l div dest_numeral c) t else Thm.reflexive t |
342 then cv (l div dest_numeral c) t else Thm.reflexive t |
343 | Const(@{const_name Divides.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) => |
343 | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) => |
344 if x=y then |
344 if x=y then |
345 let |
345 let |
346 val k = l div dest_numeral c |
346 val k = l div dest_numeral c |
347 val kt = HOLogic.mk_number iT k |
347 val kt = HOLogic.mk_number iT k |
348 val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] |
348 val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] |
554 fun qf_of_term ps vs t = case t |
554 fun qf_of_term ps vs t = case t |
555 of Const("True",_) => T |
555 of Const("True",_) => T |
556 | Const("False",_) => F |
556 | Const("False",_) => F |
557 | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
557 | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
558 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
558 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
559 | Const(@{const_name Divides.dvd},_)$t1$t2 => |
559 | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => |
560 (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") |
560 (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") |
561 | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
561 | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
562 | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2) |
562 | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2) |
563 | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |
563 | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |
564 | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2) |
564 | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2) |