including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
authorbulwahn
Tue Oct 27 09:02:22 2009 +0100 (2009-10-27)
changeset 332505c2af18a3237
parent 33218 ecb5cd453ef2
child 33251 4b13ab778b78
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/Predicate_Compile.thy
src/HOL/Quickcheck.thy
src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML
src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML
src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML
src/HOL/Tools/Predicate_Compile/pred_compile_set.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML
src/HOL/ex/Predicate_Compile.thy
src/HOL/ex/Predicate_Compile_Alternative_Defs.thy
src/HOL/ex/Predicate_Compile_Quickcheck.thy
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Oct 26 23:27:24 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 27 09:02:22 2009 +0100
     1.3 @@ -255,6 +255,7 @@
     1.4    Map.thy \
     1.5    Nat_Numeral.thy \
     1.6    Presburger.thy \
     1.7 +  Predicate_Compile.thy \
     1.8    Quickcheck.thy \
     1.9    Random.thy \
    1.10    Recdef.thy \
    1.11 @@ -283,6 +284,13 @@
    1.12    Tools/numeral_simprocs.ML \
    1.13    Tools/numeral_syntax.ML \
    1.14    Tools/polyhash.ML \
    1.15 +  Tools/Predicate_Compile/predicate_compile_aux.ML \
    1.16 +  Tools/Predicate_Compile/predicate_compile_core.ML \
    1.17 +  Tools/Predicate_Compile/predicate_compile_data.ML \
    1.18 +  Tools/Predicate_Compile/predicate_compile_fun.ML \
    1.19 +  Tools/Predicate_Compile/predicate_compile.ML \
    1.20 +  Tools/Predicate_Compile/predicate_compile_pred.ML \
    1.21 +  Tools/Predicate_Compile/predicate_compile_set.ML \
    1.22    Tools/quickcheck_generators.ML \
    1.23    Tools/Qelim/cooper_data.ML \
    1.24    Tools/Qelim/cooper.ML \
    1.25 @@ -945,7 +953,7 @@
    1.26    ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
    1.27    ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
    1.28    ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
    1.29 -  ex/Predicate_Compile.thy ex/Predicate_Compile_ex.thy			\
    1.30 +  ex/Predicate_Compile_ex.thy			\
    1.31    ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
    1.32    ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
    1.33    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
     2.1 --- a/src/HOL/Main.thy	Mon Oct 26 23:27:24 2009 +0100
     2.2 +++ b/src/HOL/Main.thy	Tue Oct 27 09:02:22 2009 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  header {* Main HOL *}
     2.5  
     2.6  theory Main
     2.7 -imports Plain Nitpick Quickcheck Recdef
     2.8 +imports Plain Nitpick Predicate_Compile Recdef
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Predicate_Compile.thy	Tue Oct 27 09:02:22 2009 +0100
     3.3 @@ -0,0 +1,19 @@
     3.4 +(* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* A compiler for predicates defined by introduction rules *}
     3.7 +
     3.8 +theory Predicate_Compile
     3.9 +imports Quickcheck
    3.10 +uses
    3.11 +  "Tools/Predicate_Compile/predicate_compile_aux.ML"
    3.12 +  "Tools/Predicate_Compile/predicate_compile_core.ML"
    3.13 +  "Tools/Predicate_Compile/predicate_compile_set.ML"
    3.14 +  "Tools/Predicate_Compile/predicate_compile_data.ML"
    3.15 +  "Tools/Predicate_Compile/predicate_compile_fun.ML"
    3.16 +  "Tools/Predicate_Compile/predicate_compile_pred.ML"
    3.17 +  "Tools/Predicate_Compile/predicate_compile.ML"
    3.18 +begin
    3.19 +
    3.20 +setup {* Predicate_Compile.setup *}
    3.21 +
    3.22 +end
    3.23 \ No newline at end of file
     4.1 --- a/src/HOL/Quickcheck.thy	Mon Oct 26 23:27:24 2009 +0100
     4.2 +++ b/src/HOL/Quickcheck.thy	Tue Oct 27 09:02:22 2009 +0100
     4.3 @@ -126,6 +126,47 @@
     4.4    shows "random_aux k = rhs k"
     4.5    using assms by (rule code_numeral.induct)
     4.6  
     4.7 +subsection {* the Random-Predicate Monad *} 
     4.8 +
     4.9 +types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
    4.10 +
    4.11 +definition empty :: "'a randompred"
    4.12 +  where "empty = Pair (bot_class.bot)"
    4.13 +
    4.14 +definition single :: "'a => 'a randompred"
    4.15 +  where "single x = Pair (Predicate.single x)"
    4.16 +
    4.17 +definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred"
    4.18 +  where
    4.19 +    "bind R f = (\<lambda>s. let
    4.20 +       (P, s') = R s;
    4.21 +       (s1, s2) = Random.split_seed s'
    4.22 +     in (Predicate.bind P (%a. fst (f a s1)), s2))"
    4.23 +
    4.24 +definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred"
    4.25 +where
    4.26 +  "union R1 R2 = (\<lambda>s. let
    4.27 +     (P1, s') = R1 s; (P2, s'') = R2 s'
    4.28 +   in (upper_semilattice_class.sup P1 P2, s''))"
    4.29 +
    4.30 +definition if_randompred :: "bool \<Rightarrow> unit randompred"
    4.31 +where
    4.32 +  "if_randompred b = (if b then single () else empty)"
    4.33 +
    4.34 +definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
    4.35 +where
    4.36 +  "not_randompred P = (\<lambda>s. let
    4.37 +     (P', s') = P s
    4.38 +   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
    4.39 +
    4.40 +definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred"
    4.41 +  where "Random g = scomp g (Pair o (Predicate.single o fst))"
    4.42 +
    4.43 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
    4.44 +  where "map f P = bind P (single o f)"
    4.45 +
    4.46 +subsection {* Code setup *}
    4.47 +
    4.48  use "Tools/quickcheck_generators.ML"
    4.49  setup {* Quickcheck_Generators.setup *}
    4.50  
    4.51 @@ -137,7 +178,9 @@
    4.52  code_reserved Quickcheck Quickcheck_Generators
    4.53  
    4.54  
    4.55 +hide (open) type randompred
    4.56  hide (open) const random collapse beyond random_fun_aux random_fun_lift
    4.57 +  empty single bind union if_randompred not_randompred Random map
    4.58  
    4.59  no_notation fcomp (infixl "o>" 60)
    4.60  no_notation scomp (infixl "o\<rightarrow>" 60)
     5.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Mon Oct 26 23:27:24 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,236 +0,0 @@
     5.4 -(* Author: Lukas Bulwahn, TU Muenchen
     5.5 -
     5.6 -Auxilary functions for predicate compiler
     5.7 -*)
     5.8 -
     5.9 -structure Predicate_Compile_Aux =
    5.10 -struct
    5.11 -
    5.12 -(* general syntactic functions *)
    5.13 -
    5.14 -(*Like dest_conj, but flattens conjunctions however nested*)
    5.15 -fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    5.16 -  | conjuncts_aux t conjs = t::conjs;
    5.17 -
    5.18 -fun conjuncts t = conjuncts_aux t [];
    5.19 -
    5.20 -(* syntactic functions *)
    5.21 -
    5.22 -fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    5.23 -  | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
    5.24 -  | is_equationlike_term _ = false
    5.25 -  
    5.26 -val is_equationlike = is_equationlike_term o prop_of 
    5.27 -
    5.28 -fun is_pred_equation_term (Const ("==", _) $ u $ v) =
    5.29 -  (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
    5.30 -  | is_pred_equation_term _ = false
    5.31 -  
    5.32 -val is_pred_equation = is_pred_equation_term o prop_of 
    5.33 -
    5.34 -fun is_intro_term constname t =
    5.35 -  case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
    5.36 -    Const (c, _) => c = constname
    5.37 -  | _ => false
    5.38 -  
    5.39 -fun is_intro constname t = is_intro_term constname (prop_of t)
    5.40 -
    5.41 -fun is_pred thy constname =
    5.42 -  let
    5.43 -    val T = (Sign.the_const_type thy constname)
    5.44 -  in body_type T = @{typ "bool"} end;
    5.45 -  
    5.46 -
    5.47 -fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
    5.48 -  | is_predT _ = false
    5.49 -
    5.50 -  
    5.51 -(*** check if a term contains only constructor functions ***)
    5.52 -fun is_constrt thy =
    5.53 -  let
    5.54 -    val cnstrs = flat (maps
    5.55 -      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    5.56 -      (Symtab.dest (Datatype.get_all thy)));
    5.57 -    fun check t = (case strip_comb t of
    5.58 -        (Free _, []) => true
    5.59 -      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
    5.60 -            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
    5.61 -          | _ => false)
    5.62 -      | _ => false)
    5.63 -  in check end;  
    5.64 -  
    5.65 -fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
    5.66 -  let
    5.67 -    val (xTs, t') = strip_ex t
    5.68 -  in
    5.69 -    ((x, T) :: xTs, t')
    5.70 -  end
    5.71 -  | strip_ex t = ([], t)
    5.72 -
    5.73 -fun focus_ex t nctxt =
    5.74 -  let
    5.75 -    val ((xs, Ts), t') = apfst split_list (strip_ex t) 
    5.76 -    val (xs', nctxt') = Name.variants xs nctxt;
    5.77 -    val ps' = xs' ~~ Ts;
    5.78 -    val vs = map Free ps';
    5.79 -    val t'' = Term.subst_bounds (rev vs, t');
    5.80 -  in ((ps', t''), nctxt') end;
    5.81 -
    5.82 -
    5.83 -(* introduction rule combinators *)
    5.84 -
    5.85 -(* combinators to apply a function to all literals of an introduction rules *)
    5.86 -
    5.87 -fun map_atoms f intro = 
    5.88 -  let
    5.89 -    val (literals, head) = Logic.strip_horn intro
    5.90 -    fun appl t = (case t of
    5.91 -        (@{term "Not"} $ t') => HOLogic.mk_not (f t')
    5.92 -      | _ => f t)
    5.93 -  in
    5.94 -    Logic.list_implies
    5.95 -      (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
    5.96 -  end
    5.97 -
    5.98 -fun fold_atoms f intro s =
    5.99 -  let
   5.100 -    val (literals, head) = Logic.strip_horn intro
   5.101 -    fun appl t s = (case t of
   5.102 -      (@{term "Not"} $ t') => f t' s
   5.103 -      | _ => f t s)
   5.104 -  in fold appl (map HOLogic.dest_Trueprop literals) s end
   5.105 -
   5.106 -fun fold_map_atoms f intro s =
   5.107 -  let
   5.108 -    val (literals, head) = Logic.strip_horn intro
   5.109 -    fun appl t s = (case t of
   5.110 -      (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
   5.111 -      | _ => f t s)
   5.112 -    val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
   5.113 -  in
   5.114 -    (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
   5.115 -  end;
   5.116 -
   5.117 -fun maps_premises f intro =
   5.118 -  let
   5.119 -    val (premises, head) = Logic.strip_horn intro
   5.120 -  in
   5.121 -    Logic.list_implies (maps f premises, head)
   5.122 -  end
   5.123 -  
   5.124 -(* lifting term operations to theorems *)
   5.125 -
   5.126 -fun map_term thy f th =
   5.127 -  Skip_Proof.make_thm thy (f (prop_of th))
   5.128 -
   5.129 -(*
   5.130 -fun equals_conv lhs_cv rhs_cv ct =
   5.131 -  case Thm.term_of ct of
   5.132 -    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct  
   5.133 -  | _ => error "equals_conv"  
   5.134 -*)
   5.135 -
   5.136 -(* Different options for compiler *)
   5.137 -
   5.138 -datatype options = Options of {  
   5.139 -  expected_modes : (string * int list list) option,
   5.140 -  show_steps : bool,
   5.141 -  show_mode_inference : bool,
   5.142 -  show_proof_trace : bool,
   5.143 -  show_intermediate_results : bool,
   5.144 -  show_compilation : bool,
   5.145 -  skip_proof : bool,
   5.146 -
   5.147 -  inductify : bool,
   5.148 -  rpred : bool,
   5.149 -  depth_limited : bool
   5.150 -};
   5.151 -
   5.152 -fun expected_modes (Options opt) = #expected_modes opt
   5.153 -fun show_steps (Options opt) = #show_steps opt
   5.154 -fun show_mode_inference (Options opt) = #show_mode_inference opt
   5.155 -fun show_intermediate_results (Options opt) = #show_intermediate_results opt
   5.156 -fun show_proof_trace (Options opt) = #show_proof_trace opt
   5.157 -fun show_compilation (Options opt) = #show_compilation opt
   5.158 -fun skip_proof (Options opt) = #skip_proof opt
   5.159 -
   5.160 -fun is_inductify (Options opt) = #inductify opt
   5.161 -fun is_rpred (Options opt) = #rpred opt
   5.162 -fun is_depth_limited (Options opt) = #depth_limited opt
   5.163 -
   5.164 -val default_options = Options {
   5.165 -  expected_modes = NONE,
   5.166 -  show_steps = false,
   5.167 -  show_intermediate_results = false,
   5.168 -  show_proof_trace = false,
   5.169 -  show_mode_inference = false,
   5.170 -  show_compilation = false,
   5.171 -  skip_proof = false,
   5.172 -  
   5.173 -  inductify = false,
   5.174 -  rpred = false,
   5.175 -  depth_limited = false
   5.176 -}
   5.177 -
   5.178 -
   5.179 -fun print_step options s =
   5.180 -  if show_steps options then tracing s else ()
   5.181 -
   5.182 -(* tuple processing *)
   5.183 -
   5.184 -fun expand_tuples thy intro =
   5.185 -  let
   5.186 -    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
   5.187 -      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
   5.188 -      (case HOLogic.strip_tupleT (fastype_of arg) of
   5.189 -        (Ts as _ :: _ :: _) =>
   5.190 -        let
   5.191 -          fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
   5.192 -            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
   5.193 -            | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
   5.194 -              let
   5.195 -                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
   5.196 -                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
   5.197 -                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
   5.198 -                val args' = map (Pattern.rewrite_term thy [pat] []) args
   5.199 -              in
   5.200 -                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
   5.201 -              end
   5.202 -            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
   5.203 -          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
   5.204 -            (args, (pats, intro_t, ctxt))
   5.205 -        in
   5.206 -          rewrite_args args' (pats, intro_t', ctxt')
   5.207 -        end
   5.208 -      | _ => rewrite_args args (pats, intro_t, ctxt))
   5.209 -    fun rewrite_prem atom =
   5.210 -      let
   5.211 -        val (_, args) = strip_comb atom
   5.212 -      in rewrite_args args end
   5.213 -    val ctxt = ProofContext.init thy
   5.214 -    val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
   5.215 -    val intro_t = prop_of intro'
   5.216 -    val concl = Logic.strip_imp_concl intro_t
   5.217 -    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
   5.218 -    val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
   5.219 -    val (pats', intro_t', ctxt3) = 
   5.220 -      fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
   5.221 -    fun rewrite_pat (ct1, ct2) =
   5.222 -      (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
   5.223 -    val t_insts' = map rewrite_pat t_insts
   5.224 -    val intro'' = Thm.instantiate (T_insts, t_insts') intro
   5.225 -    val [intro'''] = Variable.export ctxt3 ctxt [intro'']
   5.226 -    val intro'''' = Simplifier.full_simplify
   5.227 -      (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
   5.228 -      intro'''
   5.229 -    (* splitting conjunctions introduced by Pair_eq*)
   5.230 -    fun split_conj prem =
   5.231 -      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
   5.232 -    val intro''''' = map_term thy (maps_premises split_conj) intro''''
   5.233 -  in
   5.234 -    intro'''''
   5.235 -  end
   5.236 -
   5.237 -
   5.238 -
   5.239 -end;
     6.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Mon Oct 26 23:27:24 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,210 +0,0 @@
     6.4 -(* Author: Lukas Bulwahn, TU Muenchen
     6.5 -
     6.6 -Book-keeping datastructure for the predicate compiler
     6.7 -
     6.8 -*)
     6.9 -signature PREDICATE_COMPILE_DATA =
    6.10 -sig
    6.11 -  type specification_table;
    6.12 -  val make_const_spec_table : theory -> specification_table
    6.13 -  val get_specification :  specification_table -> string -> thm list
    6.14 -  val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T
    6.15 -  val normalize_equation : theory -> thm -> thm
    6.16 -end;
    6.17 -
    6.18 -structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =
    6.19 -struct
    6.20 -
    6.21 -open Predicate_Compile_Aux;
    6.22 -
    6.23 -structure Data = TheoryDataFun
    6.24 -(
    6.25 -  type T =
    6.26 -    {const_spec_table : thm list Symtab.table};
    6.27 -  val empty =
    6.28 -    {const_spec_table = Symtab.empty};
    6.29 -  val copy = I;
    6.30 -  val extend = I;
    6.31 -  fun merge _
    6.32 -    ({const_spec_table = const_spec_table1},
    6.33 -     {const_spec_table = const_spec_table2}) =
    6.34 -     {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
    6.35 -);
    6.36 -
    6.37 -fun mk_data c = {const_spec_table = c}
    6.38 -fun map_data f {const_spec_table = c} = mk_data (f c)
    6.39 -
    6.40 -type specification_table = thm list Symtab.table
    6.41 -
    6.42 -fun defining_const_of_introrule_term t =
    6.43 -  let
    6.44 -    val _ $ u = Logic.strip_imp_concl t
    6.45 -    val (pred, all_args) = strip_comb u
    6.46 -  in case pred of
    6.47 -    Const (c, T) => c
    6.48 -    | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
    6.49 -  end
    6.50 -
    6.51 -val defining_const_of_introrule = defining_const_of_introrule_term o prop_of
    6.52 -
    6.53 -(*TODO*)
    6.54 -fun is_introlike_term t = true
    6.55 -
    6.56 -val is_introlike = is_introlike_term o prop_of
    6.57 -
    6.58 -fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
    6.59 -  (case strip_comb u of
    6.60 -    (Const (c, T), args) =>
    6.61 -      if (length (binder_types T) = length args) then
    6.62 -        true
    6.63 -      else
    6.64 -        raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
    6.65 -  | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
    6.66 -  | check_equation_format_term t =
    6.67 -    raise TERM ("check_equation_format_term failed: Not an equation", [t])
    6.68 -
    6.69 -val check_equation_format = check_equation_format_term o prop_of
    6.70 -
    6.71 -fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) =
    6.72 -  (case fst (strip_comb u) of
    6.73 -    Const (c, _) => c
    6.74 -  | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t]))
    6.75 -  | defining_const_of_equation_term t =
    6.76 -    raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
    6.77 -
    6.78 -val defining_const_of_equation = defining_const_of_equation_term o prop_of
    6.79 -
    6.80 -(* Normalizing equations *)
    6.81 -
    6.82 -fun mk_meta_equation th =
    6.83 -  case prop_of th of
    6.84 -    Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
    6.85 -  | _ => th
    6.86 -
    6.87 -val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
    6.88 -
    6.89 -fun full_fun_cong_expand th =
    6.90 -  let
    6.91 -    val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
    6.92 -    val i = length (binder_types (fastype_of f)) - length args
    6.93 -  in funpow i (fn th => th RS meta_fun_cong) th end;
    6.94 -
    6.95 -fun declare_names s xs ctxt =
    6.96 -  let
    6.97 -    val res = Name.names ctxt s xs
    6.98 -  in (res, fold Name.declare (map fst res) ctxt) end
    6.99 -  
   6.100 -fun split_all_pairs thy th =
   6.101 -  let
   6.102 -    val ctxt = ProofContext.init thy
   6.103 -    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
   6.104 -    val t = prop_of th'
   6.105 -    val frees = Term.add_frees t [] 
   6.106 -    val freenames = Term.add_free_names t []
   6.107 -    val nctxt = Name.make_context freenames
   6.108 -    fun mk_tuple_rewrites (x, T) nctxt =
   6.109 -      let
   6.110 -        val Ts = HOLogic.flatten_tupleT T
   6.111 -        val (xTs, nctxt') = declare_names x Ts nctxt
   6.112 -        val paths = HOLogic.flat_tupleT_paths T
   6.113 -      in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
   6.114 -    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
   6.115 -    val t' = Pattern.rewrite_term thy rewr [] t
   6.116 -    val tac = Skip_Proof.cheat_tac thy
   6.117 -    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
   6.118 -    val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
   6.119 -  in
   6.120 -    th'''
   6.121 -  end;
   6.122 -
   6.123 -fun normalize_equation thy th =
   6.124 -  mk_meta_equation th
   6.125 -  |> Predicate_Compile_Set.unfold_set_notation
   6.126 -  |> full_fun_cong_expand
   6.127 -  |> split_all_pairs thy
   6.128 -  |> tap check_equation_format
   6.129 -
   6.130 -fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
   6.131 -((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
   6.132 -
   6.133 -fun store_thm_in_table ignore_consts thy th=
   6.134 -  let
   6.135 -    val th = th
   6.136 -      |> inline_equations thy
   6.137 -      |> Predicate_Compile_Set.unfold_set_notation
   6.138 -      |> AxClass.unoverload thy
   6.139 -    val (const, th) =
   6.140 -      if is_equationlike th then
   6.141 -        let
   6.142 -          val eq = normalize_equation thy th
   6.143 -        in
   6.144 -          (defining_const_of_equation eq, eq)
   6.145 -        end
   6.146 -      else if (is_introlike th) then (defining_const_of_introrule th, th)
   6.147 -      else error "store_thm: unexpected definition format"
   6.148 -  in
   6.149 -    if not (member (op =) ignore_consts const) then
   6.150 -      Symtab.cons_list (const, th)
   6.151 -    else I
   6.152 -  end
   6.153 -
   6.154 -fun make_const_spec_table thy =
   6.155 -  let
   6.156 -    fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
   6.157 -    val table = Symtab.empty
   6.158 -      |> store [] Predicate_Compile_Alternative_Defs.get
   6.159 -    val ignore_consts = Symtab.keys table
   6.160 -  in
   6.161 -    table
   6.162 -    |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
   6.163 -    |> store ignore_consts Nitpick_Simps.get
   6.164 -    |> store ignore_consts Nitpick_Intros.get
   6.165 -  end
   6.166 -
   6.167 -fun get_specification table constname =
   6.168 -  case Symtab.lookup table constname of
   6.169 -    SOME thms => thms
   6.170 -  | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
   6.171 -
   6.172 -val logic_operator_names =
   6.173 -  [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, 
   6.174 -   @{const_name "op &"}]
   6.175 -
   6.176 -val special_cases = member (op =) [
   6.177 -    @{const_name "False"},
   6.178 -    @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
   6.179 -    @{const_name Nat.one_nat_inst.one_nat},
   6.180 -@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
   6.181 -@{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
   6.182 -@{const_name Nat.ord_nat_inst.less_eq_nat},
   6.183 -@{const_name number_nat_inst.number_of_nat},
   6.184 -  @{const_name Int.Bit0},
   6.185 -  @{const_name Int.Bit1},
   6.186 -  @{const_name Int.Pls},
   6.187 -@{const_name "Int.zero_int_inst.zero_int"},
   6.188 -@{const_name "List.filter"}]
   6.189 -
   6.190 -fun case_consts thy s = is_some (Datatype.info_of_case thy s)
   6.191 -
   6.192 -fun obtain_specification_graph thy table constname =
   6.193 -  let
   6.194 -    fun is_nondefining_constname c = member (op =) logic_operator_names c
   6.195 -    val is_defining_constname = member (op =) (Symtab.keys table)
   6.196 -    fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c)
   6.197 -    fun defiants_of specs =
   6.198 -      fold (Term.add_const_names o prop_of) specs []
   6.199 -      |> filter is_defining_constname
   6.200 -      |> filter_out is_nondefining_constname
   6.201 -      |> filter_out has_code_pred_intros
   6.202 -      |> filter_out (case_consts thy)
   6.203 -      |> filter_out special_cases
   6.204 -    fun extend constname =
   6.205 -      let
   6.206 -        val specs = get_specification table constname
   6.207 -      in (specs, defiants_of specs) end;
   6.208 -  in
   6.209 -    Graph.extend extend constname Graph.empty
   6.210 -  end;
   6.211 -  
   6.212 -  
   6.213 -end;
     7.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Mon Oct 26 23:27:24 2009 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,189 +0,0 @@
     7.4 -(* Author: Lukas Bulwahn, TU Muenchen
     7.5 -
     7.6 -Preprocessing definitions of predicates to introduction rules
     7.7 -*)
     7.8 -
     7.9 -signature PREDICATE_COMPILE_PRED =
    7.10 -sig
    7.11 -  (* preprocesses an equation to a set of intro rules; defines new constants *)
    7.12 -  (*
    7.13 -  val preprocess_pred_equation : thm -> theory -> thm list * theory
    7.14 -  *)
    7.15 -  val preprocess : string -> theory -> (thm list list * theory) 
    7.16 -  (* output is the term list of clauses of an unknown predicate *)
    7.17 -  val preprocess_term : term -> theory -> (term list * theory)
    7.18 -  
    7.19 -  (*val rewrite : thm -> thm*)
    7.20 -  
    7.21 -end;
    7.22 -(* : PREDICATE_COMPILE_PREPROC_PRED *)
    7.23 -structure Predicate_Compile_Pred =
    7.24 -struct
    7.25 -
    7.26 -open Predicate_Compile_Aux
    7.27 -
    7.28 -fun is_compound ((Const ("Not", _)) $ t) =
    7.29 -    error "is_compound: Negation should not occur; preprocessing is defect"
    7.30 -  | is_compound ((Const ("Ex", _)) $ _) = true
    7.31 -  | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
    7.32 -  | is_compound ((Const ("op &", _)) $ _ $ _) =
    7.33 -    error "is_compound: Conjunction should not occur; preprocessing is defect"
    7.34 -  | is_compound _ = false
    7.35 -
    7.36 -fun flatten constname atom (defs, thy) =
    7.37 -  if is_compound atom then
    7.38 -    let
    7.39 -      val constname = Name.variant (map (Long_Name.base_name o fst) defs)
    7.40 -        ((Long_Name.base_name constname) ^ "_aux")
    7.41 -      val full_constname = Sign.full_bname thy constname
    7.42 -      val (params, args) = List.partition (is_predT o fastype_of)
    7.43 -        (map Free (Term.add_frees atom []))
    7.44 -      val constT = map fastype_of (params @ args) ---> HOLogic.boolT
    7.45 -      val lhs = list_comb (Const (full_constname, constT), params @ args)
    7.46 -      val def = Logic.mk_equals (lhs, atom)
    7.47 -      val ([definition], thy') = thy
    7.48 -        |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
    7.49 -        |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
    7.50 -    in
    7.51 -      (lhs, ((full_constname, [definition]) :: defs, thy'))
    7.52 -    end
    7.53 -  else
    7.54 -    (atom, (defs, thy))
    7.55 -
    7.56 -fun flatten_intros constname intros thy =
    7.57 -  let
    7.58 -    val ctxt = ProofContext.init thy
    7.59 -    val ((_, intros), ctxt') = Variable.import true intros ctxt
    7.60 -    val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
    7.61 -      (flatten constname) (map prop_of intros) ([], thy)
    7.62 -    val tac = fn _ => Skip_Proof.cheat_tac thy'
    7.63 -    val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
    7.64 -      |> Variable.export ctxt' ctxt
    7.65 -  in
    7.66 -    (intros'', (local_defs, thy'))
    7.67 -  end
    7.68 -
    7.69 -(* TODO: same function occurs in inductive package *)
    7.70 -fun select_disj 1 1 = []
    7.71 -  | select_disj _ 1 = [rtac @{thm disjI1}]
    7.72 -  | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
    7.73 -
    7.74 -fun introrulify thy ths = 
    7.75 -  let
    7.76 -    val ctxt = ProofContext.init thy
    7.77 -    val ((_, ths'), ctxt') = Variable.import true ths ctxt
    7.78 -    fun introrulify' th =
    7.79 -      let
    7.80 -        val (lhs, rhs) = Logic.dest_equals (prop_of th)
    7.81 -        val frees = Term.add_free_names rhs []
    7.82 -        val disjuncts = HOLogic.dest_disj rhs
    7.83 -        val nctxt = Name.make_context frees
    7.84 -        fun mk_introrule t =
    7.85 -          let
    7.86 -            val ((ps, t'), nctxt') = focus_ex t nctxt
    7.87 -            val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
    7.88 -          in
    7.89 -            (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
    7.90 -          end
    7.91 -        val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
    7.92 -          Logic.dest_implies o prop_of) @{thm exI}
    7.93 -        fun prove_introrule (index, (ps, introrule)) =
    7.94 -          let
    7.95 -            val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1
    7.96 -              THEN EVERY1 (select_disj (length disjuncts) (index + 1)) 
    7.97 -              THEN (EVERY (map (fn y =>
    7.98 -                rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
    7.99 -              THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
   7.100 -              THEN TRY (atac 1)
   7.101 -          in
   7.102 -            Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
   7.103 -          end
   7.104 -      in
   7.105 -        map_index prove_introrule (map mk_introrule disjuncts)
   7.106 -      end
   7.107 -  in maps introrulify' ths' |> Variable.export ctxt' ctxt end
   7.108 -
   7.109 -val rewrite =
   7.110 -  Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}])
   7.111 -  #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) 
   7.112 -  #> Conv.fconv_rule nnf_conv 
   7.113 -  #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
   7.114 -
   7.115 -val rewrite_intros =
   7.116 -  Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)})
   7.117 -
   7.118 -fun preprocess (constname, specs) thy =
   7.119 -  let
   7.120 -    val ctxt = ProofContext.init thy
   7.121 -      val intros =
   7.122 -      if forall is_pred_equation specs then 
   7.123 -        introrulify thy (map rewrite specs)
   7.124 -      else if forall (is_intro constname) specs then
   7.125 -        map rewrite_intros specs
   7.126 -      else
   7.127 -        error ("unexpected specification for constant " ^ quote constname ^ ":\n"
   7.128 -          ^ commas (map (quote o Display.string_of_thm_global thy) specs))
   7.129 -    val (intros', (local_defs, thy')) = flatten_intros constname intros thy
   7.130 -    val (intross, thy'') = fold_map preprocess local_defs thy'
   7.131 -  in
   7.132 -    ((constname, intros') :: flat intross,thy'')
   7.133 -  end;
   7.134 -
   7.135 -fun preprocess_term t thy = error "preprocess_pred_term: to implement" 
   7.136 -
   7.137 -fun is_Abs (Abs _) = true
   7.138 -  | is_Abs _       = false
   7.139 -
   7.140 -fun flat_higher_order_arguments (intross, thy) =
   7.141 -  let
   7.142 -    fun process constname atom (new_defs, thy) =
   7.143 -      let
   7.144 -        val (pred, args) = strip_comb atom
   7.145 -        val abs_args = filter is_Abs args
   7.146 -        fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
   7.147 -          let
   7.148 -            val _ = tracing ("Introduce new constant for " ^
   7.149 -              Syntax.string_of_term_global thy abs_arg)
   7.150 -            val vars = map Var (Term.add_vars abs_arg [])
   7.151 -            val abs_arg' = Logic.unvarify abs_arg
   7.152 -            val frees = map Free (Term.add_frees abs_arg' [])
   7.153 -            val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
   7.154 -              ((Long_Name.base_name constname) ^ "_hoaux")
   7.155 -            val full_constname = Sign.full_bname thy constname
   7.156 -            val constT = map fastype_of frees ---> (fastype_of abs_arg')
   7.157 -            val const = Const (full_constname, constT)
   7.158 -            val lhs = list_comb (const, frees)
   7.159 -            val def = Logic.mk_equals (lhs, abs_arg')
   7.160 -            val _ = tracing (Syntax.string_of_term_global thy def)
   7.161 -            val ([definition], thy') = thy
   7.162 -              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   7.163 -              |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
   7.164 -          in
   7.165 -            (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
   7.166 -          end
   7.167 -        | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy))
   7.168 -        val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
   7.169 -      in
   7.170 -        (list_comb (pred, args'), (new_defs', thy'))
   7.171 -      end
   7.172 -    fun flat_intro intro (new_defs, thy) =
   7.173 -      let
   7.174 -        val constname = fst (dest_Const (fst (strip_comb
   7.175 -          (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
   7.176 -        val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
   7.177 -        val th = Skip_Proof.make_thm thy intro_ts
   7.178 -      in
   7.179 -        (th, (new_defs, thy))
   7.180 -      end
   7.181 -    fun fold_map_spec f [] s = ([], s)
   7.182 -      | fold_map_spec f ((c, ths) :: specs) s =
   7.183 -        let
   7.184 -          val (ths', s') = f ths s
   7.185 -          val (specs', s'') = fold_map_spec f specs s'
   7.186 -        in ((c, ths') :: specs', s'') end
   7.187 -    val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy)
   7.188 -  in
   7.189 -    (intross', (new_defs, thy'))
   7.190 -  end
   7.191 -
   7.192 -end;
     8.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Mon Oct 26 23:27:24 2009 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,96 +0,0 @@
     8.4 -(* Author: Lukas Bulwahn, TU Muenchen
     8.5 -
     8.6 -A quickcheck generator based on the predicate compiler
     8.7 -*)
     8.8 -
     8.9 -signature PREDICATE_COMPILE_QUICKCHECK =
    8.10 -sig
    8.11 -  val quickcheck : Proof.context -> term -> int -> term list option
    8.12 -  val test_ref :
    8.13 -    ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
    8.14 -end;
    8.15 -
    8.16 -structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
    8.17 -struct
    8.18 -
    8.19 -val test_ref =
    8.20 -  Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
    8.21 -
    8.22 -val target = "Quickcheck"
    8.23 -
    8.24 -fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
    8.25 -val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
    8.26 -val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
    8.27 -val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
    8.28 -val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
    8.29 -val lift_pred = #lift_pred (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
    8.30 -
    8.31 -fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
    8.32 -  | mk_split_lambda [x] t = lambda x t
    8.33 -  | mk_split_lambda xs t =
    8.34 -  let
    8.35 -    fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
    8.36 -      | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
    8.37 -  in
    8.38 -    mk_split_lambda' xs t
    8.39 -  end;
    8.40 -
    8.41 -fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B
    8.42 -  | strip_imp_prems _ = [];
    8.43 -
    8.44 -fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B
    8.45 -  | strip_imp_concl A = A : term;
    8.46 -
    8.47 -fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    8.48 -
    8.49 -fun quickcheck ctxt t =
    8.50 -  let
    8.51 -    val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t))
    8.52 -    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
    8.53 -    val thy = (ProofContext.theory_of ctxt') 
    8.54 -    val (vs, t') = strip_abs t
    8.55 -    val vs' = Variable.variant_frees ctxt' [] vs
    8.56 -    val t'' = subst_bounds (map Free (rev vs'), t')
    8.57 -    val (prems, concl) = strip_horn t''
    8.58 -    val constname = "pred_compile_quickcheck"
    8.59 -    val full_constname = Sign.full_bname thy constname
    8.60 -    val constT = map snd vs' ---> @{typ bool}
    8.61 -    val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
    8.62 -    val t = Logic.list_implies
    8.63 -      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    8.64 -       HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
    8.65 -    val tac = fn _ => Skip_Proof.cheat_tac thy'
    8.66 -    val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
    8.67 -    val _ = tracing (Display.string_of_thm ctxt' intro)
    8.68 -    val thy'' = thy'
    8.69 -      |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
    8.70 -      |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
    8.71 -      (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*)
    8.72 -      (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
    8.73 -      (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *)
    8.74 -    val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
    8.75 -    val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  
    8.76 -    val prog =
    8.77 -      if member (op =) modes ([], []) then
    8.78 -        let
    8.79 -          val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
    8.80 -          val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
    8.81 -          in Const (name, T) $ @{term True} $ Bound 0 end
    8.82 -      else if member (op =) depth_limited_modes ([], []) then
    8.83 -        let
    8.84 -          val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
    8.85 -          val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
    8.86 -        in lift_pred (Const (name, T) $ Bound 0) end
    8.87 -      else error "Predicate Compile Quickcheck failed"
    8.88 -    val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog,
    8.89 -      mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
    8.90 -      (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
    8.91 -    val _ = tracing (Syntax.string_of_term ctxt' qc_term)
    8.92 -    val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
    8.93 -      (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
    8.94 -      thy'' qc_term []
    8.95 -  in
    8.96 -    ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield))
    8.97 -  end
    8.98 -
    8.99 -end;
     9.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Mon Oct 26 23:27:24 2009 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,52 +0,0 @@
     9.4 -(* Author: Lukas Bulwahn, TU Muenchen
     9.5 -
     9.6 -Preprocessing sets to predicates
     9.7 -*)
     9.8 -
     9.9 -signature PREDICATE_COMPILE_SET =
    9.10 -sig
    9.11 -(*
    9.12 -  val preprocess_intro : thm -> theory -> thm * theory
    9.13 -  val preprocess_clause : term -> theory -> term * theory
    9.14 -*)
    9.15 -  val unfold_set_notation : thm -> thm;
    9.16 -end;
    9.17 -
    9.18 -structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
    9.19 -struct
    9.20 -(*FIXME: unfolding Ball in pretty adhoc here *)
    9.21 -val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
    9.22 -@{thm Ball_def}, @{thm Bex_def}]
    9.23 -
    9.24 -val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
    9.25 -
    9.26 -(*
    9.27 -fun find_set_theorems ctxt cname =
    9.28 -  let
    9.29 -    val _ = cname 
    9.30 -*)
    9.31 -
    9.32 -(*
    9.33 -fun preprocess_term t ctxt =
    9.34 -  case t of
    9.35 -    Const ("op :", _) $ x $ A => 
    9.36 -      case strip_comb A of
    9.37 -        (Const (cname, T), params) =>
    9.38 -          let 
    9.39 -            val _ = find_set_theorems
    9.40 -          in
    9.41 -            (t, ctxt)
    9.42 -          end
    9.43 -      | _ => (t, ctxt)  
    9.44 -  | _ => (t, ctxt)
    9.45 -*) 
    9.46 -(*
    9.47 -fun preprocess_intro th thy =
    9.48 -  let
    9.49 -    val cnames = find_heads_of_prems
    9.50 -    val set_cname = filter (has_set_definition
    9.51 -    val _ = define_preds
    9.52 -    val _ = prep_pred_def
    9.53 -  in
    9.54 -*)
    9.55 -end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 27 09:02:22 2009 +0100
    10.3 @@ -0,0 +1,236 @@
    10.4 +(* Author: Lukas Bulwahn, TU Muenchen
    10.5 +
    10.6 +Auxilary functions for predicate compiler
    10.7 +*)
    10.8 +
    10.9 +structure Predicate_Compile_Aux =
   10.10 +struct
   10.11 +
   10.12 +(* general syntactic functions *)
   10.13 +
   10.14 +(*Like dest_conj, but flattens conjunctions however nested*)
   10.15 +fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
   10.16 +  | conjuncts_aux t conjs = t::conjs;
   10.17 +
   10.18 +fun conjuncts t = conjuncts_aux t [];
   10.19 +
   10.20 +(* syntactic functions *)
   10.21 +
   10.22 +fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
   10.23 +  | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
   10.24 +  | is_equationlike_term _ = false
   10.25 +  
   10.26 +val is_equationlike = is_equationlike_term o prop_of 
   10.27 +
   10.28 +fun is_pred_equation_term (Const ("==", _) $ u $ v) =
   10.29 +  (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
   10.30 +  | is_pred_equation_term _ = false
   10.31 +  
   10.32 +val is_pred_equation = is_pred_equation_term o prop_of 
   10.33 +
   10.34 +fun is_intro_term constname t =
   10.35 +  case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
   10.36 +    Const (c, _) => c = constname
   10.37 +  | _ => false
   10.38 +  
   10.39 +fun is_intro constname t = is_intro_term constname (prop_of t)
   10.40 +
   10.41 +fun is_pred thy constname =
   10.42 +  let
   10.43 +    val T = (Sign.the_const_type thy constname)
   10.44 +  in body_type T = @{typ "bool"} end;
   10.45 +  
   10.46 +
   10.47 +fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
   10.48 +  | is_predT _ = false
   10.49 +
   10.50 +  
   10.51 +(*** check if a term contains only constructor functions ***)
   10.52 +fun is_constrt thy =
   10.53 +  let
   10.54 +    val cnstrs = flat (maps
   10.55 +      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
   10.56 +      (Symtab.dest (Datatype.get_all thy)));
   10.57 +    fun check t = (case strip_comb t of
   10.58 +        (Free _, []) => true
   10.59 +      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
   10.60 +            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
   10.61 +          | _ => false)
   10.62 +      | _ => false)
   10.63 +  in check end;  
   10.64 +  
   10.65 +fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
   10.66 +  let
   10.67 +    val (xTs, t') = strip_ex t
   10.68 +  in
   10.69 +    ((x, T) :: xTs, t')
   10.70 +  end
   10.71 +  | strip_ex t = ([], t)
   10.72 +
   10.73 +fun focus_ex t nctxt =
   10.74 +  let
   10.75 +    val ((xs, Ts), t') = apfst split_list (strip_ex t) 
   10.76 +    val (xs', nctxt') = Name.variants xs nctxt;
   10.77 +    val ps' = xs' ~~ Ts;
   10.78 +    val vs = map Free ps';
   10.79 +    val t'' = Term.subst_bounds (rev vs, t');
   10.80 +  in ((ps', t''), nctxt') end;
   10.81 +
   10.82 +
   10.83 +(* introduction rule combinators *)
   10.84 +
   10.85 +(* combinators to apply a function to all literals of an introduction rules *)
   10.86 +
   10.87 +fun map_atoms f intro = 
   10.88 +  let
   10.89 +    val (literals, head) = Logic.strip_horn intro
   10.90 +    fun appl t = (case t of
   10.91 +        (@{term "Not"} $ t') => HOLogic.mk_not (f t')
   10.92 +      | _ => f t)
   10.93 +  in
   10.94 +    Logic.list_implies
   10.95 +      (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
   10.96 +  end
   10.97 +
   10.98 +fun fold_atoms f intro s =
   10.99 +  let
  10.100 +    val (literals, head) = Logic.strip_horn intro
  10.101 +    fun appl t s = (case t of
  10.102 +      (@{term "Not"} $ t') => f t' s
  10.103 +      | _ => f t s)
  10.104 +  in fold appl (map HOLogic.dest_Trueprop literals) s end
  10.105 +
  10.106 +fun fold_map_atoms f intro s =
  10.107 +  let
  10.108 +    val (literals, head) = Logic.strip_horn intro
  10.109 +    fun appl t s = (case t of
  10.110 +      (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
  10.111 +      | _ => f t s)
  10.112 +    val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
  10.113 +  in
  10.114 +    (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
  10.115 +  end;
  10.116 +
  10.117 +fun maps_premises f intro =
  10.118 +  let
  10.119 +    val (premises, head) = Logic.strip_horn intro
  10.120 +  in
  10.121 +    Logic.list_implies (maps f premises, head)
  10.122 +  end
  10.123 +  
  10.124 +(* lifting term operations to theorems *)
  10.125 +
  10.126 +fun map_term thy f th =
  10.127 +  Skip_Proof.make_thm thy (f (prop_of th))
  10.128 +
  10.129 +(*
  10.130 +fun equals_conv lhs_cv rhs_cv ct =
  10.131 +  case Thm.term_of ct of
  10.132 +    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct  
  10.133 +  | _ => error "equals_conv"  
  10.134 +*)
  10.135 +
  10.136 +(* Different options for compiler *)
  10.137 +
  10.138 +datatype options = Options of {  
  10.139 +  expected_modes : (string * int list list) option,
  10.140 +  show_steps : bool,
  10.141 +  show_mode_inference : bool,
  10.142 +  show_proof_trace : bool,
  10.143 +  show_intermediate_results : bool,
  10.144 +  show_compilation : bool,
  10.145 +  skip_proof : bool,
  10.146 +
  10.147 +  inductify : bool,
  10.148 +  rpred : bool,
  10.149 +  depth_limited : bool
  10.150 +};
  10.151 +
  10.152 +fun expected_modes (Options opt) = #expected_modes opt
  10.153 +fun show_steps (Options opt) = #show_steps opt
  10.154 +fun show_mode_inference (Options opt) = #show_mode_inference opt
  10.155 +fun show_intermediate_results (Options opt) = #show_intermediate_results opt
  10.156 +fun show_proof_trace (Options opt) = #show_proof_trace opt
  10.157 +fun show_compilation (Options opt) = #show_compilation opt
  10.158 +fun skip_proof (Options opt) = #skip_proof opt
  10.159 +
  10.160 +fun is_inductify (Options opt) = #inductify opt
  10.161 +fun is_rpred (Options opt) = #rpred opt
  10.162 +fun is_depth_limited (Options opt) = #depth_limited opt
  10.163 +
  10.164 +val default_options = Options {
  10.165 +  expected_modes = NONE,
  10.166 +  show_steps = false,
  10.167 +  show_intermediate_results = false,
  10.168 +  show_proof_trace = false,
  10.169 +  show_mode_inference = false,
  10.170 +  show_compilation = false,
  10.171 +  skip_proof = false,
  10.172 +  
  10.173 +  inductify = false,
  10.174 +  rpred = false,
  10.175 +  depth_limited = false
  10.176 +}
  10.177 +
  10.178 +
  10.179 +fun print_step options s =
  10.180 +  if show_steps options then tracing s else ()
  10.181 +
  10.182 +(* tuple processing *)
  10.183 +
  10.184 +fun expand_tuples thy intro =
  10.185 +  let
  10.186 +    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
  10.187 +      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
  10.188 +      (case HOLogic.strip_tupleT (fastype_of arg) of
  10.189 +        (Ts as _ :: _ :: _) =>
  10.190 +        let
  10.191 +          fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
  10.192 +            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
  10.193 +            | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
  10.194 +              let
  10.195 +                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
  10.196 +                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
  10.197 +                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
  10.198 +                val args' = map (Pattern.rewrite_term thy [pat] []) args
  10.199 +              in
  10.200 +                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
  10.201 +              end
  10.202 +            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
  10.203 +          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
  10.204 +            (args, (pats, intro_t, ctxt))
  10.205 +        in
  10.206 +          rewrite_args args' (pats, intro_t', ctxt')
  10.207 +        end
  10.208 +      | _ => rewrite_args args (pats, intro_t, ctxt))
  10.209 +    fun rewrite_prem atom =
  10.210 +      let
  10.211 +        val (_, args) = strip_comb atom
  10.212 +      in rewrite_args args end
  10.213 +    val ctxt = ProofContext.init thy
  10.214 +    val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
  10.215 +    val intro_t = prop_of intro'
  10.216 +    val concl = Logic.strip_imp_concl intro_t
  10.217 +    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
  10.218 +    val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
  10.219 +    val (pats', intro_t', ctxt3) = 
  10.220 +      fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
  10.221 +    fun rewrite_pat (ct1, ct2) =
  10.222 +      (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
  10.223 +    val t_insts' = map rewrite_pat t_insts
  10.224 +    val intro'' = Thm.instantiate (T_insts, t_insts') intro
  10.225 +    val [intro'''] = Variable.export ctxt3 ctxt [intro'']
  10.226 +    val intro'''' = Simplifier.full_simplify
  10.227 +      (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
  10.228 +      intro'''
  10.229 +    (* splitting conjunctions introduced by Pair_eq*)
  10.230 +    fun split_conj prem =
  10.231 +      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
  10.232 +    val intro''''' = map_term thy (maps_premises split_conj) intro''''
  10.233 +  in
  10.234 +    intro'''''
  10.235 +  end
  10.236 +
  10.237 +
  10.238 +
  10.239 +end;
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 26 23:27:24 2009 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 09:02:22 2009 +0100
    11.3 @@ -49,11 +49,10 @@
    11.4      mk_sup : term * term -> term,
    11.5      mk_if : term -> term,
    11.6      mk_not : term -> term,
    11.7 -    mk_map : typ -> typ -> term -> term -> term,
    11.8 -    lift_pred : term -> term
    11.9 +    mk_map : typ -> typ -> term -> term -> term
   11.10    };
   11.11    val pred_compfuns : compilation_funs
   11.12 -  val rpred_compfuns : compilation_funs
   11.13 +  val randompred_compfuns : compilation_funs
   11.14      (*  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   11.15    val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   11.16    val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   11.17 @@ -720,12 +719,6 @@
   11.18      PredData.map (Graph.map_node pred (map_pred_data set))
   11.19    end
   11.20  
   11.21 -(** data structures for generic compilation for different monads **)
   11.22 -
   11.23 -(* maybe rename functions more generic:
   11.24 -  mk_predT -> mk_monadT; dest_predT -> dest_monadT
   11.25 -  mk_single -> mk_return (?)
   11.26 -*)
   11.27  datatype compilation_funs = CompilationFuns of {
   11.28    mk_predT : typ -> typ,
   11.29    dest_predT : typ -> typ,
   11.30 @@ -735,8 +728,7 @@
   11.31    mk_sup : term * term -> term,
   11.32    mk_if : term -> term,
   11.33    mk_not : term -> term,
   11.34 -  mk_map : typ -> typ -> term -> term -> term,
   11.35 -  lift_pred : term -> term
   11.36 +  mk_map : typ -> typ -> term -> term -> term
   11.37  };
   11.38  
   11.39  fun mk_predT (CompilationFuns funs) = #mk_predT funs
   11.40 @@ -748,7 +740,6 @@
   11.41  fun mk_if (CompilationFuns funs) = #mk_if funs
   11.42  fun mk_not (CompilationFuns funs) = #mk_not funs
   11.43  fun mk_map (CompilationFuns funs) = #mk_map funs
   11.44 -fun lift_pred (CompilationFuns funs) = #lift_pred funs
   11.45  
   11.46  fun funT_of compfuns (iss, is) T =
   11.47    let
   11.48 @@ -766,9 +757,9 @@
   11.49  structure PredicateCompFuns =
   11.50  struct
   11.51  
   11.52 -fun mk_predT T = Type (@{type_name "Predicate.pred"}, [T])
   11.53 +fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
   11.54  
   11.55 -fun dest_predT (Type (@{type_name "Predicate.pred"}, [T])) = T
   11.56 +fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
   11.57    | dest_predT T = raise TYPE ("dest_predT", [T], []);
   11.58  
   11.59  fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
   11.60 @@ -807,75 +798,65 @@
   11.61  fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
   11.62    (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
   11.63  
   11.64 -val lift_pred = I
   11.65 -
   11.66  val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   11.67    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
   11.68 -  mk_map = mk_map, lift_pred = lift_pred};
   11.69 +  mk_map = mk_map};
   11.70  
   11.71  end;
   11.72  
   11.73 -structure RPredCompFuns =
   11.74 +structure RandomPredCompFuns =
   11.75  struct
   11.76  
   11.77 -fun mk_rpredT T =
   11.78 -  @{typ "Random.seed"} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ "Random.seed"})
   11.79 +fun mk_randompredT T =
   11.80 +  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
   11.81  
   11.82 -fun dest_rpredT (Type ("fun", [_,
   11.83 -  Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T
   11.84 -  | dest_rpredT T = raise TYPE ("dest_rpredT", [T], []); 
   11.85 +fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
   11.86 +  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
   11.87 +  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
   11.88  
   11.89 -fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T)
   11.90 +fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
   11.91  
   11.92  fun mk_single t =
   11.93    let
   11.94      val T = fastype_of t
   11.95    in
   11.96 -    Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t
   11.97 +    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
   11.98    end;
   11.99  
  11.100  fun mk_bind (x, f) =
  11.101    let
  11.102      val T as (Type ("fun", [_, U])) = fastype_of f
  11.103    in
  11.104 -    Const (@{const_name RPred.bind}, fastype_of x --> T --> U) $ x $ f
  11.105 +    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
  11.106    end
  11.107  
  11.108 -val mk_sup = HOLogic.mk_binop @{const_name RPred.supp}
  11.109 -
  11.110 -fun mk_if cond = Const (@{const_name RPred.if_rpred},
  11.111 -  HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
  11.112 +val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
  11.113  
  11.114 -fun mk_not t = let val T = mk_rpredT HOLogic.unitT
  11.115 -  in Const (@{const_name RPred.not_rpred}, T --> T) $ t end
  11.116 -
  11.117 -fun mk_map T1 T2 tf tp = Const (@{const_name RPred.map},
  11.118 -  (T1 --> T2) --> mk_rpredT T1 --> mk_rpredT T2) $ tf $ tp
  11.119 +fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
  11.120 +  HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
  11.121  
  11.122 -fun lift_pred t =
  11.123 -  let
  11.124 -    val T = PredicateCompFuns.dest_predT (fastype_of t)
  11.125 -    val lift_predT = PredicateCompFuns.mk_predT T --> mk_rpredT T 
  11.126 -  in
  11.127 -    Const (@{const_name "RPred.lift_pred"}, lift_predT) $ t  
  11.128 -  end;
  11.129 +fun mk_not t = let val T = mk_randompredT HOLogic.unitT
  11.130 +  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
  11.131  
  11.132 -val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
  11.133 +fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
  11.134 +  (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
  11.135 +
  11.136 +val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, mk_bot = mk_bot,
  11.137      mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
  11.138 -    mk_map = mk_map, lift_pred = lift_pred};
  11.139 +    mk_map = mk_map};
  11.140  
  11.141  end;
  11.142  (* for external use with interactive mode *)
  11.143  val pred_compfuns = PredicateCompFuns.compfuns
  11.144 -val rpred_compfuns = RPredCompFuns.compfuns;
  11.145 +val randompred_compfuns = RandomPredCompFuns.compfuns;
  11.146  
  11.147  fun lift_random random =
  11.148    let
  11.149      val T = dest_randomT (fastype_of random)
  11.150    in
  11.151 -    Const (@{const_name lift_random}, (@{typ Random.seed} -->
  11.152 +    Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} -->
  11.153        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> 
  11.154 -      RPredCompFuns.mk_rpredT T) $ random
  11.155 +      RandomPredCompFuns.mk_randompredT T) $ random
  11.156    end;
  11.157  
  11.158  fun depth_limited_funT_of compfuns (iss, is) T =
  11.159 @@ -1604,7 +1585,7 @@
  11.160      val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs
  11.161    in
  11.162      (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
  11.163 -      (mk_predT RPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
  11.164 +      (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
  11.165    end
  11.166  
  11.167  fun rpred_create_definitions preds (name, modes) thy =
  11.168 @@ -2291,7 +2272,7 @@
  11.169  val add_quickcheck_equations = gen_add_equations
  11.170    {infer_modes = infer_modes_with_generator,
  11.171    create_definitions = rpred_create_definitions,
  11.172 -  compile_preds = compile_preds rpred_comp_modifiers RPredCompFuns.compfuns,
  11.173 +  compile_preds = compile_preds rpred_comp_modifiers RandomPredCompFuns.compfuns,
  11.174    prove = prove_by_skip,
  11.175    are_not_defined = fn thy => forall (null o rpred_modes_of thy),
  11.176    qname = "rpred_equation"}
  11.177 @@ -2420,7 +2401,7 @@
  11.178  
  11.179  fun eval thy (options as (depth_limit, random)) t_compr =
  11.180    let
  11.181 -    val compfuns = if random then RPredCompFuns.compfuns else PredicateCompFuns.compfuns
  11.182 +    val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns
  11.183      val t = analyze_compr thy compfuns options t_compr;
  11.184      val T = dest_predT compfuns (fastype_of t);
  11.185      val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
  11.186 @@ -2467,12 +2448,10 @@
  11.187  
  11.188  val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
  11.189  
  11.190 -val _ = List.app OuterKeyword.keyword ["depth_limit", "random"]
  11.191 -
  11.192  val options =
  11.193    let
  11.194 -    val depth_limit = Scan.optional (P.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
  11.195 -    val random = Scan.optional (P.$$$ "random" >> K true) false
  11.196 +    val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
  11.197 +    val random = Scan.optional (Args.$$$ "random" >> K true) false
  11.198    in
  11.199      Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false)
  11.200    end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Oct 27 09:02:22 2009 +0100
    12.3 @@ -0,0 +1,210 @@
    12.4 +(* Author: Lukas Bulwahn, TU Muenchen
    12.5 +
    12.6 +Book-keeping datastructure for the predicate compiler
    12.7 +
    12.8 +*)
    12.9 +signature PREDICATE_COMPILE_DATA =
   12.10 +sig
   12.11 +  type specification_table;
   12.12 +  val make_const_spec_table : theory -> specification_table
   12.13 +  val get_specification :  specification_table -> string -> thm list
   12.14 +  val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T
   12.15 +  val normalize_equation : theory -> thm -> thm
   12.16 +end;
   12.17 +
   12.18 +structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =
   12.19 +struct
   12.20 +
   12.21 +open Predicate_Compile_Aux;
   12.22 +
   12.23 +structure Data = TheoryDataFun
   12.24 +(
   12.25 +  type T =
   12.26 +    {const_spec_table : thm list Symtab.table};
   12.27 +  val empty =
   12.28 +    {const_spec_table = Symtab.empty};
   12.29 +  val copy = I;
   12.30 +  val extend = I;
   12.31 +  fun merge _
   12.32 +    ({const_spec_table = const_spec_table1},
   12.33 +     {const_spec_table = const_spec_table2}) =
   12.34 +     {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
   12.35 +);
   12.36 +
   12.37 +fun mk_data c = {const_spec_table = c}
   12.38 +fun map_data f {const_spec_table = c} = mk_data (f c)
   12.39 +
   12.40 +type specification_table = thm list Symtab.table
   12.41 +
   12.42 +fun defining_const_of_introrule_term t =
   12.43 +  let
   12.44 +    val _ $ u = Logic.strip_imp_concl t
   12.45 +    val (pred, all_args) = strip_comb u
   12.46 +  in case pred of
   12.47 +    Const (c, T) => c
   12.48 +    | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
   12.49 +  end
   12.50 +
   12.51 +val defining_const_of_introrule = defining_const_of_introrule_term o prop_of
   12.52 +
   12.53 +(*TODO*)
   12.54 +fun is_introlike_term t = true
   12.55 +
   12.56 +val is_introlike = is_introlike_term o prop_of
   12.57 +
   12.58 +fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
   12.59 +  (case strip_comb u of
   12.60 +    (Const (c, T), args) =>
   12.61 +      if (length (binder_types T) = length args) then
   12.62 +        true
   12.63 +      else
   12.64 +        raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
   12.65 +  | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
   12.66 +  | check_equation_format_term t =
   12.67 +    raise TERM ("check_equation_format_term failed: Not an equation", [t])
   12.68 +
   12.69 +val check_equation_format = check_equation_format_term o prop_of
   12.70 +
   12.71 +fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) =
   12.72 +  (case fst (strip_comb u) of
   12.73 +    Const (c, _) => c
   12.74 +  | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t]))
   12.75 +  | defining_const_of_equation_term t =
   12.76 +    raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
   12.77 +
   12.78 +val defining_const_of_equation = defining_const_of_equation_term o prop_of
   12.79 +
   12.80 +(* Normalizing equations *)
   12.81 +
   12.82 +fun mk_meta_equation th =
   12.83 +  case prop_of th of
   12.84 +    Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
   12.85 +  | _ => th
   12.86 +
   12.87 +val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
   12.88 +
   12.89 +fun full_fun_cong_expand th =
   12.90 +  let
   12.91 +    val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
   12.92 +    val i = length (binder_types (fastype_of f)) - length args
   12.93 +  in funpow i (fn th => th RS meta_fun_cong) th end;
   12.94 +
   12.95 +fun declare_names s xs ctxt =
   12.96 +  let
   12.97 +    val res = Name.names ctxt s xs
   12.98 +  in (res, fold Name.declare (map fst res) ctxt) end
   12.99 +  
  12.100 +fun split_all_pairs thy th =
  12.101 +  let
  12.102 +    val ctxt = ProofContext.init thy
  12.103 +    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
  12.104 +    val t = prop_of th'
  12.105 +    val frees = Term.add_frees t [] 
  12.106 +    val freenames = Term.add_free_names t []
  12.107 +    val nctxt = Name.make_context freenames
  12.108 +    fun mk_tuple_rewrites (x, T) nctxt =
  12.109 +      let
  12.110 +        val Ts = HOLogic.flatten_tupleT T
  12.111 +        val (xTs, nctxt') = declare_names x Ts nctxt
  12.112 +        val paths = HOLogic.flat_tupleT_paths T
  12.113 +      in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
  12.114 +    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
  12.115 +    val t' = Pattern.rewrite_term thy rewr [] t
  12.116 +    val tac = Skip_Proof.cheat_tac thy
  12.117 +    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
  12.118 +    val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
  12.119 +  in
  12.120 +    th'''
  12.121 +  end;
  12.122 +
  12.123 +fun normalize_equation thy th =
  12.124 +  mk_meta_equation th
  12.125 +  |> Predicate_Compile_Set.unfold_set_notation
  12.126 +  |> full_fun_cong_expand
  12.127 +  |> split_all_pairs thy
  12.128 +  |> tap check_equation_format
  12.129 +
  12.130 +fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
  12.131 +((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
  12.132 +
  12.133 +fun store_thm_in_table ignore_consts thy th=
  12.134 +  let
  12.135 +    val th = th
  12.136 +      |> inline_equations thy
  12.137 +      |> Predicate_Compile_Set.unfold_set_notation
  12.138 +      |> AxClass.unoverload thy
  12.139 +    val (const, th) =
  12.140 +      if is_equationlike th then
  12.141 +        let
  12.142 +          val eq = normalize_equation thy th
  12.143 +        in
  12.144 +          (defining_const_of_equation eq, eq)
  12.145 +        end
  12.146 +      else if (is_introlike th) then (defining_const_of_introrule th, th)
  12.147 +      else error "store_thm: unexpected definition format"
  12.148 +  in
  12.149 +    if not (member (op =) ignore_consts const) then
  12.150 +      Symtab.cons_list (const, th)
  12.151 +    else I
  12.152 +  end
  12.153 +
  12.154 +fun make_const_spec_table thy =
  12.155 +  let
  12.156 +    fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
  12.157 +    val table = Symtab.empty
  12.158 +      |> store [] Predicate_Compile_Alternative_Defs.get
  12.159 +    val ignore_consts = Symtab.keys table
  12.160 +  in
  12.161 +    table
  12.162 +    |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
  12.163 +    |> store ignore_consts Nitpick_Simps.get
  12.164 +    |> store ignore_consts Nitpick_Intros.get
  12.165 +  end
  12.166 +
  12.167 +fun get_specification table constname =
  12.168 +  case Symtab.lookup table constname of
  12.169 +    SOME thms => thms
  12.170 +  | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
  12.171 +
  12.172 +val logic_operator_names =
  12.173 +  [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, 
  12.174 +   @{const_name "op &"}]
  12.175 +
  12.176 +val special_cases = member (op =) [
  12.177 +    @{const_name "False"},
  12.178 +    @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
  12.179 +    @{const_name Nat.one_nat_inst.one_nat},
  12.180 +@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
  12.181 +@{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
  12.182 +@{const_name Nat.ord_nat_inst.less_eq_nat},
  12.183 +@{const_name number_nat_inst.number_of_nat},
  12.184 +  @{const_name Int.Bit0},
  12.185 +  @{const_name Int.Bit1},
  12.186 +  @{const_name Int.Pls},
  12.187 +@{const_name "Int.zero_int_inst.zero_int"},
  12.188 +@{const_name "List.filter"}]
  12.189 +
  12.190 +fun case_consts thy s = is_some (Datatype.info_of_case thy s)
  12.191 +
  12.192 +fun obtain_specification_graph thy table constname =
  12.193 +  let
  12.194 +    fun is_nondefining_constname c = member (op =) logic_operator_names c
  12.195 +    val is_defining_constname = member (op =) (Symtab.keys table)
  12.196 +    fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c)
  12.197 +    fun defiants_of specs =
  12.198 +      fold (Term.add_const_names o prop_of) specs []
  12.199 +      |> filter is_defining_constname
  12.200 +      |> filter_out is_nondefining_constname
  12.201 +      |> filter_out has_code_pred_intros
  12.202 +      |> filter_out (case_consts thy)
  12.203 +      |> filter_out special_cases
  12.204 +    fun extend constname =
  12.205 +      let
  12.206 +        val specs = get_specification table constname
  12.207 +      in (specs, defiants_of specs) end;
  12.208 +  in
  12.209 +    Graph.extend extend constname Graph.empty
  12.210 +  end;
  12.211 +  
  12.212 +  
  12.213 +end;
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Oct 27 09:02:22 2009 +0100
    13.3 @@ -0,0 +1,437 @@
    13.4 +(* Author: Lukas Bulwahn, TU Muenchen
    13.5 +
    13.6 +Preprocessing functions to predicates
    13.7 +*)
    13.8 +
    13.9 +signature PREDICATE_COMPILE_FUN =
   13.10 +sig
   13.11 +val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
   13.12 +  val rewrite_intro : theory -> thm -> thm list
   13.13 +  val setup_oracle : theory -> theory
   13.14 +  val pred_of_function : theory -> string -> string option
   13.15 +end;
   13.16 +
   13.17 +structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
   13.18 +struct
   13.19 +
   13.20 +
   13.21 +(* Oracle for preprocessing  *)
   13.22 +
   13.23 +val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
   13.24 +
   13.25 +fun the_oracle () =
   13.26 +  case !oracle of
   13.27 +    NONE => error "Oracle is not setup"
   13.28 +  | SOME (_, oracle) => oracle
   13.29 +             
   13.30 +val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
   13.31 +  (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
   13.32 +  
   13.33 +  
   13.34 +fun is_funtype (Type ("fun", [_, _])) = true
   13.35 +  | is_funtype _ = false;
   13.36 +
   13.37 +fun is_Type (Type _) = true
   13.38 +  | is_Type _ = false
   13.39 +
   13.40 +(* returns true if t is an application of an datatype constructor *)
   13.41 +(* which then consequently would be splitted *)
   13.42 +(* else false *)
   13.43 +(*
   13.44 +fun is_constructor thy t =
   13.45 +  if (is_Type (fastype_of t)) then
   13.46 +    (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
   13.47 +      NONE => false
   13.48 +    | SOME info => (let
   13.49 +      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
   13.50 +      val (c, _) = strip_comb t
   13.51 +      in (case c of
   13.52 +        Const (name, _) => name mem_string constr_consts
   13.53 +        | _ => false) end))
   13.54 +  else false
   13.55 +*)
   13.56 +
   13.57 +(* must be exported in code.ML *)
   13.58 +fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
   13.59 +
   13.60 +(* Table from constant name (string) to term of inductive predicate *)
   13.61 +structure Pred_Compile_Preproc = TheoryDataFun
   13.62 +(
   13.63 +  type T = string Symtab.table;
   13.64 +  val empty = Symtab.empty;
   13.65 +  val copy = I;
   13.66 +  val extend = I;
   13.67 +  fun merge _ = Symtab.merge (op =);
   13.68 +)
   13.69 +
   13.70 +fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
   13.71 +
   13.72 +fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) 
   13.73 +
   13.74 +
   13.75 +fun transform_ho_typ (T as Type ("fun", _)) =
   13.76 +  let
   13.77 +    val (Ts, T') = strip_type T
   13.78 +  in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end
   13.79 +| transform_ho_typ t = t
   13.80 +
   13.81 +fun transform_ho_arg arg = 
   13.82 +  case (fastype_of arg) of
   13.83 +    (T as Type ("fun", _)) =>
   13.84 +      (case arg of
   13.85 +        Free (name, _) => Free (name, transform_ho_typ T)
   13.86 +      | _ => error "I am surprised")
   13.87 +| _ => arg
   13.88 +
   13.89 +fun pred_type T =
   13.90 +  let
   13.91 +    val (Ts, T') = strip_type T
   13.92 +    val Ts' = map transform_ho_typ Ts
   13.93 +  in
   13.94 +    (Ts' @ [T']) ---> HOLogic.boolT
   13.95 +  end;
   13.96 +
   13.97 +(* FIXME: create new predicate name -- does not avoid nameclashing *)
   13.98 +fun pred_of f =
   13.99 +  let
  13.100 +    val (name, T) = dest_Const f
  13.101 +  in
  13.102 +    if (body_type T = @{typ bool}) then
  13.103 +      (Free (Long_Name.base_name name ^ "P", T))
  13.104 +    else
  13.105 +      (Free (Long_Name.base_name name ^ "P", pred_type T))
  13.106 +  end
  13.107 +
  13.108 +fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
  13.109 +  | mk_param thy lookup_pred t =
  13.110 +  let
  13.111 +  val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
  13.112 +  in if Predicate_Compile_Aux.is_predT (fastype_of t) then
  13.113 +    t
  13.114 +  else
  13.115 +    let
  13.116 +      val (vs, body) = strip_abs t
  13.117 +      val names = Term.add_free_names body []
  13.118 +      val vs_names = Name.variant_list names (map fst vs)
  13.119 +      val vs' = map2 (curry Free) vs_names (map snd vs)
  13.120 +      val body' = subst_bounds (rev vs', body)
  13.121 +      val (f, args) = strip_comb body'
  13.122 +      val resname = Name.variant (vs_names @ names) "res"
  13.123 +      val resvar = Free (resname, body_type (fastype_of body'))
  13.124 +      (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param"
  13.125 +      val pred_body = list_comb (P, args @ [resvar])
  13.126 +      *)
  13.127 +      val pred_body = HOLogic.mk_eq (body', resvar)
  13.128 +      val param = fold_rev lambda (vs' @ [resvar]) pred_body
  13.129 +    in param end
  13.130 +  end
  13.131 +(* creates the list of premises for every intro rule *)
  13.132 +(* theory -> term -> (string list, term list list) *)
  13.133 +
  13.134 +fun dest_code_eqn eqn = let
  13.135 +  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
  13.136 +  val (func, args) = strip_comb lhs
  13.137 +in ((func, args), rhs) end;
  13.138 +
  13.139 +fun string_of_typ T = Syntax.string_of_typ_global @{theory} T
  13.140 +
  13.141 +fun string_of_term t =
  13.142 +  case t of
  13.143 +    Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")"
  13.144 +  | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")"
  13.145 +  | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")"
  13.146 +  | Bound i => "Bound " ^ string_of_int i
  13.147 +  | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")"
  13.148 +  | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
  13.149 +  
  13.150 +fun ind_package_get_nparams thy name =
  13.151 +  case try (Inductive.the_inductive (ProofContext.init thy)) name of
  13.152 +    SOME (_, result) => length (Inductive.params_of (#raw_induct result))
  13.153 +  | NONE => error ("No such predicate: " ^ quote name) 
  13.154 +
  13.155 +(* TODO: does not work with higher order functions yet *)
  13.156 +fun mk_rewr_eq (func, pred) =
  13.157 +  let
  13.158 +    val (argTs, resT) = (strip_type (fastype_of func))
  13.159 +    val nctxt =
  13.160 +      Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
  13.161 +    val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
  13.162 +    val ([resname], nctxt'') = Name.variants ["r"] nctxt'
  13.163 +    val args = map Free (argnames ~~ argTs)
  13.164 +    val res = Free (resname, resT)
  13.165 +  in Logic.mk_equals
  13.166 +      (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
  13.167 +  end;
  13.168 +
  13.169 +fun has_split_rule_cname @{const_name "nat_case"} = true
  13.170 +  | has_split_rule_cname @{const_name "list_case"} = true
  13.171 +  | has_split_rule_cname _ = false
  13.172 +  
  13.173 +fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true 
  13.174 +  | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true 
  13.175 +  | has_split_rule_term thy _ = false
  13.176 +
  13.177 +fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
  13.178 +  | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
  13.179 +  | has_split_rule_term' thy c = has_split_rule_term thy c
  13.180 +  
  13.181 +fun prepare_split_thm ctxt split_thm =
  13.182 +    (split_thm RS @{thm iffD2})
  13.183 +    |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
  13.184 +      @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
  13.185 +
  13.186 +fun find_split_thm thy (Const (name, typ)) =
  13.187 +  let
  13.188 +    fun split_name str =
  13.189 +      case first_field "." str
  13.190 +        of (SOME (field, rest)) => field :: split_name rest
  13.191 +         | NONE => [str]
  13.192 +    val splitted_name = split_name name
  13.193 +  in
  13.194 +    if length splitted_name > 0 andalso
  13.195 +       String.isSuffix "_case" (List.last splitted_name)
  13.196 +    then
  13.197 +      (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
  13.198 +      |> space_implode "."
  13.199 +      |> PureThy.get_thm thy
  13.200 +      |> SOME
  13.201 +      handle ERROR msg => NONE
  13.202 +    else NONE
  13.203 +  end
  13.204 +  | find_split_thm _ _ = NONE
  13.205 +
  13.206 +fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
  13.207 +  | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
  13.208 +  | find_split_thm' thy c = find_split_thm thy c
  13.209 +
  13.210 +fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
  13.211 +
  13.212 +fun folds_map f xs y =
  13.213 +  let
  13.214 +    fun folds_map' acc [] y = [(rev acc, y)]
  13.215 +      | folds_map' acc (x :: xs) y =
  13.216 +        maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y)
  13.217 +    in
  13.218 +      folds_map' [] xs y
  13.219 +    end;
  13.220 +
  13.221 +fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) =
  13.222 +  let
  13.223 +    fun mk_prems' (t as Const (name, T)) (names, prems) =
  13.224 +      if is_constr thy name orelse (is_none (try lookup_pred t)) then
  13.225 +        [(t, (names, prems))]
  13.226 +      else [(lookup_pred t, (names, prems))]
  13.227 +    | mk_prems' (t as Free (f, T)) (names, prems) = 
  13.228 +      [(lookup_pred t, (names, prems))]
  13.229 +    | mk_prems' (t as Abs _) (names, prems) =
  13.230 +      if Predicate_Compile_Aux.is_predT (fastype_of t) then
  13.231 +      [(t, (names, prems))] else error "mk_prems': Abs "
  13.232 +      (* mk_param *)
  13.233 +    | mk_prems' t (names, prems) =
  13.234 +      if Predicate_Compile_Aux.is_constrt thy t then
  13.235 +        [(t, (names, prems))]
  13.236 +      else
  13.237 +        if has_split_rule_term' thy (fst (strip_comb t)) then
  13.238 +          let
  13.239 +            val (f, args) = strip_comb t
  13.240 +            val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
  13.241 +            (* TODO: contextify things - this line is to unvarify the split_thm *)
  13.242 +            (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
  13.243 +            val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
  13.244 +            val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
  13.245 +            val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
  13.246 +            val (_, split_args) = strip_comb split_t
  13.247 +            val match = split_args ~~ args
  13.248 +            fun mk_prems_of_assm assm =
  13.249 +              let
  13.250 +                val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
  13.251 +                val var_names = Name.variant_list names (map fst vTs)
  13.252 +                val vars = map Free (var_names ~~ (map snd vTs))
  13.253 +                val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
  13.254 +                val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
  13.255 +              in
  13.256 +                mk_prems' inner_t (var_names @ names, prems' @ prems)
  13.257 +              end
  13.258 +          in
  13.259 +            maps mk_prems_of_assm assms
  13.260 +          end
  13.261 +        else
  13.262 +          let
  13.263 +            val (f, args) = strip_comb t
  13.264 +            (* TODO: special procedure for higher-order functions: split arguments in
  13.265 +              simple types and function types *)
  13.266 +            val resname = Name.variant names "res"
  13.267 +            val resvar = Free (resname, body_type (fastype_of t))
  13.268 +            val names' = resname :: names
  13.269 +            fun mk_prems'' (t as Const (c, _)) =
  13.270 +              if is_constr thy c orelse (is_none (try lookup_pred t)) then
  13.271 +                folds_map mk_prems' args (names', prems) |>
  13.272 +                map
  13.273 +                  (fn (argvs, (names'', prems')) =>
  13.274 +                  let
  13.275 +                    val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
  13.276 +                  in (names'', prem :: prems') end)
  13.277 +              else
  13.278 +                let
  13.279 +                  val pred = lookup_pred t
  13.280 +                  val nparams = get_nparams pred
  13.281 +                  val (params, args) = chop nparams args
  13.282 +                  val params' = map (mk_param thy lookup_pred) params
  13.283 +                in
  13.284 +                  folds_map mk_prems' args (names', prems)
  13.285 +                  |> map (fn (argvs, (names'', prems')) =>
  13.286 +                    let
  13.287 +                      val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar]))
  13.288 +                    in (names'', prem :: prems') end)
  13.289 +                end
  13.290 +            | mk_prems'' (t as Free (_, _)) =
  13.291 +                let
  13.292 +                  (* higher order argument call *)
  13.293 +                  val pred = lookup_pred t
  13.294 +                in
  13.295 +                  folds_map mk_prems' args (resname :: names, prems)
  13.296 +                  |> map (fn (argvs, (names', prems')) =>
  13.297 +                     let
  13.298 +                       val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
  13.299 +                     in (names', prem :: prems') end)
  13.300 +                end
  13.301 +            | mk_prems'' t =
  13.302 +              error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
  13.303 +          in
  13.304 +            map (pair resvar) (mk_prems'' f)
  13.305 +          end
  13.306 +  in
  13.307 +    mk_prems' t (names, prems)
  13.308 +  end;
  13.309 +
  13.310 +(* assumption: mutual recursive predicates all have the same parameters. *)  
  13.311 +fun define_predicates specs thy =
  13.312 +  if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then
  13.313 +    ([], thy)
  13.314 +  else
  13.315 +  let
  13.316 +    val consts = map fst specs
  13.317 +    val eqns = maps snd specs
  13.318 +    (*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*)
  13.319 +      (* create prednames *)
  13.320 +    val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
  13.321 +    val argss' = map (map transform_ho_arg) argss
  13.322 +    val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss'))
  13.323 +    val preds = map pred_of funs
  13.324 +    val prednames = map (fst o dest_Free) preds
  13.325 +    val funnames = map (fst o dest_Const) funs
  13.326 +    val fun_pred_names = (funnames ~~ prednames)  
  13.327 +      (* mapping from term (Free or Const) to term *)
  13.328 +    fun lookup_pred (Const (name, T)) =
  13.329 +      (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
  13.330 +          SOME c => Const (c, pred_type T)
  13.331 +        | NONE =>
  13.332 +          (case AList.lookup op = fun_pred_names name of
  13.333 +            SOME f => Free (f, pred_type T)
  13.334 +          | NONE => Const (name, T)))
  13.335 +      | lookup_pred (Free (name, T)) =
  13.336 +        if member op = (map fst pnames) name then
  13.337 +          Free (name, transform_ho_typ T)
  13.338 +        else
  13.339 +          Free (name, T)
  13.340 +      | lookup_pred t =
  13.341 +         error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t)
  13.342 +     
  13.343 +        (* mapping from term (predicate term, not function term!) to int *)
  13.344 +    fun get_nparams (Const (name, _)) =
  13.345 +      the_default 0 (try (ind_package_get_nparams thy) name)
  13.346 +    | get_nparams (Free (name, _)) =
  13.347 +        (if member op = prednames name then
  13.348 +          length pnames
  13.349 +        else 0)
  13.350 +    | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
  13.351 +  
  13.352 +    (* create intro rules *)
  13.353 +  
  13.354 +    fun mk_intros ((func, pred), (args, rhs)) =
  13.355 +      if (body_type (fastype_of func) = @{typ bool}) then
  13.356 +       (*TODO: preprocess predicate definition of rhs *)
  13.357 +        [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
  13.358 +      else
  13.359 +        let
  13.360 +          val names = Term.add_free_names rhs []
  13.361 +        in mk_prems thy (lookup_pred, get_nparams) rhs (names, [])
  13.362 +          |> map (fn (resultt, (names', prems)) =>
  13.363 +            Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
  13.364 +        end
  13.365 +    fun mk_rewr_thm (func, pred) = @{thm refl}
  13.366 +  in
  13.367 +    case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
  13.368 +      NONE => ([], thy) 
  13.369 +    | SOME intr_ts =>
  13.370 +        if is_some (try (map (cterm_of thy)) intr_ts) then
  13.371 +          let
  13.372 +            val (ind_result, thy') =
  13.373 +              Inductive.add_inductive_global (serial ())
  13.374 +                {quiet_mode = false, verbose = false, kind = Thm.internalK,
  13.375 +                  alt_name = Binding.empty, coind = false, no_elim = false,
  13.376 +                  no_ind = false, skip_mono = false, fork_mono = false}
  13.377 +                (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
  13.378 +                pnames
  13.379 +                (map (fn x => (Attrib.empty_binding, x)) intr_ts)
  13.380 +                [] thy
  13.381 +            val prednames = map (fst o dest_Const) (#preds ind_result)
  13.382 +            (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
  13.383 +            (* add constants to my table *)
  13.384 +            val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames
  13.385 +            val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
  13.386 +          in
  13.387 +            (specs, thy'')
  13.388 +          end
  13.389 +        else
  13.390 +          let
  13.391 +            val _ = tracing "Introduction rules of function_predicate are not welltyped"
  13.392 +          in ([], thy) end
  13.393 +  end
  13.394 +
  13.395 +(* preprocessing intro rules - uses oracle *)
  13.396 +
  13.397 +(* theory -> thm -> thm *)
  13.398 +fun rewrite_intro thy intro =
  13.399 +  let
  13.400 +    fun lookup_pred (Const (name, T)) =
  13.401 +      (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
  13.402 +        SOME c => Const (c, pred_type T)
  13.403 +      | NONE => error ("Function " ^ name ^ " is not inductified"))
  13.404 +    | lookup_pred (Free (name, T)) = Free (name, T)
  13.405 +    | lookup_pred _ = error "lookup function is not defined!"
  13.406 +
  13.407 +    fun get_nparams (Const (name, _)) =
  13.408 +      the_default 0 (try (ind_package_get_nparams thy) name)
  13.409 +    | get_nparams (Free _) = 0
  13.410 +    | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
  13.411 +    
  13.412 +    val intro_t = (Logic.unvarify o prop_of) intro
  13.413 +    val (prems, concl) = Logic.strip_horn intro_t
  13.414 +    val frees = map fst (Term.add_frees intro_t [])
  13.415 +    fun rewrite prem names =
  13.416 +      let
  13.417 +        val t = (HOLogic.dest_Trueprop prem)
  13.418 +        val (lit, mk_lit) = case try HOLogic.dest_not t of
  13.419 +            SOME t => (t, HOLogic.mk_not)
  13.420 +          | NONE => (t, I)
  13.421 +        val (P, args) = (strip_comb lit) 
  13.422 +      in
  13.423 +        folds_map (
  13.424 +          fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)])
  13.425 +            else mk_prems thy (lookup_pred, get_nparams) t) args (names, [])
  13.426 +        |> map (fn (resargs, (names', prems')) =>
  13.427 +          let
  13.428 +            val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
  13.429 +          in (prem'::prems', names') end)
  13.430 +      end
  13.431 +    val intro_ts' = folds_map rewrite prems frees
  13.432 +      |> maps (fn (prems', frees') =>
  13.433 +        rewrite concl frees'
  13.434 +        |> map (fn (concl'::conclprems, _) =>
  13.435 +          Logic.list_implies ((flat prems') @ conclprems, concl')))
  13.436 +  in
  13.437 +    map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
  13.438 +  end; 
  13.439 +
  13.440 +end;
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Oct 27 09:02:22 2009 +0100
    14.3 @@ -0,0 +1,189 @@
    14.4 +(* Author: Lukas Bulwahn, TU Muenchen
    14.5 +
    14.6 +Preprocessing definitions of predicates to introduction rules
    14.7 +*)
    14.8 +
    14.9 +signature PREDICATE_COMPILE_PRED =
   14.10 +sig
   14.11 +  (* preprocesses an equation to a set of intro rules; defines new constants *)
   14.12 +  (*
   14.13 +  val preprocess_pred_equation : thm -> theory -> thm list * theory
   14.14 +  *)
   14.15 +  val preprocess : string -> theory -> (thm list list * theory) 
   14.16 +  (* output is the term list of clauses of an unknown predicate *)
   14.17 +  val preprocess_term : term -> theory -> (term list * theory)
   14.18 +  
   14.19 +  (*val rewrite : thm -> thm*)
   14.20 +  
   14.21 +end;
   14.22 +(* : PREDICATE_COMPILE_PREPROC_PRED *)
   14.23 +structure Predicate_Compile_Pred =
   14.24 +struct
   14.25 +
   14.26 +open Predicate_Compile_Aux
   14.27 +
   14.28 +fun is_compound ((Const ("Not", _)) $ t) =
   14.29 +    error "is_compound: Negation should not occur; preprocessing is defect"
   14.30 +  | is_compound ((Const ("Ex", _)) $ _) = true
   14.31 +  | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
   14.32 +  | is_compound ((Const ("op &", _)) $ _ $ _) =
   14.33 +    error "is_compound: Conjunction should not occur; preprocessing is defect"
   14.34 +  | is_compound _ = false
   14.35 +
   14.36 +fun flatten constname atom (defs, thy) =
   14.37 +  if is_compound atom then
   14.38 +    let
   14.39 +      val constname = Name.variant (map (Long_Name.base_name o fst) defs)
   14.40 +        ((Long_Name.base_name constname) ^ "_aux")
   14.41 +      val full_constname = Sign.full_bname thy constname
   14.42 +      val (params, args) = List.partition (is_predT o fastype_of)
   14.43 +        (map Free (Term.add_frees atom []))
   14.44 +      val constT = map fastype_of (params @ args) ---> HOLogic.boolT
   14.45 +      val lhs = list_comb (Const (full_constname, constT), params @ args)
   14.46 +      val def = Logic.mk_equals (lhs, atom)
   14.47 +      val ([definition], thy') = thy
   14.48 +        |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   14.49 +        |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
   14.50 +    in
   14.51 +      (lhs, ((full_constname, [definition]) :: defs, thy'))
   14.52 +    end
   14.53 +  else
   14.54 +    (atom, (defs, thy))
   14.55 +
   14.56 +fun flatten_intros constname intros thy =
   14.57 +  let
   14.58 +    val ctxt = ProofContext.init thy
   14.59 +    val ((_, intros), ctxt') = Variable.import true intros ctxt
   14.60 +    val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
   14.61 +      (flatten constname) (map prop_of intros) ([], thy)
   14.62 +    val tac = fn _ => Skip_Proof.cheat_tac thy'
   14.63 +    val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
   14.64 +      |> Variable.export ctxt' ctxt
   14.65 +  in
   14.66 +    (intros'', (local_defs, thy'))
   14.67 +  end
   14.68 +
   14.69 +(* TODO: same function occurs in inductive package *)
   14.70 +fun select_disj 1 1 = []
   14.71 +  | select_disj _ 1 = [rtac @{thm disjI1}]
   14.72 +  | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
   14.73 +
   14.74 +fun introrulify thy ths = 
   14.75 +  let
   14.76 +    val ctxt = ProofContext.init thy
   14.77 +    val ((_, ths'), ctxt') = Variable.import true ths ctxt
   14.78 +    fun introrulify' th =
   14.79 +      let
   14.80 +        val (lhs, rhs) = Logic.dest_equals (prop_of th)
   14.81 +        val frees = Term.add_free_names rhs []
   14.82 +        val disjuncts = HOLogic.dest_disj rhs
   14.83 +        val nctxt = Name.make_context frees
   14.84 +        fun mk_introrule t =
   14.85 +          let
   14.86 +            val ((ps, t'), nctxt') = focus_ex t nctxt
   14.87 +            val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
   14.88 +          in
   14.89 +            (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
   14.90 +          end
   14.91 +        val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
   14.92 +          Logic.dest_implies o prop_of) @{thm exI}
   14.93 +        fun prove_introrule (index, (ps, introrule)) =
   14.94 +          let
   14.95 +            val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1
   14.96 +              THEN EVERY1 (select_disj (length disjuncts) (index + 1)) 
   14.97 +              THEN (EVERY (map (fn y =>
   14.98 +                rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
   14.99 +              THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
  14.100 +              THEN TRY (atac 1)
  14.101 +          in
  14.102 +            Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
  14.103 +          end
  14.104 +      in
  14.105 +        map_index prove_introrule (map mk_introrule disjuncts)
  14.106 +      end
  14.107 +  in maps introrulify' ths' |> Variable.export ctxt' ctxt end
  14.108 +
  14.109 +val rewrite =
  14.110 +  Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}])
  14.111 +  #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) 
  14.112 +  #> Conv.fconv_rule nnf_conv 
  14.113 +  #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
  14.114 +
  14.115 +val rewrite_intros =
  14.116 +  Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)})
  14.117 +
  14.118 +fun preprocess (constname, specs) thy =
  14.119 +  let
  14.120 +    val ctxt = ProofContext.init thy
  14.121 +      val intros =
  14.122 +      if forall is_pred_equation specs then 
  14.123 +        introrulify thy (map rewrite specs)
  14.124 +      else if forall (is_intro constname) specs then
  14.125 +        map rewrite_intros specs
  14.126 +      else
  14.127 +        error ("unexpected specification for constant " ^ quote constname ^ ":\n"
  14.128 +          ^ commas (map (quote o Display.string_of_thm_global thy) specs))
  14.129 +    val (intros', (local_defs, thy')) = flatten_intros constname intros thy
  14.130 +    val (intross, thy'') = fold_map preprocess local_defs thy'
  14.131 +  in
  14.132 +    ((constname, intros') :: flat intross,thy'')
  14.133 +  end;
  14.134 +
  14.135 +fun preprocess_term t thy = error "preprocess_pred_term: to implement" 
  14.136 +
  14.137 +fun is_Abs (Abs _) = true
  14.138 +  | is_Abs _       = false
  14.139 +
  14.140 +fun flat_higher_order_arguments (intross, thy) =
  14.141 +  let
  14.142 +    fun process constname atom (new_defs, thy) =
  14.143 +      let
  14.144 +        val (pred, args) = strip_comb atom
  14.145 +        val abs_args = filter is_Abs args
  14.146 +        fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
  14.147 +          let
  14.148 +            val _ = tracing ("Introduce new constant for " ^
  14.149 +              Syntax.string_of_term_global thy abs_arg)
  14.150 +            val vars = map Var (Term.add_vars abs_arg [])
  14.151 +            val abs_arg' = Logic.unvarify abs_arg
  14.152 +            val frees = map Free (Term.add_frees abs_arg' [])
  14.153 +            val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
  14.154 +              ((Long_Name.base_name constname) ^ "_hoaux")
  14.155 +            val full_constname = Sign.full_bname thy constname
  14.156 +            val constT = map fastype_of frees ---> (fastype_of abs_arg')
  14.157 +            val const = Const (full_constname, constT)
  14.158 +            val lhs = list_comb (const, frees)
  14.159 +            val def = Logic.mk_equals (lhs, abs_arg')
  14.160 +            val _ = tracing (Syntax.string_of_term_global thy def)
  14.161 +            val ([definition], thy') = thy
  14.162 +              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
  14.163 +              |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
  14.164 +          in
  14.165 +            (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
  14.166 +          end
  14.167 +        | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy))
  14.168 +        val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
  14.169 +      in
  14.170 +        (list_comb (pred, args'), (new_defs', thy'))
  14.171 +      end
  14.172 +    fun flat_intro intro (new_defs, thy) =
  14.173 +      let
  14.174 +        val constname = fst (dest_Const (fst (strip_comb
  14.175 +          (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
  14.176 +        val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
  14.177 +        val th = Skip_Proof.make_thm thy intro_ts
  14.178 +      in
  14.179 +        (th, (new_defs, thy))
  14.180 +      end
  14.181 +    fun fold_map_spec f [] s = ([], s)
  14.182 +      | fold_map_spec f ((c, ths) :: specs) s =
  14.183 +        let
  14.184 +          val (ths', s') = f ths s
  14.185 +          val (specs', s'') = fold_map_spec f specs s'
  14.186 +        in ((c, ths') :: specs', s'') end
  14.187 +    val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy)
  14.188 +  in
  14.189 +    (intross', (new_defs, thy'))
  14.190 +  end
  14.191 +
  14.192 +end;
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Oct 27 09:02:22 2009 +0100
    15.3 @@ -0,0 +1,96 @@
    15.4 +(* Author: Lukas Bulwahn, TU Muenchen
    15.5 +
    15.6 +A quickcheck generator based on the predicate compiler
    15.7 +*)
    15.8 +
    15.9 +signature PREDICATE_COMPILE_QUICKCHECK =
   15.10 +sig
   15.11 +  val quickcheck : Proof.context -> term -> int -> term list option
   15.12 +  val test_ref :
   15.13 +    ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
   15.14 +end;
   15.15 +
   15.16 +structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
   15.17 +struct
   15.18 +
   15.19 +val test_ref =
   15.20 +  Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
   15.21 +
   15.22 +val target = "Quickcheck"
   15.23 +
   15.24 +fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
   15.25 +val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
   15.26 +val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
   15.27 +val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
   15.28 +val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
   15.29 +val lift_pred = #lift_pred (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
   15.30 +
   15.31 +fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
   15.32 +  | mk_split_lambda [x] t = lambda x t
   15.33 +  | mk_split_lambda xs t =
   15.34 +  let
   15.35 +    fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
   15.36 +      | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
   15.37 +  in
   15.38 +    mk_split_lambda' xs t
   15.39 +  end;
   15.40 +
   15.41 +fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B
   15.42 +  | strip_imp_prems _ = [];
   15.43 +
   15.44 +fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B
   15.45 +  | strip_imp_concl A = A : term;
   15.46 +
   15.47 +fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   15.48 +
   15.49 +fun quickcheck ctxt t =
   15.50 +  let
   15.51 +    val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t))
   15.52 +    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
   15.53 +    val thy = (ProofContext.theory_of ctxt') 
   15.54 +    val (vs, t') = strip_abs t
   15.55 +    val vs' = Variable.variant_frees ctxt' [] vs
   15.56 +    val t'' = subst_bounds (map Free (rev vs'), t')
   15.57 +    val (prems, concl) = strip_horn t''
   15.58 +    val constname = "pred_compile_quickcheck"
   15.59 +    val full_constname = Sign.full_bname thy constname
   15.60 +    val constT = map snd vs' ---> @{typ bool}
   15.61 +    val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
   15.62 +    val t = Logic.list_implies
   15.63 +      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
   15.64 +       HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
   15.65 +    val tac = fn _ => Skip_Proof.cheat_tac thy'
   15.66 +    val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
   15.67 +    val _ = tracing (Display.string_of_thm ctxt' intro)
   15.68 +    val thy'' = thy'
   15.69 +      |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
   15.70 +      |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
   15.71 +      (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*)
   15.72 +      (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
   15.73 +      (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *)
   15.74 +    val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
   15.75 +    val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  
   15.76 +    val prog =
   15.77 +      if member (op =) modes ([], []) then
   15.78 +        let
   15.79 +          val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
   15.80 +          val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
   15.81 +          in Const (name, T) $ @{term True} $ Bound 0 end
   15.82 +      else if member (op =) depth_limited_modes ([], []) then
   15.83 +        let
   15.84 +          val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
   15.85 +          val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
   15.86 +        in lift_pred (Const (name, T) $ Bound 0) end
   15.87 +      else error "Predicate Compile Quickcheck failed"
   15.88 +    val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog,
   15.89 +      mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
   15.90 +      (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
   15.91 +    val _ = tracing (Syntax.string_of_term ctxt' qc_term)
   15.92 +    val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
   15.93 +      (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
   15.94 +      thy'' qc_term []
   15.95 +  in
   15.96 +    ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield))
   15.97 +  end
   15.98 +
   15.99 +end;
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML	Tue Oct 27 09:02:22 2009 +0100
    16.3 @@ -0,0 +1,52 @@
    16.4 +(* Author: Lukas Bulwahn, TU Muenchen
    16.5 +
    16.6 +Preprocessing sets to predicates
    16.7 +*)
    16.8 +
    16.9 +signature PREDICATE_COMPILE_SET =
   16.10 +sig
   16.11 +(*
   16.12 +  val preprocess_intro : thm -> theory -> thm * theory
   16.13 +  val preprocess_clause : term -> theory -> term * theory
   16.14 +*)
   16.15 +  val unfold_set_notation : thm -> thm;
   16.16 +end;
   16.17 +
   16.18 +structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
   16.19 +struct
   16.20 +(*FIXME: unfolding Ball in pretty adhoc here *)
   16.21 +val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
   16.22 +@{thm Ball_def}, @{thm Bex_def}]
   16.23 +
   16.24 +val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
   16.25 +
   16.26 +(*
   16.27 +fun find_set_theorems ctxt cname =
   16.28 +  let
   16.29 +    val _ = cname 
   16.30 +*)
   16.31 +
   16.32 +(*
   16.33 +fun preprocess_term t ctxt =
   16.34 +  case t of
   16.35 +    Const ("op :", _) $ x $ A => 
   16.36 +      case strip_comb A of
   16.37 +        (Const (cname, T), params) =>
   16.38 +          let 
   16.39 +            val _ = find_set_theorems
   16.40 +          in
   16.41 +            (t, ctxt)
   16.42 +          end
   16.43 +      | _ => (t, ctxt)  
   16.44 +  | _ => (t, ctxt)
   16.45 +*) 
   16.46 +(*
   16.47 +fun preprocess_intro th thy =
   16.48 +  let
   16.49 +    val cnames = find_heads_of_prems
   16.50 +    val set_cname = filter (has_set_definition
   16.51 +    val _ = define_preds
   16.52 +    val _ = prep_pred_def
   16.53 +  in
   16.54 +*)
   16.55 +end;
    17.1 --- a/src/HOL/ex/Predicate_Compile.thy	Mon Oct 26 23:27:24 2009 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,17 +0,0 @@
    17.4 -theory Predicate_Compile
    17.5 -imports Complex_Main RPred
    17.6 -uses
    17.7 -  "../Tools/Predicate_Compile/pred_compile_aux.ML"
    17.8 -  "../Tools/Predicate_Compile/predicate_compile_core.ML"
    17.9 -  "../Tools/Predicate_Compile/pred_compile_set.ML"
   17.10 -  "../Tools/Predicate_Compile/pred_compile_data.ML"
   17.11 -  "../Tools/Predicate_Compile/pred_compile_fun.ML"
   17.12 -  "../Tools/Predicate_Compile/pred_compile_pred.ML"
   17.13 -  "../Tools/Predicate_Compile/predicate_compile.ML"
   17.14 -  "../Tools/Predicate_Compile/pred_compile_quickcheck.ML"
   17.15 -begin
   17.16 -
   17.17 -setup {* Predicate_Compile.setup *}
   17.18 -setup {* Quickcheck.add_generator ("pred_compile", Predicate_Compile_Quickcheck.quickcheck) *}
   17.19 -
   17.20 -end
   17.21 \ No newline at end of file
    18.1 --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy	Mon Oct 26 23:27:24 2009 +0100
    18.2 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy	Tue Oct 27 09:02:22 2009 +0100
    18.3 @@ -1,5 +1,5 @@
    18.4  theory Predicate_Compile_Alternative_Defs
    18.5 -imports Predicate_Compile
    18.6 +imports Main
    18.7  begin
    18.8  
    18.9  section {* Set operations *}
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Tue Oct 27 09:02:22 2009 +0100
    19.3 @@ -0,0 +1,12 @@
    19.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
    19.5 +
    19.6 +header {* A Prototype of Quickcheck based on the Predicate Compiler *}
    19.7 +
    19.8 +theory Predicate_Compile_Quickcheck
    19.9 +imports Main
   19.10 +uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
   19.11 +begin
   19.12 +
   19.13 +setup {* Quickcheck.add_generator ("predicate_compile", Predicate_Compile_Quickcheck.quickcheck) *}
   19.14 +
   19.15 +end
   19.16 \ No newline at end of file
    20.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Mon Oct 26 23:27:24 2009 +0100
    20.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Oct 27 09:02:22 2009 +0100
    20.3 @@ -2,6 +2,64 @@
    20.4  imports Main Predicate_Compile_Alternative_Defs
    20.5  begin
    20.6  
    20.7 +subsection {* Basic predicates *}
    20.8 +
    20.9 +inductive False' :: "bool"
   20.10 +
   20.11 +code_pred (mode: []) False' .
   20.12 +code_pred [depth_limited] False' .
   20.13 +code_pred [rpred, show_compilation] False' .
   20.14 +
   20.15 +inductive EmptySet :: "'a \<Rightarrow> bool"
   20.16 +
   20.17 +code_pred (mode: [], [1]) EmptySet .
   20.18 +
   20.19 +inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   20.20 +
   20.21 +code_pred (mode: [], [1], [2], [1, 2]) EmptyRel .
   20.22 +
   20.23 +inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   20.24 +for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   20.25 +
   20.26 +code_pred (mode: [], [1], [2], [1, 2])EmptyClosure .
   20.27 +thm EmptyClosure.equation
   20.28 +
   20.29 +inductive False'' :: "bool"
   20.30 +where
   20.31 +  "False \<Longrightarrow> False''"
   20.32 +
   20.33 +code_pred (mode: []) False'' .
   20.34 +
   20.35 +inductive EmptySet' :: "'a \<Rightarrow> bool"
   20.36 +where
   20.37 +  "False \<Longrightarrow> EmptySet' x"
   20.38 +
   20.39 +code_pred (mode: [1]) EmptySet' .
   20.40 +code_pred (mode: [], [1]) [inductify] EmptySet' .
   20.41 +
   20.42 +inductive True' :: "bool"
   20.43 +where
   20.44 +  "True \<Longrightarrow> True'"
   20.45 +
   20.46 +code_pred (mode: []) True' .
   20.47 +
   20.48 +consts a' :: 'a
   20.49 +
   20.50 +inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   20.51 +where
   20.52 +"Fact a' a'"
   20.53 +
   20.54 +code_pred (mode: [], [1], [2], [1, 2]) Fact .
   20.55 +
   20.56 +inductive zerozero :: "nat * nat => bool"
   20.57 +where
   20.58 +  "zerozero (0, 0)"
   20.59 +
   20.60 +code_pred zerozero .
   20.61 +code_pred [rpred, show_compilation] zerozero .
   20.62 +
   20.63 +subsection {* even predicate *}
   20.64 +
   20.65  inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
   20.66      "even 0"
   20.67    | "even n \<Longrightarrow> odd (Suc n)"
   20.68 @@ -26,7 +84,6 @@
   20.69  values [depth_limit = 7] "{x. even 6}"
   20.70  values [depth_limit = 2] "{x. odd 7}"
   20.71  values [depth_limit = 8] "{x. odd 7}"
   20.72 -
   20.73  values [depth_limit = 7] 10 "{n. even n}"
   20.74  
   20.75  definition odd' where "odd' x == \<not> even x"
   20.76 @@ -39,6 +96,14 @@
   20.77  values [depth_limit = 2] "{x. odd' 7}"
   20.78  values [depth_limit = 9] "{x. odd' 7}"
   20.79  
   20.80 +inductive is_even :: "nat \<Rightarrow> bool"
   20.81 +where
   20.82 +  "n mod 2 = 0 \<Longrightarrow> is_even n"
   20.83 +
   20.84 +code_pred is_even .
   20.85 +
   20.86 +subsection {* append predicate *}
   20.87 +
   20.88  inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   20.89      "append [] xs xs"
   20.90    | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
   20.91 @@ -60,7 +125,7 @@
   20.92  value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
   20.93  value [code] "Predicate.the (append_3 ([]::int list))"
   20.94  
   20.95 -subsection {* Tricky case with alternative rules *}
   20.96 +text {* tricky case with alternative rules *}
   20.97  
   20.98  inductive append2
   20.99  where
  20.100 @@ -78,15 +143,6 @@
  20.101    from append2.cases[OF append2(1)] append2(2-3) show thesis by blast
  20.102  qed
  20.103  
  20.104 -subsection {* Tricky cases with tuples *}
  20.105 -
  20.106 -inductive zerozero :: "nat * nat => bool"
  20.107 -where
  20.108 -  "zerozero (0, 0)"
  20.109 -
  20.110 -code_pred zerozero .
  20.111 -code_pred [rpred] zerozero .
  20.112 -
  20.113  inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
  20.114  where
  20.115    "tupled_append ([], xs, xs)"
  20.116 @@ -127,6 +183,8 @@
  20.117  code_pred [inductify] tupled_append''' .
  20.118  thm tupled_append'''.equation
  20.119  
  20.120 +subsection {* map_ofP predicate *}
  20.121 +
  20.122  inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
  20.123  where
  20.124    "map_ofP ((a, b)#xs) a b"
  20.125 @@ -135,6 +193,8 @@
  20.126  code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
  20.127  thm map_ofP.equation
  20.128  
  20.129 +subsection {* filter predicate *}
  20.130 +
  20.131  inductive filter1
  20.132  for P
  20.133  where
  20.134 @@ -168,7 +228,7 @@
  20.135  code_pred filter3 .
  20.136  code_pred [depth_limited] filter3 .
  20.137  thm filter3.depth_limited_equation
  20.138 -(*code_pred [rpred] filter3 .*)
  20.139 +
  20.140  inductive filter4
  20.141  where
  20.142    "List.filter P xs = ys ==> filter4 P xs ys"
  20.143 @@ -177,7 +237,7 @@
  20.144  code_pred [depth_limited] filter4 .
  20.145  code_pred [rpred] filter4 .
  20.146  
  20.147 -section {* reverse *}
  20.148 +subsection {* reverse predicate *}
  20.149  
  20.150  inductive rev where
  20.151      "rev [] []"
  20.152 @@ -196,6 +256,8 @@
  20.153  code_pred tupled_rev .
  20.154  thm tupled_rev.equation
  20.155  
  20.156 +subsection {* partition predicate *}
  20.157 +
  20.158  inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  20.159    for f where
  20.160      "partition f [] [] []"
  20.161 @@ -206,6 +268,11 @@
  20.162  code_pred [depth_limited] partition .
  20.163  code_pred [rpred] partition .
  20.164  
  20.165 +values 10 "{(ys, zs). partition is_even
  20.166 +  [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
  20.167 +values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
  20.168 +values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
  20.169 +
  20.170  inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
  20.171    for f where
  20.172     "tupled_partition f ([], [], [])"
  20.173 @@ -216,23 +283,13 @@
  20.174  
  20.175  thm tupled_partition.equation
  20.176  
  20.177 -
  20.178 -inductive is_even :: "nat \<Rightarrow> bool"
  20.179 -where
  20.180 -  "n mod 2 = 0 \<Longrightarrow> is_even n"
  20.181 -
  20.182 -code_pred is_even .
  20.183 -
  20.184 -values 10 "{(ys, zs). partition is_even
  20.185 -  [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
  20.186 -values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
  20.187 -values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
  20.188 -
  20.189  lemma [code_pred_intros]:
  20.190    "r a b \<Longrightarrow> tranclp r a b"
  20.191    "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
  20.192    by auto
  20.193  
  20.194 +subsection {* transitive predicate *}
  20.195 +
  20.196  code_pred tranclp
  20.197  proof -
  20.198    case tranclp
  20.199 @@ -265,7 +322,7 @@
  20.200  values 20 "{(n, m). tranclp succ n m}"
  20.201  *)
  20.202  
  20.203 -subsection{* IMP *}
  20.204 +subsection {* IMP *}
  20.205  
  20.206  types
  20.207    var = nat
  20.208 @@ -304,7 +361,7 @@
  20.209  
  20.210  code_pred tupled_exec .
  20.211  
  20.212 -subsection{* CCS *}
  20.213 +subsection {* CCS *}
  20.214  
  20.215  text{* This example formalizes finite CCS processes without communication or
  20.216  recursion. For simplicity, labels are natural numbers. *}
  20.217 @@ -354,18 +411,15 @@
  20.218  
  20.219  value [code] "Predicate.the (divmod_rel_1_2 1705 42)"
  20.220  
  20.221 -section {* Executing definitions *}
  20.222 +subsection {* Minimum *}
  20.223  
  20.224  definition Min
  20.225  where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
  20.226  
  20.227  code_pred [inductify] Min .
  20.228  
  20.229 -subsection {* Examples with lists *}
  20.230 +subsection {* Lexicographic order *}
  20.231  
  20.232 -subsubsection {* Lexicographic order *}
  20.233 -
  20.234 -thm lexord_def
  20.235  code_pred [inductify] lexord .
  20.236  code_pred [inductify, rpred] lexord .
  20.237  thm lexord.equation
  20.238 @@ -392,6 +446,7 @@
  20.239  
  20.240  values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
  20.241  values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
  20.242 +
  20.243  (*values [random] "{xys. test_lexord xys}"*)
  20.244  (*values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}"*)
  20.245  (*
  20.246 @@ -419,7 +474,7 @@
  20.247  
  20.248  thm lists.equation
  20.249  
  20.250 -section {* AVL Tree Example *}
  20.251 +subsection {* AVL Tree *}
  20.252  
  20.253  datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
  20.254  fun height :: "'a tree => nat" where
  20.255 @@ -437,7 +492,6 @@
  20.256  
  20.257  code_pred [rpred] avl .
  20.258  thm avl.rpred_equation
  20.259 -(*values [random] 10 "{t. avl (t::int tree)}"*)
  20.260  
  20.261  fun set_of
  20.262  where
  20.263 @@ -455,10 +509,11 @@
  20.264  
  20.265  code_pred [inductify] is_ord .
  20.266  thm is_ord.equation
  20.267 +
  20.268  code_pred [rpred] is_ord .
  20.269  thm is_ord.rpred_equation
  20.270  
  20.271 -section {* Definitions about Relations *}
  20.272 +subsection {* Definitions about Relations *}
  20.273  
  20.274  code_pred [inductify] converse .
  20.275  thm converse.equation
  20.276 @@ -467,7 +522,6 @@
  20.277  code_pred [inductify] Image .
  20.278  thm Image.equation
  20.279  (*TODO: *)
  20.280 -ML {* Toplevel.debug := true *}
  20.281  declare Id_on_def[unfolded UNION_def, code_pred_def]
  20.282  
  20.283  code_pred [inductify] Id_on .
  20.284 @@ -483,10 +537,6 @@
  20.285  thm refl_on.equation
  20.286  code_pred [inductify] total_on .
  20.287  thm total_on.equation
  20.288 -(*
  20.289 -code_pred [inductify] sym .
  20.290 -thm sym.equation
  20.291 -*)
  20.292  code_pred [inductify] antisym .
  20.293  thm antisym.equation
  20.294  code_pred [inductify] trans .
  20.295 @@ -496,12 +546,13 @@
  20.296  code_pred [inductify] inv_image .
  20.297  thm inv_image.equation
  20.298  
  20.299 -section {* List functions *}
  20.300 +subsection {* Inverting list functions *}
  20.301  
  20.302  code_pred [inductify] length .
  20.303 +code_pred [inductify, rpred] length .
  20.304  thm size_listP.equation
  20.305 -code_pred [inductify, rpred] length .
  20.306  thm size_listP.rpred_equation
  20.307 +
  20.308  values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}"
  20.309  
  20.310  code_pred [inductify] concat .
  20.311 @@ -509,7 +560,6 @@
  20.312  code_pred [inductify] tl .
  20.313  code_pred [inductify] last .
  20.314  code_pred [inductify] butlast .
  20.315 -(*code_pred [inductify] listsum .*)
  20.316  code_pred [inductify] take .
  20.317  code_pred [inductify] drop .
  20.318  code_pred [inductify] zip .
  20.319 @@ -526,15 +576,8 @@
  20.320  code_pred [inductify] foldl .
  20.321  code_pred [inductify] filter .
  20.322  code_pred [inductify, rpred] filter .
  20.323 -thm filterP.rpred_equation
  20.324  
  20.325 -definition test where "test xs = filter (\<lambda>x. x = (1::nat)) xs"
  20.326 -code_pred [inductify] test .
  20.327 -thm testP.equation
  20.328 -code_pred [inductify, rpred] test .
  20.329 -thm testP.rpred_equation
  20.330 -
  20.331 -section {* Context Free Grammar *}
  20.332 +subsection {* Context Free Grammar *}
  20.333  
  20.334  datatype alphabet = a | b
  20.335  
  20.336 @@ -553,79 +596,6 @@
  20.337  
  20.338  values [random] 5 "{x. S\<^isub>1p x}"
  20.339  
  20.340 -inductive is_a where
  20.341 -  "is_a a"
  20.342 -
  20.343 -inductive is_b where
  20.344 -  "is_b b"
  20.345 -
  20.346 -code_pred is_a .
  20.347 -code_pred [depth_limited] is_a .
  20.348 -code_pred [rpred] is_a .
  20.349 -
  20.350 -values [random] "{x. is_a x}"
  20.351 -code_pred [depth_limited] is_b .
  20.352 -code_pred [rpred] is_b .
  20.353 -
  20.354 -code_pred [inductify, depth_limited] filter .
  20.355 -
  20.356 -values [depth_limit=5] "{x. filterP is_a [a, b] x}"
  20.357 -values [depth_limit=3] "{x. filterP is_b [a, b] x}"
  20.358 -
  20.359 -lemma "w \<in> S\<^isub>1 \<Longrightarrow> length (filter (\<lambda>x. x = a) w) = 1"
  20.360 -(*quickcheck[generator=pred_compile, size=10]*)
  20.361 -oops
  20.362 -
  20.363 -inductive test_lemma where
  20.364 -  "S\<^isub>1p w ==> filterP is_a w r1 ==> size_listP r1 r2 ==> filterP is_b w r3 ==> size_listP r3 r4 ==> r2 \<noteq> r4 ==> test_lemma w"
  20.365 -(*
  20.366 -code_pred [rpred] test_lemma .
  20.367 -*)
  20.368 -(*
  20.369 -definition test_lemma' where
  20.370 -  "test_lemma' w == (w \<in> S\<^isub>1 \<and> (\<not> length [x <- w. x = a] = length [x <- w. x = b]))"
  20.371 -
  20.372 -code_pred [inductify, rpred] test_lemma' .
  20.373 -thm test_lemma'.rpred_equation
  20.374 -*)
  20.375 -(*thm test_lemma'.rpred_equation*)
  20.376 -(*
  20.377 -values [depth_limit=3 random] "{x. S\<^isub>1 x}"
  20.378 -*)
  20.379 -code_pred [depth_limited] is_b .
  20.380 -(*
  20.381 -code_pred [inductify, depth_limited] filter .
  20.382 -*)
  20.383 -thm filterP.intros
  20.384 -thm filterP.equation
  20.385 -(*
  20.386 -values [depth_limit=3] "{x. filterP is_b [a, b] x}"
  20.387 -find_theorems "test_lemma'_hoaux"
  20.388 -code_pred [depth_limited] test_lemma'_hoaux .
  20.389 -thm test_lemma'_hoaux.depth_limited_equation
  20.390 -values [depth_limit=2] "{x. test_lemma'_hoaux b}"
  20.391 -inductive test1 where
  20.392 -  "\<not> test_lemma'_hoaux x ==> test1 x"
  20.393 -code_pred test1 .
  20.394 -code_pred [depth_limited] test1 .
  20.395 -thm test1.depth_limited_equation
  20.396 -thm test_lemma'_hoaux.depth_limited_equation
  20.397 -thm test1.intros
  20.398 -
  20.399 -values [depth_limit=2] "{x. test1 b}"
  20.400 -
  20.401 -thm filterP.intros
  20.402 -thm filterP.depth_limited_equation
  20.403 -values [depth_limit=3] "{x. filterP test_lemma'_hoaux [a, b] x}"
  20.404 -values [depth_limit=4 random] "{w. test_lemma w}"
  20.405 -values [depth_limit=4 random] "{w. test_lemma' w}"
  20.406 -*)
  20.407 -(*
  20.408 -theorem S\<^isub>1_sound:
  20.409 -"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
  20.410 -quickcheck[generator=pred_compile, size=15]
  20.411 -oops
  20.412 -*)
  20.413  inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
  20.414    "[] \<in> S\<^isub>2"
  20.415  | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
  20.416 @@ -641,12 +611,6 @@
  20.417  
  20.418  values [random] 10 "{x. S\<^isub>2 x}"
  20.419  
  20.420 -theorem S\<^isub>2_sound:
  20.421 -"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
  20.422 -(*quickcheck[generator=SML]*)
  20.423 -(*quickcheck[generator=pred_compile, size=15, iterations=1]*)
  20.424 -oops
  20.425 -
  20.426  inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
  20.427    "[] \<in> S\<^isub>3"
  20.428  | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
  20.429 @@ -659,31 +623,6 @@
  20.430  thm S\<^isub>3.equation
  20.431  
  20.432  values 10 "{x. S\<^isub>3 x}"
  20.433 -(*
  20.434 -theorem S\<^isub>3_sound:
  20.435 -"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
  20.436 -quickcheck[generator=pred_compile, size=10, iterations=1]
  20.437 -oops
  20.438 -*)
  20.439 -lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
  20.440 -(*quickcheck[size=10, generator = pred_compile]*)
  20.441 -oops
  20.442 -(*
  20.443 -inductive test
  20.444 -where
  20.445 -  "length [x \<leftarrow> w. a = x] = length [x \<leftarrow> w. x = b] ==> test w"
  20.446 -ML {* @{term "[x \<leftarrow> w. x = a]"} *}
  20.447 -code_pred (inductify_all) test .
  20.448 -
  20.449 -thm test.equation
  20.450 -*)
  20.451 -(*
  20.452 -theorem S\<^isub>3_complete:
  20.453 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3"
  20.454 -(*quickcheck[generator=SML]*)
  20.455 -quickcheck[generator=pred_compile, size=10, iterations=100]
  20.456 -oops
  20.457 -*)
  20.458  
  20.459  inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
  20.460    "[] \<in> S\<^isub>4"
  20.461 @@ -693,25 +632,8 @@
  20.462  | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
  20.463  | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
  20.464  | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
  20.465 -(*
  20.466 -theorem S\<^isub>4_sound:
  20.467 -"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
  20.468 -quickcheck[generator = pred_compile, size=2, iterations=1]
  20.469 -oops
  20.470 -*)
  20.471 -theorem S\<^isub>4_complete:
  20.472 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
  20.473 -(*quickcheck[generator = pred_compile, size=5, iterations=1]*)
  20.474 -oops
  20.475  
  20.476 -theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
  20.477 -"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
  20.478 -"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
  20.479 -"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
  20.480 -(*quickcheck[generator = pred_compile, size=5, iterations=1]*)
  20.481 -oops
  20.482 -
  20.483 -section {* Lambda *}
  20.484 +subsection {* Lambda *}
  20.485  
  20.486  datatype type =
  20.487      Atom nat
  20.488 @@ -728,7 +650,6 @@
  20.489    "[]\<langle>i\<rangle> = None"
  20.490  | "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
  20.491  
  20.492 -
  20.493  inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
  20.494  where
  20.495    "nth_el' (x # xs) 0 x"
  20.496 @@ -738,8 +659,7 @@
  20.497    where
  20.498      Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
  20.499    | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
  20.500 -(*  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" *)
  20.501 -  | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
  20.502 +  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
  20.503  
  20.504  primrec
  20.505    lift :: "[dB, nat] => dB"
  20.506 @@ -763,15 +683,4 @@
  20.507    | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
  20.508    | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
  20.509  
  20.510 -lemma "Gamma \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> Gamma \<turnstile> t' : T"
  20.511 -(*quickcheck[generator = pred_compile, size = 10, iterations = 1]*)
  20.512 -oops
  20.513 -
  20.514 -lemma filter_eq_ConsD:
  20.515 - "filter P ys = x#xs \<Longrightarrow>
  20.516 -  \<exists>us vs. ys = ts @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  20.517 -(*quickcheck[generator = pred_compile]*)
  20.518 -oops
  20.519 -
  20.520 -
  20.521  end
  20.522 \ No newline at end of file