src/HOL/SMT.thy
changeset 41126 e0bd443c0fdd
parent 41125 4a9eec045f2a
child 41127 2ea84c8535c6
     1.1 --- a/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
     1.3 @@ -130,18 +130,20 @@
     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: "k div l = (
     1.8 -     if k = 0 \<or> l = 0 then 0
     1.9 -     else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
    1.10 -     else z3div (-k) (-l))"
    1.11 -  by (auto simp add: z3div_def)
    1.12 +lemma div_by_z3div:
    1.13 +  "\<forall>k l. k div l = (
    1.14 +    if k = 0 \<or> l = 0 then 0
    1.15 +    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
    1.16 +    else z3div (-k) (-l))"
    1.17 +  by (auto simp add: z3div_def trigger_def)
    1.18  
    1.19 -lemma mod_by_z3mod: "k mod l = (
    1.20 -     if l = 0 then k
    1.21 -     else if k = 0 then 0
    1.22 -     else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
    1.23 -     else - z3mod (-k) (-l))"
    1.24 -  by (auto simp add: z3mod_def)
    1.25 +lemma mod_by_z3mod:
    1.26 +  "\<forall>k l. k mod l = (
    1.27 +    if l = 0 then k
    1.28 +    else if k = 0 then 0
    1.29 +    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
    1.30 +    else - z3mod (-k) (-l))"
    1.31 +  by (auto simp add: z3mod_def trigger_def)
    1.32  
    1.33  
    1.34