src/HOL/Quickcheck_Narrowing.thy
changeset 50046 0051dc4f301f
parent 49962 a8cc904a6820
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 11 19:24:01 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Nov 11 19:56:02 2012 +0100
     1.3 @@ -411,34 +411,6 @@
     1.4       Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
     1.5  by (rule partial_term_of_anything)+
     1.6  
     1.7 -text {* Defining integers by positive and negative copy of naturals *}
     1.8 -(*
     1.9 -datatype simple_int = Positive nat | Negative nat
    1.10 -
    1.11 -primrec int_of_simple_int :: "simple_int => int"
    1.12 -where
    1.13 -  "int_of_simple_int (Positive n) = int n"
    1.14 -| "int_of_simple_int (Negative n) = (-1 - int n)"
    1.15 -
    1.16 -instantiation int :: narrowing
    1.17 -begin
    1.18 -
    1.19 -definition narrowing_int :: "code_int => int cons"
    1.20 -where
    1.21 -  "narrowing_int d = map_cons int_of_simple_int ((narrowing :: simple_int narrowing) d)"
    1.22 -
    1.23 -instance ..
    1.24 -
    1.25 -end
    1.26 -
    1.27 -text {* printing the partial terms *}
    1.28 -
    1.29 -lemma [code]:
    1.30 -  "partial_term_of (ty :: int itself) t == Code_Evaluation.App (Code_Evaluation.Const (STR ''Quickcheck_Narrowing.int_of_simple_int'')
    1.31 -     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)"
    1.32 -by (rule partial_term_of_anything)
    1.33 -
    1.34 -*)
    1.35  
    1.36  subsection {* The @{text find_unused_assms} command *}
    1.37