--- a/src/HOL/Quickcheck.thy Wed May 20 12:09:07 2009 +0200
+++ b/src/HOL/Quickcheck.thy Wed May 20 12:10:22 2009 +0200
@@ -176,66 +176,6 @@
end
-subsection {* Type copies *}
-
-setup {*
-let
-
-fun mk_random_typecopy tyco vs constr typ thy =
- let
- val Ts = map TFree vs;
- val T = Type (tyco, Ts);
- fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
- val Ttm = mk_termifyT T;
- val typtm = mk_termifyT typ;
- fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
- fun mk_random T = mk_const @{const_name random} [T];
- val size = @{term "k\<Colon>code_numeral"};
- val v = "x";
- val t_v = Free (v, typtm);
- val t_constr = mk_const constr Ts;
- val lhs = mk_random T $ size;
- val rhs = HOLogic.mk_ST [((mk_random typ $ size, @{typ Random.seed}), SOME (v, typtm))]
- (HOLogic.mk_return Ttm @{typ Random.seed}
- (mk_const "Code_Eval.valapp" [typ, T]
- $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
- @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
-
-fun ensure_random_typecopy tyco thy =
- let
- val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
- TypecopyPackage.get_info thy tyco;
- val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
- val typ = map_atyps (fn TFree (v, sort) =>
- TFree (v, constrain sort @{sort random})) raw_typ;
- val vs' = Term.add_tfreesT typ [];
- val vs = map (fn (v, sort) =>
- (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
- val do_inst = can (Sign.of_sort thy) (typ, @{sort random});
- in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
-
-in
-
-TypecopyPackage.interpretation ensure_random_typecopy
-
-end
-*}
-
-
-subsection {* Datatypes *}
-
-text {* under construction *}
-
-
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)