removed quickcheck generator for type copies temporarily
authorhaftmann
Wed May 20 12:10:22 2009 +0200 (2009-05-20)
changeset 31211ba0ad1c020ee
parent 31210 d6681ddc046c
child 31212 a94aea0cef76
removed quickcheck generator for type copies temporarily
src/HOL/Quickcheck.thy
     1.1 --- a/src/HOL/Quickcheck.thy	Wed May 20 12:09:07 2009 +0200
     1.2 +++ b/src/HOL/Quickcheck.thy	Wed May 20 12:10:22 2009 +0200
     1.3 @@ -176,66 +176,6 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection {* Type copies *}
     1.8 -
     1.9 -setup {*
    1.10 -let
    1.11 -
    1.12 -fun mk_random_typecopy tyco vs constr typ thy =
    1.13 -  let
    1.14 -    val Ts = map TFree vs;
    1.15 -    val T = Type (tyco, Ts);
    1.16 -    fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
    1.17 -    val Ttm = mk_termifyT T;
    1.18 -    val typtm = mk_termifyT typ;
    1.19 -    fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
    1.20 -    fun mk_random T = mk_const @{const_name random} [T];
    1.21 -    val size = @{term "k\<Colon>code_numeral"};
    1.22 -    val v = "x";
    1.23 -    val t_v = Free (v, typtm);
    1.24 -    val t_constr = mk_const constr Ts;
    1.25 -    val lhs = mk_random T $ size;
    1.26 -    val rhs = HOLogic.mk_ST [((mk_random typ $ size, @{typ Random.seed}), SOME (v, typtm))]
    1.27 -      (HOLogic.mk_return Ttm @{typ Random.seed}
    1.28 -      (mk_const "Code_Eval.valapp" [typ, T]
    1.29 -        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
    1.30 -      @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
    1.31 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.32 -  in
    1.33 -    thy
    1.34 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
    1.35 -    |> `(fn lthy => Syntax.check_term lthy eq)
    1.36 -    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    1.37 -    |> snd
    1.38 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.39 -  end;
    1.40 -
    1.41 -fun ensure_random_typecopy tyco thy =
    1.42 -  let
    1.43 -    val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
    1.44 -      TypecopyPackage.get_info thy tyco;
    1.45 -    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
    1.46 -    val typ = map_atyps (fn TFree (v, sort) =>
    1.47 -      TFree (v, constrain sort @{sort random})) raw_typ;
    1.48 -    val vs' = Term.add_tfreesT typ [];
    1.49 -    val vs = map (fn (v, sort) =>
    1.50 -      (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
    1.51 -    val do_inst = can (Sign.of_sort thy) (typ, @{sort random});
    1.52 -  in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
    1.53 -
    1.54 -in
    1.55 -
    1.56 -TypecopyPackage.interpretation ensure_random_typecopy
    1.57 -
    1.58 -end
    1.59 -*}
    1.60 -
    1.61 -
    1.62 -subsection {* Datatypes *}
    1.63 -
    1.64 -text {* under construction *}
    1.65 -
    1.66 -
    1.67  no_notation fcomp (infixl "o>" 60)
    1.68  no_notation scomp (infixl "o\<rightarrow>" 60)
    1.69