src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 39541 6605c1e87c7f
parent 39383 ddfafa97da2f
child 39657 5e57675b7e40
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 20 09:19:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 20 09:26:15 2010 +0200
     1.3 @@ -148,6 +148,8 @@
     1.4    val remove_equalities : theory -> thm -> thm
     1.5    val remove_pointless_clauses : thm -> thm list
     1.6    val peephole_optimisation : theory -> thm -> thm option
     1.7 +  val define_quickcheck_predicate :
     1.8 +    term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory 
     1.9  end;
    1.10  
    1.11  structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
    1.12 @@ -909,4 +911,34 @@
    1.13        (process_False (process_True (prop_of (process intro))))
    1.14    end
    1.15  
    1.16 +(* defining a quickcheck predicate *)
    1.17 +
    1.18 +fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
    1.19 +  | strip_imp_prems _ = [];
    1.20 +
    1.21 +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
    1.22 +  | strip_imp_concl A = A : term;
    1.23 +
    1.24 +fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    1.25 +
    1.26 +fun define_quickcheck_predicate t thy =
    1.27 +  let
    1.28 +    val (vs, t') = strip_abs t
    1.29 +    val vs' = Variable.variant_frees (ProofContext.init_global thy) [] vs
    1.30 +    val t'' = subst_bounds (map Free (rev vs'), t')
    1.31 +    val (prems, concl) = strip_horn t''
    1.32 +    val constname = "quickcheck"
    1.33 +    val full_constname = Sign.full_bname thy constname
    1.34 +    val constT = map snd vs' ---> @{typ bool}
    1.35 +    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
    1.36 +    val const = Const (full_constname, constT)
    1.37 +    val t = Logic.list_implies
    1.38 +      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    1.39 +       HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
    1.40 +    val tac = fn _ => Skip_Proof.cheat_tac thy1
    1.41 +    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
    1.42 +  in
    1.43 +    ((((full_constname, constT), vs'), intro), thy1)
    1.44 +  end
    1.45 +
    1.46  end;