Adapted to changes in Transitive_Closure theory.
authorberghofe
Wed Feb 07 17:26:49 2007 +0100 (2007-02-07)
changeset 222619e185f78e7d4
parent 22260 45f01828cb69
child 22262 96ba62dff413
Adapted to changes in Transitive_Closure theory.
src/HOL/Divides.thy
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Feb 07 17:26:04 2007 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Feb 07 17:26:49 2007 +0100
     1.3 @@ -32,9 +32,9 @@
     1.4    mod (infixl "mod" 70)
     1.5  
     1.6  instance nat :: "Divides.div"
     1.7 -  mod_def: "m mod n == wfrec (trancl pred_nat)
     1.8 +  mod_def: "m mod n == wfrec (pred_nat^+)
     1.9                            (%f j. if j<n | n=0 then j else f (j-n)) m"
    1.10 -  div_def:   "m div n == wfrec (trancl pred_nat) 
    1.11 +  div_def:   "m div n == wfrec (pred_nat^+) 
    1.12                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
    1.13  
    1.14  definition
    1.15 @@ -61,10 +61,10 @@
    1.16                    standard]
    1.17  
    1.18  lemma mod_eq: "(%m. m mod n) = 
    1.19 -              wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
    1.20 +              wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
    1.21  by (simp add: mod_def)
    1.22  
    1.23 -lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)  
    1.24 +lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)  
    1.25                 (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
    1.26  by (simp add: div_def)
    1.27  
     2.1 --- a/src/HOL/Wellfounded_Relations.thy	Wed Feb 07 17:26:04 2007 +0100
     2.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Feb 07 17:26:49 2007 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  
     2.5  constdefs
     2.6   less_than :: "(nat*nat)set"
     2.7 -    "less_than == trancl pred_nat"
     2.8 +    "less_than == pred_nat^+"
     2.9  
    2.10   measure   :: "('a => nat) => ('a * 'a)set"
    2.11      "measure == inv_image less_than"