src/HOL/Rat.thy
changeset 45507 6975db7fd6f0
parent 45478 8e299034eab4
child 45694 4a8743618257
     1.1 --- a/src/HOL/Rat.thy	Tue Nov 15 15:38:49 2011 +0100
     1.2 +++ b/src/HOL/Rat.thy	Tue Nov 15 15:38:50 2011 +0100
     1.3 @@ -1154,7 +1154,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "exhaustive f d = exhaustive (%k. exhaustive (%l. f (Fract (Code_Numeral.int_of k) (Code_Numeral.int_of l))) d) d"
     1.8 +  "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
     1.9  
    1.10  instance ..
    1.11  
    1.12 @@ -1164,8 +1164,9 @@
    1.13  begin
    1.14  
    1.15  definition
    1.16 -  "full_exhaustive f d = full_exhaustive (%(k, kt). full_exhaustive (%(l, lt).
    1.17 -     f (valterm_fract (Code_Numeral.int_of k, %_. Code_Evaluation.term_of (Code_Numeral.int_of k)) (Code_Numeral.int_of l, %_. Code_Evaluation.term_of (Code_Numeral.int_of l)))) d) d"
    1.18 +  "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k.
    1.19 +     f (let j = Code_Numeral.int_of l + 1
    1.20 +        in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"
    1.21  
    1.22  instance ..
    1.23  
    1.24 @@ -1181,16 +1182,17 @@
    1.25  lemma [code]:
    1.26    "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
    1.27    "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
    1.28 -     Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Fract'')
    1.29 -     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [],
    1.30 -        Typerep.Typerep (STR ''Rat.rat'') []]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k)" 
    1.31 +     Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'')
    1.32 +     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []],
    1.33 +        Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))"
    1.34  by (rule partial_term_of_anything)+
    1.35  
    1.36  instantiation rat :: narrowing
    1.37  begin
    1.38  
    1.39  definition
    1.40 -  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Fract) narrowing) narrowing"
    1.41 +  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply
    1.42 +    (Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing"
    1.43  
    1.44  instance ..
    1.45