src/HOL/SMT.thy
changeset 41280 a7de9d36f4f2
parent 41174 10eb369f8c01
child 41281 679118e35378
     1.1 --- a/src/HOL/SMT.thy	Sun Dec 19 00:13:25 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Sun Dec 19 17:55:56 2010 +0100
     1.3 @@ -130,21 +130,6 @@
     1.4  definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
     1.5    "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
     1.6  
     1.7 -lemma div_by_z3div:
     1.8 -  "\<forall>k l. k div l = (
     1.9 -    if k = 0 \<or> l = 0 then 0
    1.10 -    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
    1.11 -    else z3div (-k) (-l))"
    1.12 -  by (auto simp add: z3div_def trigger_def)
    1.13 -
    1.14 -lemma mod_by_z3mod:
    1.15 -  "\<forall>k l. k mod l = (
    1.16 -    if l = 0 then k
    1.17 -    else if k = 0 then 0
    1.18 -    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
    1.19 -    else - z3mod (-k) (-l))"
    1.20 -  by (auto simp add: z3mod_def trigger_def)
    1.21 -
    1.22  
    1.23  
    1.24  subsection {* Setup *}
    1.25 @@ -391,8 +376,8 @@
    1.26  
    1.27  hide_type term_bool
    1.28  hide_type (open) pattern
    1.29 -hide_const Pattern fun_app
    1.30 -hide_const (open) trigger pat nopat weight z3div z3mod
    1.31 +hide_const Pattern fun_app z3div z3mod
    1.32 +hide_const (open) trigger pat nopat weight
    1.33  
    1.34  
    1.35