71 Const("op &",_)$_$_ => And (Thm.dest_binop ct) |
71 Const("op &",_)$_$_ => And (Thm.dest_binop ct) |
72 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct) |
72 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct) |
73 | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox |
73 | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox |
74 | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) => |
74 | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) => |
75 if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox |
75 if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox |
76 | Const (@{const_name HOL.less}, _) $ y$ z => |
76 | Const (@{const_name Algebras.less}, _) $ y$ z => |
77 if term_of x aconv y then Lt (Thm.dest_arg ct) |
77 if term_of x aconv y then Lt (Thm.dest_arg ct) |
78 else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox |
78 else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox |
79 | Const (@{const_name HOL.less_eq}, _) $ y $ z => |
79 | Const (@{const_name Algebras.less_eq}, _) $ y $ z => |
80 if term_of x aconv y then Le (Thm.dest_arg ct) |
80 if term_of x aconv y then Le (Thm.dest_arg ct) |
81 else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox |
81 else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox |
82 | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) => |
82 | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) => |
83 if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox |
83 if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox |
84 | Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) => |
84 | Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) => |
85 if term_of x aconv y then |
85 if term_of x aconv y then |
86 NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox |
86 NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox |
87 | _ => Nox) |
87 | _ => Nox) |
88 handle CTERM _ => Nox; |
88 handle CTERM _ => Nox; |
89 |
89 |
173 (* Canonical linear form for terms, formulae etc.. *) |
173 (* Canonical linear form for terms, formulae etc.. *) |
174 fun provelin ctxt t = Goal.prove ctxt [] [] t |
174 fun provelin ctxt t = Goal.prove ctxt [] [] t |
175 (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]); |
175 (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]); |
176 fun linear_cmul 0 tm = zero |
176 fun linear_cmul 0 tm = zero |
177 | linear_cmul n tm = case tm of |
177 | linear_cmul n tm = case tm of |
178 Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b |
178 Const (@{const_name Algebras.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b |
179 | Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x |
179 | Const (@{const_name Algebras.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x |
180 | Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b |
180 | Const (@{const_name Algebras.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b |
181 | (m as Const (@{const_name HOL.uminus}, _)) $ a => m $ linear_cmul n a |
181 | (m as Const (@{const_name Algebras.uminus}, _)) $ a => m $ linear_cmul n a |
182 | _ => numeral1 (fn m => n * m) tm; |
182 | _ => numeral1 (fn m => n * m) tm; |
183 fun earlier [] x y = false |
183 fun earlier [] x y = false |
184 | earlier (h::t) x y = |
184 | earlier (h::t) x y = |
185 if h aconv y then false else if h aconv x then true else earlier t x y; |
185 if h aconv y then false else if h aconv x then true else earlier t x y; |
186 |
186 |
187 fun linear_add vars tm1 tm2 = case (tm1, tm2) of |
187 fun linear_add vars tm1 tm2 = case (tm1, tm2) of |
188 (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, |
188 (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, |
189 Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) => |
189 Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) => |
190 if x1 = x2 then |
190 if x1 = x2 then |
191 let val c = numeral2 Integer.add c1 c2 |
191 let val c = numeral2 Integer.add c1 c2 |
192 in if c = zero then linear_add vars r1 r2 |
192 in if c = zero then linear_add vars r1 r2 |
193 else addC$(mulC$c$x1)$(linear_add vars r1 r2) |
193 else addC$(mulC$c$x1)$(linear_add vars r1 r2) |
194 end |
194 end |
195 else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
195 else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
196 else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
196 else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
197 | (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, _) => |
197 | (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) => |
198 addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
198 addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
199 | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) => |
199 | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) => |
200 addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
200 addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
201 | (_, _) => numeral2 Integer.add tm1 tm2; |
201 | (_, _) => numeral2 Integer.add tm1 tm2; |
202 |
202 |
203 fun linear_neg tm = linear_cmul ~1 tm; |
203 fun linear_neg tm = linear_cmul ~1 tm; |
204 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); |
204 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); |
205 |
205 |
206 |
206 |
207 fun lint vars tm = if is_numeral tm then tm else case tm of |
207 fun lint vars tm = if is_numeral tm then tm else case tm of |
208 Const (@{const_name HOL.uminus}, _) $ t => linear_neg (lint vars t) |
208 Const (@{const_name Algebras.uminus}, _) $ t => linear_neg (lint vars t) |
209 | Const (@{const_name HOL.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) |
209 | Const (@{const_name Algebras.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) |
210 | Const (@{const_name HOL.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) |
210 | Const (@{const_name Algebras.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) |
211 | Const (@{const_name HOL.times}, _) $ s $ t => |
211 | Const (@{const_name Algebras.times}, _) $ s $ t => |
212 let val s' = lint vars s |
212 let val s' = lint vars s |
213 val t' = lint vars t |
213 val t' = lint vars t |
214 in if is_numeral s' then (linear_cmul (dest_numeral s') t') |
214 in if is_numeral s' then (linear_cmul (dest_numeral s') t') |
215 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
215 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
216 else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm])) |
216 else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm])) |
217 end |
217 end |
218 | _ => addC $ (mulC $ one $ tm) $ zero; |
218 | _ => addC $ (mulC $ one $ tm) $ zero; |
219 |
219 |
220 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = |
220 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) = |
221 lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s) |
221 lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s) |
222 | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = |
222 | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) = |
223 lin vs (Const (@{const_name HOL.less}, T) $ t $ s) |
223 lin vs (Const (@{const_name Algebras.less}, T) $ t $ s) |
224 | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t) |
224 | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t) |
225 | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) = |
225 | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) = |
226 HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t) |
226 HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t) |
227 | lin (vs as x::_) ((b as Const("op =",_))$s$t) = |
227 | lin (vs as x::_) ((b as Const("op =",_))$s$t) = |
228 (case lint vs (subC$t$s) of |
228 (case lint vs (subC$t$s) of |
291 val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE |
291 val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE |
292 val x = term_of cx |
292 val x = term_of cx |
293 val ins = insert (op = : int * int -> bool) |
293 val ins = insert (op = : int * int -> bool) |
294 fun h (acc,dacc) t = |
294 fun h (acc,dacc) t = |
295 case (term_of t) of |
295 case (term_of t) of |
296 Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ => |
296 Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ => |
297 if x aconv y andalso member (op =) |
297 if x aconv y andalso member (op =) |
298 ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s |
298 ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s |
299 then (ins (dest_numeral c) acc,dacc) else (acc,dacc) |
299 then (ins (dest_numeral c) acc,dacc) else (acc,dacc) |
300 | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => |
300 | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) => |
301 if x aconv y andalso member (op =) |
301 if x aconv y andalso member (op =) |
302 [@{const_name HOL.less}, @{const_name HOL.less_eq}] s |
302 [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s |
303 then (ins (dest_numeral c) acc, dacc) else (acc,dacc) |
303 then (ins (dest_numeral c) acc, dacc) else (acc,dacc) |
304 | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) => |
304 | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) => |
305 if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) |
305 if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) |
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("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
307 | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
308 | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) |
308 | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) |
309 | _ => (acc, dacc) |
309 | _ => (acc, dacc) |
333 fun unit_conv t = |
333 fun unit_conv t = |
334 case (term_of t) of |
334 case (term_of t) of |
335 Const("op &",_)$_$_ => binop_conv unit_conv t |
335 Const("op &",_)$_$_ => binop_conv unit_conv t |
336 | Const("op |",_)$_$_ => binop_conv unit_conv t |
336 | Const("op |",_)$_$_ => binop_conv unit_conv t |
337 | Const (@{const_name Not},_)$_ => arg_conv unit_conv t |
337 | Const (@{const_name Not},_)$_ => arg_conv unit_conv t |
338 | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ => |
338 | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ => |
339 if x=y andalso member (op =) |
339 if x=y andalso member (op =) |
340 ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s |
340 ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s |
341 then cv (l div dest_numeral c) t else Thm.reflexive t |
341 then cv (l div dest_numeral c) t else Thm.reflexive t |
342 | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => |
342 | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) => |
343 if x=y andalso member (op =) |
343 if x=y andalso member (op =) |
344 [@{const_name HOL.less}, @{const_name HOL.less_eq}] s |
344 [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s |
345 then cv (l div dest_numeral c) t else Thm.reflexive t |
345 then cv (l div dest_numeral c) t else Thm.reflexive t |
346 | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) => |
346 | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) => |
347 if x=y then |
347 if x=y then |
348 let |
348 let |
349 val k = l div dest_numeral c |
349 val k = l div dest_numeral c |
350 val kt = HOLogic.mk_number iT k |
350 val kt = HOLogic.mk_number iT k |
351 val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] |
351 val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] |
544 of NONE => cooper "Variable not found in the list!" |
544 of NONE => cooper "Variable not found in the list!" |
545 | SOME n => Bound n) |
545 | SOME n => Bound n) |
546 | @{term "0::int"} => C 0 |
546 | @{term "0::int"} => C 0 |
547 | @{term "1::int"} => C 1 |
547 | @{term "1::int"} => C 1 |
548 | Term.Bound i => Bound i |
548 | Term.Bound i => Bound i |
549 | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t') |
549 | Const(@{const_name Algebras.uminus},_)$t' => Neg (i_of_term vs t') |
550 | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
550 | Const(@{const_name Algebras.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
551 | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
551 | Const(@{const_name Algebras.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
552 | Const(@{const_name HOL.times},_)$t1$t2 => |
552 | Const(@{const_name Algebras.times},_)$t1$t2 => |
553 (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2) |
553 (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2) |
554 handle TERM _ => |
554 handle TERM _ => |
555 (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1) |
555 (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1) |
556 handle TERM _ => cooper "Reification: Unsupported kind of multiplication")) |
556 handle TERM _ => cooper "Reification: Unsupported kind of multiplication")) |
557 | _ => (C (HOLogic.dest_number t |> snd) |
557 | _ => (C (HOLogic.dest_number t |> snd) |
558 handle TERM _ => cooper "Reification: unknown term"); |
558 handle TERM _ => cooper "Reification: unknown term"); |
559 |
559 |
560 fun qf_of_term ps vs t = case t |
560 fun qf_of_term ps vs t = case t |
561 of Const("True",_) => T |
561 of Const("True",_) => T |
562 | Const("False",_) => F |
562 | Const("False",_) => F |
563 | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
563 | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
564 | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
564 | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
565 | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => |
565 | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => |
566 (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *) |
566 (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *) |
567 | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
567 | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
568 | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2) |
568 | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2) |
569 | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |
569 | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |