# HG changeset patch # User bulwahn # Date 1256655698 -3600 # Node ID f8d43d5215c21562c01bfceba3c39897ecccadfd # Parent 2ac8ef0342b470fac4851f28dd38d39ce032615c# Parent f93390060bbe0a3209828bcffdfcbeed16a6986c merged diff -r f93390060bbe -r f8d43d5215c2 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Oct 27 14:40:24 2009 +0100 +++ b/src/HOL/IsaMakefile Tue Oct 27 16:01:38 2009 +0100 @@ -255,6 +255,7 @@ Map.thy \ Nat_Numeral.thy \ Presburger.thy \ + Predicate_Compile.thy \ Quickcheck.thy \ Random.thy \ Recdef.thy \ @@ -283,6 +284,13 @@ Tools/numeral_simprocs.ML \ Tools/numeral_syntax.ML \ Tools/polyhash.ML \ + Tools/Predicate_Compile/predicate_compile_aux.ML \ + Tools/Predicate_Compile/predicate_compile_core.ML \ + Tools/Predicate_Compile/predicate_compile_data.ML \ + Tools/Predicate_Compile/predicate_compile_fun.ML \ + Tools/Predicate_Compile/predicate_compile.ML \ + Tools/Predicate_Compile/predicate_compile_pred.ML \ + Tools/Predicate_Compile/predicate_compile_set.ML \ Tools/quickcheck_generators.ML \ Tools/Qelim/cooper_data.ML \ Tools/Qelim/cooper.ML \ @@ -945,7 +953,7 @@ ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \ - ex/Predicate_Compile.thy ex/Predicate_Compile_ex.thy \ + ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \ ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \ ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Main.thy --- a/src/HOL/Main.thy Tue Oct 27 14:40:24 2009 +0100 +++ b/src/HOL/Main.thy Tue Oct 27 16:01:38 2009 +0100 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Nitpick Quickcheck Recdef +imports Plain Nitpick Predicate_Compile Recdef begin text {* diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Predicate_Compile.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Predicate_Compile.thy Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,19 @@ +(* Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen *) + +header {* A compiler for predicates defined by introduction rules *} + +theory Predicate_Compile +imports Quickcheck +uses + "Tools/Predicate_Compile/predicate_compile_aux.ML" + "Tools/Predicate_Compile/predicate_compile_core.ML" + "Tools/Predicate_Compile/predicate_compile_set.ML" + "Tools/Predicate_Compile/predicate_compile_data.ML" + "Tools/Predicate_Compile/predicate_compile_fun.ML" + "Tools/Predicate_Compile/predicate_compile_pred.ML" + "Tools/Predicate_Compile/predicate_compile.ML" +begin + +setup {* Predicate_Compile.setup *} + +end \ No newline at end of file diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Tue Oct 27 14:40:24 2009 +0100 +++ b/src/HOL/Quickcheck.thy Tue Oct 27 16:01:38 2009 +0100 @@ -126,6 +126,47 @@ shows "random_aux k = rhs k" using assms by (rule code_numeral.induct) +subsection {* the Random-Predicate Monad *} + +types 'a randompred = "Random.seed \ ('a Predicate.pred \ Random.seed)" + +definition empty :: "'a randompred" + where "empty = Pair (bot_class.bot)" + +definition single :: "'a => 'a randompred" + where "single x = Pair (Predicate.single x)" + +definition bind :: "'a randompred \ ('a \ 'b randompred) \ 'b randompred" + where + "bind R f = (\s. let + (P, s') = R s; + (s1, s2) = Random.split_seed s' + in (Predicate.bind P (%a. fst (f a s1)), s2))" + +definition union :: "'a randompred \ 'a randompred \ 'a randompred" +where + "union R1 R2 = (\s. let + (P1, s') = R1 s; (P2, s'') = R2 s' + in (upper_semilattice_class.sup P1 P2, s''))" + +definition if_randompred :: "bool \ unit randompred" +where + "if_randompred b = (if b then single () else empty)" + +definition not_randompred :: "unit randompred \ unit randompred" +where + "not_randompred P = (\s. let + (P', s') = P s + in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" + +definition Random :: "(Random.seed \ ('a \ (unit \ term)) \ Random.seed) \ 'a randompred" + where "Random g = scomp g (Pair o (Predicate.single o fst))" + +definition map :: "('a \ 'b) \ ('a randompred \ 'b randompred)" + where "map f P = bind P (single o f)" + +subsection {* Code setup *} + use "Tools/quickcheck_generators.ML" setup {* Quickcheck_Generators.setup *} @@ -136,8 +177,10 @@ code_reserved Quickcheck Quickcheck_Generators - +hide (open) fact empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def +hide (open) type randompred hide (open) const random collapse beyond random_fun_aux random_fun_lift + empty single bind union if_randompred not_randompred Random map no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\" 60) diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Tue Oct 27 14:40:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,236 +0,0 @@ -(* Author: Lukas Bulwahn, TU Muenchen - -Auxilary functions for predicate compiler -*) - -structure Predicate_Compile_Aux = -struct - -(* general syntactic functions *) - -(*Like dest_conj, but flattens conjunctions however nested*) -fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) - | conjuncts_aux t conjs = t::conjs; - -fun conjuncts t = conjuncts_aux t []; - -(* syntactic functions *) - -fun is_equationlike_term (Const ("==", _) $ _ $ _) = true - | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true - | is_equationlike_term _ = false - -val is_equationlike = is_equationlike_term o prop_of - -fun is_pred_equation_term (Const ("==", _) $ u $ v) = - (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool}) - | is_pred_equation_term _ = false - -val is_pred_equation = is_pred_equation_term o prop_of - -fun is_intro_term constname t = - case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of - Const (c, _) => c = constname - | _ => false - -fun is_intro constname t = is_intro_term constname (prop_of t) - -fun is_pred thy constname = - let - val T = (Sign.the_const_type thy constname) - in body_type T = @{typ "bool"} end; - - -fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT) - | is_predT _ = false - - -(*** check if a term contains only constructor functions ***) -fun is_constrt thy = - let - val cnstrs = flat (maps - (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) - (Symtab.dest (Datatype.get_all thy))); - fun check t = (case strip_comb t of - (Free _, []) => true - | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of - (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts - | _ => false) - | _ => false) - in check end; - -fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) = - let - val (xTs, t') = strip_ex t - in - ((x, T) :: xTs, t') - end - | strip_ex t = ([], t) - -fun focus_ex t nctxt = - let - val ((xs, Ts), t') = apfst split_list (strip_ex t) - val (xs', nctxt') = Name.variants xs nctxt; - val ps' = xs' ~~ Ts; - val vs = map Free ps'; - val t'' = Term.subst_bounds (rev vs, t'); - in ((ps', t''), nctxt') end; - - -(* introduction rule combinators *) - -(* combinators to apply a function to all literals of an introduction rules *) - -fun map_atoms f intro = - let - val (literals, head) = Logic.strip_horn intro - fun appl t = (case t of - (@{term "Not"} $ t') => HOLogic.mk_not (f t') - | _ => f t) - in - Logic.list_implies - (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head) - end - -fun fold_atoms f intro s = - let - val (literals, head) = Logic.strip_horn intro - fun appl t s = (case t of - (@{term "Not"} $ t') => f t' s - | _ => f t s) - in fold appl (map HOLogic.dest_Trueprop literals) s end - -fun fold_map_atoms f intro s = - let - val (literals, head) = Logic.strip_horn intro - fun appl t s = (case t of - (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s) - | _ => f t s) - val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s - in - (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') - end; - -fun maps_premises f intro = - let - val (premises, head) = Logic.strip_horn intro - in - Logic.list_implies (maps f premises, head) - end - -(* lifting term operations to theorems *) - -fun map_term thy f th = - Skip_Proof.make_thm thy (f (prop_of th)) - -(* -fun equals_conv lhs_cv rhs_cv ct = - case Thm.term_of ct of - Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct - | _ => error "equals_conv" -*) - -(* Different options for compiler *) - -datatype options = Options of { - expected_modes : (string * int list list) option, - show_steps : bool, - show_mode_inference : bool, - show_proof_trace : bool, - show_intermediate_results : bool, - show_compilation : bool, - skip_proof : bool, - - inductify : bool, - rpred : bool, - depth_limited : bool -}; - -fun expected_modes (Options opt) = #expected_modes opt -fun show_steps (Options opt) = #show_steps opt -fun show_mode_inference (Options opt) = #show_mode_inference opt -fun show_intermediate_results (Options opt) = #show_intermediate_results opt -fun show_proof_trace (Options opt) = #show_proof_trace opt -fun show_compilation (Options opt) = #show_compilation opt -fun skip_proof (Options opt) = #skip_proof opt - -fun is_inductify (Options opt) = #inductify opt -fun is_rpred (Options opt) = #rpred opt -fun is_depth_limited (Options opt) = #depth_limited opt - -val default_options = Options { - expected_modes = NONE, - show_steps = false, - show_intermediate_results = false, - show_proof_trace = false, - show_mode_inference = false, - show_compilation = false, - skip_proof = false, - - inductify = false, - rpred = false, - depth_limited = false -} - - -fun print_step options s = - if show_steps options then tracing s else () - -(* tuple processing *) - -fun expand_tuples thy intro = - let - fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) - | rewrite_args (arg::args) (pats, intro_t, ctxt) = - (case HOLogic.strip_tupleT (fastype_of arg) of - (Ts as _ :: _ :: _) => - let - fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) - (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) - | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = - let - val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt - val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) - val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t - val args' = map (Pattern.rewrite_term thy [pat] []) args - in - rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) - end - | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) - val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) - (args, (pats, intro_t, ctxt)) - in - rewrite_args args' (pats, intro_t', ctxt') - end - | _ => rewrite_args args (pats, intro_t, ctxt)) - fun rewrite_prem atom = - let - val (_, args) = strip_comb atom - in rewrite_args args end - val ctxt = ProofContext.init thy - val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt - val intro_t = prop_of intro' - val concl = Logic.strip_imp_concl intro_t - val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) - val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) - val (pats', intro_t', ctxt3) = - fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) - fun rewrite_pat (ct1, ct2) = - (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) - val t_insts' = map rewrite_pat t_insts - val intro'' = Thm.instantiate (T_insts, t_insts') intro - val [intro'''] = Variable.export ctxt3 ctxt [intro''] - val intro'''' = Simplifier.full_simplify - (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) - intro''' - (* splitting conjunctions introduced by Pair_eq*) - fun split_conj prem = - map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem)) - val intro''''' = map_term thy (maps_premises split_conj) intro'''' - in - intro''''' - end - - - -end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Tue Oct 27 14:40:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,210 +0,0 @@ -(* Author: Lukas Bulwahn, TU Muenchen - -Book-keeping datastructure for the predicate compiler - -*) -signature PREDICATE_COMPILE_DATA = -sig - type specification_table; - val make_const_spec_table : theory -> specification_table - val get_specification : specification_table -> string -> thm list - val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T - val normalize_equation : theory -> thm -> thm -end; - -structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = -struct - -open Predicate_Compile_Aux; - -structure Data = TheoryDataFun -( - type T = - {const_spec_table : thm list Symtab.table}; - val empty = - {const_spec_table = Symtab.empty}; - val copy = I; - val extend = I; - fun merge _ - ({const_spec_table = const_spec_table1}, - {const_spec_table = const_spec_table2}) = - {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)} -); - -fun mk_data c = {const_spec_table = c} -fun map_data f {const_spec_table = c} = mk_data (f c) - -type specification_table = thm list Symtab.table - -fun defining_const_of_introrule_term t = - let - val _ $ u = Logic.strip_imp_concl t - val (pred, all_args) = strip_comb u - in case pred of - Const (c, T) => c - | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) - end - -val defining_const_of_introrule = defining_const_of_introrule_term o prop_of - -(*TODO*) -fun is_introlike_term t = true - -val is_introlike = is_introlike_term o prop_of - -fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) = - (case strip_comb u of - (Const (c, T), args) => - if (length (binder_types T) = length args) then - true - else - raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t]) - | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t])) - | check_equation_format_term t = - raise TERM ("check_equation_format_term failed: Not an equation", [t]) - -val check_equation_format = check_equation_format_term o prop_of - -fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) = - (case fst (strip_comb u) of - Const (c, _) => c - | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t])) - | defining_const_of_equation_term t = - raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) - -val defining_const_of_equation = defining_const_of_equation_term o prop_of - -(* Normalizing equations *) - -fun mk_meta_equation th = - case prop_of th of - Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection} - | _ => th - -val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} - -fun full_fun_cong_expand th = - let - val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th))) - val i = length (binder_types (fastype_of f)) - length args - in funpow i (fn th => th RS meta_fun_cong) th end; - -fun declare_names s xs ctxt = - let - val res = Name.names ctxt s xs - in (res, fold Name.declare (map fst res) ctxt) end - -fun split_all_pairs thy th = - let - val ctxt = ProofContext.init thy - val ((_, [th']), ctxt') = Variable.import true [th] ctxt - val t = prop_of th' - val frees = Term.add_frees t [] - val freenames = Term.add_free_names t [] - val nctxt = Name.make_context freenames - fun mk_tuple_rewrites (x, T) nctxt = - let - val Ts = HOLogic.flatten_tupleT T - val (xTs, nctxt') = declare_names x Ts nctxt - val paths = HOLogic.flat_tupleT_paths T - in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end - val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt - val t' = Pattern.rewrite_term thy rewr [] t - val tac = Skip_Proof.cheat_tac thy - val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac) - val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th'' - in - th''' - end; - -fun normalize_equation thy th = - mk_meta_equation th - |> Predicate_Compile_Set.unfold_set_notation - |> full_fun_cong_expand - |> split_all_pairs thy - |> tap check_equation_format - -fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite -((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th - -fun store_thm_in_table ignore_consts thy th= - let - val th = th - |> inline_equations thy - |> Predicate_Compile_Set.unfold_set_notation - |> AxClass.unoverload thy - val (const, th) = - if is_equationlike th then - let - val eq = normalize_equation thy th - in - (defining_const_of_equation eq, eq) - end - else if (is_introlike th) then (defining_const_of_introrule th, th) - else error "store_thm: unexpected definition format" - in - if not (member (op =) ignore_consts const) then - Symtab.cons_list (const, th) - else I - end - -fun make_const_spec_table thy = - let - fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy))) - val table = Symtab.empty - |> store [] Predicate_Compile_Alternative_Defs.get - val ignore_consts = Symtab.keys table - in - table - |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get - |> store ignore_consts Nitpick_Simps.get - |> store ignore_consts Nitpick_Intros.get - end - -fun get_specification table constname = - case Symtab.lookup table constname of - SOME thms => thms - | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed") - -val logic_operator_names = - [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, - @{const_name "op &"}] - -val special_cases = member (op =) [ - @{const_name "False"}, - @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat}, - @{const_name Nat.one_nat_inst.one_nat}, -@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"}, -@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus}, -@{const_name Nat.ord_nat_inst.less_eq_nat}, -@{const_name number_nat_inst.number_of_nat}, - @{const_name Int.Bit0}, - @{const_name Int.Bit1}, - @{const_name Int.Pls}, -@{const_name "Int.zero_int_inst.zero_int"}, -@{const_name "List.filter"}] - -fun case_consts thy s = is_some (Datatype.info_of_case thy s) - -fun obtain_specification_graph thy table constname = - let - fun is_nondefining_constname c = member (op =) logic_operator_names c - val is_defining_constname = member (op =) (Symtab.keys table) - fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c) - fun defiants_of specs = - fold (Term.add_const_names o prop_of) specs [] - |> filter is_defining_constname - |> filter_out is_nondefining_constname - |> filter_out has_code_pred_intros - |> filter_out (case_consts thy) - |> filter_out special_cases - fun extend constname = - let - val specs = get_specification table constname - in (specs, defiants_of specs) end; - in - Graph.extend extend constname Graph.empty - end; - - -end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Tue Oct 27 14:40:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,189 +0,0 @@ -(* Author: Lukas Bulwahn, TU Muenchen - -Preprocessing definitions of predicates to introduction rules -*) - -signature PREDICATE_COMPILE_PRED = -sig - (* preprocesses an equation to a set of intro rules; defines new constants *) - (* - val preprocess_pred_equation : thm -> theory -> thm list * theory - *) - val preprocess : string -> theory -> (thm list list * theory) - (* output is the term list of clauses of an unknown predicate *) - val preprocess_term : term -> theory -> (term list * theory) - - (*val rewrite : thm -> thm*) - -end; -(* : PREDICATE_COMPILE_PREPROC_PRED *) -structure Predicate_Compile_Pred = -struct - -open Predicate_Compile_Aux - -fun is_compound ((Const ("Not", _)) $ t) = - error "is_compound: Negation should not occur; preprocessing is defect" - | is_compound ((Const ("Ex", _)) $ _) = true - | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true - | is_compound ((Const ("op &", _)) $ _ $ _) = - error "is_compound: Conjunction should not occur; preprocessing is defect" - | is_compound _ = false - -fun flatten constname atom (defs, thy) = - if is_compound atom then - let - val constname = Name.variant (map (Long_Name.base_name o fst) defs) - ((Long_Name.base_name constname) ^ "_aux") - val full_constname = Sign.full_bname thy constname - val (params, args) = List.partition (is_predT o fastype_of) - (map Free (Term.add_frees atom [])) - val constT = map fastype_of (params @ args) ---> HOLogic.boolT - val lhs = list_comb (Const (full_constname, constT), params @ args) - val def = Logic.mk_equals (lhs, atom) - val ([definition], thy') = thy - |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] - |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] - in - (lhs, ((full_constname, [definition]) :: defs, thy')) - end - else - (atom, (defs, thy)) - -fun flatten_intros constname intros thy = - let - val ctxt = ProofContext.init thy - val ((_, intros), ctxt') = Variable.import true intros ctxt - val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms) - (flatten constname) (map prop_of intros) ([], thy) - val tac = fn _ => Skip_Proof.cheat_tac thy' - val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros' - |> Variable.export ctxt' ctxt - in - (intros'', (local_defs, thy')) - end - -(* TODO: same function occurs in inductive package *) -fun select_disj 1 1 = [] - | select_disj _ 1 = [rtac @{thm disjI1}] - | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1)); - -fun introrulify thy ths = - let - val ctxt = ProofContext.init thy - val ((_, ths'), ctxt') = Variable.import true ths ctxt - fun introrulify' th = - let - val (lhs, rhs) = Logic.dest_equals (prop_of th) - val frees = Term.add_free_names rhs [] - val disjuncts = HOLogic.dest_disj rhs - val nctxt = Name.make_context frees - fun mk_introrule t = - let - val ((ps, t'), nctxt') = focus_ex t nctxt - val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t') - in - (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs)) - end - val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o - Logic.dest_implies o prop_of) @{thm exI} - fun prove_introrule (index, (ps, introrule)) = - let - val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1 - THEN EVERY1 (select_disj (length disjuncts) (index + 1)) - THEN (EVERY (map (fn y => - rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps)) - THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1) - THEN TRY (atac 1) - in - Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac) - end - in - map_index prove_introrule (map mk_introrule disjuncts) - end - in maps introrulify' ths' |> Variable.export ctxt' ctxt end - -val rewrite = - Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}]) - #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) - #> Conv.fconv_rule nnf_conv - #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}]) - -val rewrite_intros = - Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)}) - -fun preprocess (constname, specs) thy = - let - val ctxt = ProofContext.init thy - val intros = - if forall is_pred_equation specs then - introrulify thy (map rewrite specs) - else if forall (is_intro constname) specs then - map rewrite_intros specs - else - error ("unexpected specification for constant " ^ quote constname ^ ":\n" - ^ commas (map (quote o Display.string_of_thm_global thy) specs)) - val (intros', (local_defs, thy')) = flatten_intros constname intros thy - val (intross, thy'') = fold_map preprocess local_defs thy' - in - ((constname, intros') :: flat intross,thy'') - end; - -fun preprocess_term t thy = error "preprocess_pred_term: to implement" - -fun is_Abs (Abs _) = true - | is_Abs _ = false - -fun flat_higher_order_arguments (intross, thy) = - let - fun process constname atom (new_defs, thy) = - let - val (pred, args) = strip_comb atom - val abs_args = filter is_Abs args - fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = - let - val _ = tracing ("Introduce new constant for " ^ - Syntax.string_of_term_global thy abs_arg) - val vars = map Var (Term.add_vars abs_arg []) - val abs_arg' = Logic.unvarify abs_arg - val frees = map Free (Term.add_frees abs_arg' []) - val constname = Name.variant (map (Long_Name.base_name o fst) new_defs) - ((Long_Name.base_name constname) ^ "_hoaux") - val full_constname = Sign.full_bname thy constname - val constT = map fastype_of frees ---> (fastype_of abs_arg') - val const = Const (full_constname, constT) - val lhs = list_comb (const, frees) - val def = Logic.mk_equals (lhs, abs_arg') - val _ = tracing (Syntax.string_of_term_global thy def) - val ([definition], thy') = thy - |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] - |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] - in - (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy')) - end - | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy)) - val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy) - in - (list_comb (pred, args'), (new_defs', thy')) - end - fun flat_intro intro (new_defs, thy) = - let - val constname = fst (dest_Const (fst (strip_comb - (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro)))))) - val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy) - val th = Skip_Proof.make_thm thy intro_ts - in - (th, (new_defs, thy)) - end - fun fold_map_spec f [] s = ([], s) - | fold_map_spec f ((c, ths) :: specs) s = - let - val (ths', s') = f ths s - val (specs', s'') = fold_map_spec f specs s' - in ((c, ths') :: specs', s'') end - val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy) - in - (intross', (new_defs, thy')) - end - -end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Tue Oct 27 14:40:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -(* Author: Lukas Bulwahn, TU Muenchen - -A quickcheck generator based on the predicate compiler -*) - -signature PREDICATE_COMPILE_QUICKCHECK = -sig - val quickcheck : Proof.context -> term -> int -> term list option - val test_ref : - ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref -end; - -structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = -struct - -val test_ref = - Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) - -val target = "Quickcheck" - -fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs -val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns) -val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns) -val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.rpred_compfuns) -val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.rpred_compfuns) -val lift_pred = #lift_pred (dest_compfuns Predicate_Compile_Core.rpred_compfuns) - -fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t) - | mk_split_lambda [x] t = lambda x t - | mk_split_lambda xs t = - let - fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) - | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) - in - mk_split_lambda' xs t - end; - -fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B - | strip_imp_prems _ = []; - -fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B - | strip_imp_concl A = A : term; - -fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); - -fun quickcheck ctxt t = - let - val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) - val ctxt' = ProofContext.theory (Context.copy_thy) ctxt - val thy = (ProofContext.theory_of ctxt') - val (vs, t') = strip_abs t - val vs' = Variable.variant_frees ctxt' [] vs - val t'' = subst_bounds (map Free (rev vs'), t') - val (prems, concl) = strip_horn t'' - val constname = "pred_compile_quickcheck" - val full_constname = Sign.full_bname thy constname - val constT = map snd vs' ---> @{typ bool} - val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy - val t = Logic.list_implies - (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), - HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) - val tac = fn _ => Skip_Proof.cheat_tac thy' - val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac - val _ = tracing (Display.string_of_thm ctxt' intro) - val thy'' = thy' - |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) - |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname - (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*) - (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) - (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *) - val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname - val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname - val prog = - if member (op =) modes ([], []) then - let - val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], []) - val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs'))) - in Const (name, T) $ @{term True} $ Bound 0 end - else if member (op =) depth_limited_modes ([], []) then - let - val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) - val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) - in lift_pred (Const (name, T) $ Bound 0) end - else error "Predicate Compile Quickcheck failed" - val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog, - mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} - (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) - val _ = tracing (Syntax.string_of_term ctxt' qc_term) - val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) - (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) - thy'' qc_term [] - in - ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield)) - end - -end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/pred_compile_set.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Tue Oct 27 14:40:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,52 +0,0 @@ -(* Author: Lukas Bulwahn, TU Muenchen - -Preprocessing sets to predicates -*) - -signature PREDICATE_COMPILE_SET = -sig -(* - val preprocess_intro : thm -> theory -> thm * theory - val preprocess_clause : term -> theory -> term * theory -*) - val unfold_set_notation : thm -> thm; -end; - -structure Predicate_Compile_Set : PREDICATE_COMPILE_SET = -struct -(*FIXME: unfolding Ball in pretty adhoc here *) -val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, -@{thm Ball_def}, @{thm Bex_def}] - -val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas - -(* -fun find_set_theorems ctxt cname = - let - val _ = cname -*) - -(* -fun preprocess_term t ctxt = - case t of - Const ("op :", _) $ x $ A => - case strip_comb A of - (Const (cname, T), params) => - let - val _ = find_set_theorems - in - (t, ctxt) - end - | _ => (t, ctxt) - | _ => (t, ctxt) -*) -(* -fun preprocess_intro th thy = - let - val cnames = find_heads_of_prems - val set_cname = filter (has_set_definition - val _ = define_preds - val _ = prep_pred_def - in -*) -end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Oct 27 14:40:24 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Oct 27 16:01:38 2009 +0100 @@ -99,7 +99,7 @@ let val _ = print_step options "Fetching definitions from theory..." val table = Predicate_Compile_Data.make_const_spec_table thy - val gr = Predicate_Compile_Data.obtain_specification_graph thy table const + val gr = Predicate_Compile_Data.obtain_specification_graph options thy table const val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr in fold_rev (preprocess_strong_conn_constnames options gr) (Graph.strong_conn gr) thy @@ -114,6 +114,7 @@ show_steps = chk "show_steps", show_intermediate_results = chk "show_intermediate_results", show_proof_trace = chk "show_proof_trace", + show_modes = chk "show_modes", show_mode_inference = chk "show_mode_inference", show_compilation = chk "show_compilation", skip_proof = chk "skip_proof", @@ -146,7 +147,7 @@ val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup -val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", +val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"] local structure P = OuterParse diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,239 @@ +(* Author: Lukas Bulwahn, TU Muenchen + +Auxilary functions for predicate compiler +*) + +structure Predicate_Compile_Aux = +struct + +(* general syntactic functions *) + +(*Like dest_conj, but flattens conjunctions however nested*) +fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) + | conjuncts_aux t conjs = t::conjs; + +fun conjuncts t = conjuncts_aux t []; + +(* syntactic functions *) + +fun is_equationlike_term (Const ("==", _) $ _ $ _) = true + | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true + | is_equationlike_term _ = false + +val is_equationlike = is_equationlike_term o prop_of + +fun is_pred_equation_term (Const ("==", _) $ u $ v) = + (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool}) + | is_pred_equation_term _ = false + +val is_pred_equation = is_pred_equation_term o prop_of + +fun is_intro_term constname t = + case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of + Const (c, _) => c = constname + | _ => false + +fun is_intro constname t = is_intro_term constname (prop_of t) + +fun is_pred thy constname = + let + val T = (Sign.the_const_type thy constname) + in body_type T = @{typ "bool"} end; + + +fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT) + | is_predT _ = false + + +(*** check if a term contains only constructor functions ***) +fun is_constrt thy = + let + val cnstrs = flat (maps + (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) + (Symtab.dest (Datatype.get_all thy))); + fun check t = (case strip_comb t of + (Free _, []) => true + | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of + (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts + | _ => false) + | _ => false) + in check end; + +fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) = + let + val (xTs, t') = strip_ex t + in + ((x, T) :: xTs, t') + end + | strip_ex t = ([], t) + +fun focus_ex t nctxt = + let + val ((xs, Ts), t') = apfst split_list (strip_ex t) + val (xs', nctxt') = Name.variants xs nctxt; + val ps' = xs' ~~ Ts; + val vs = map Free ps'; + val t'' = Term.subst_bounds (rev vs, t'); + in ((ps', t''), nctxt') end; + + +(* introduction rule combinators *) + +(* combinators to apply a function to all literals of an introduction rules *) + +fun map_atoms f intro = + let + val (literals, head) = Logic.strip_horn intro + fun appl t = (case t of + (@{term "Not"} $ t') => HOLogic.mk_not (f t') + | _ => f t) + in + Logic.list_implies + (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head) + end + +fun fold_atoms f intro s = + let + val (literals, head) = Logic.strip_horn intro + fun appl t s = (case t of + (@{term "Not"} $ t') => f t' s + | _ => f t s) + in fold appl (map HOLogic.dest_Trueprop literals) s end + +fun fold_map_atoms f intro s = + let + val (literals, head) = Logic.strip_horn intro + fun appl t s = (case t of + (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s) + | _ => f t s) + val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s + in + (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') + end; + +fun maps_premises f intro = + let + val (premises, head) = Logic.strip_horn intro + in + Logic.list_implies (maps f premises, head) + end + +(* lifting term operations to theorems *) + +fun map_term thy f th = + Skip_Proof.make_thm thy (f (prop_of th)) + +(* +fun equals_conv lhs_cv rhs_cv ct = + case Thm.term_of ct of + Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct + | _ => error "equals_conv" +*) + +(* Different options for compiler *) + +datatype options = Options of { + expected_modes : (string * int list list) option, + show_steps : bool, + show_proof_trace : bool, + show_intermediate_results : bool, + show_mode_inference : bool, + show_modes : bool, + show_compilation : bool, + skip_proof : bool, + + inductify : bool, + rpred : bool, + depth_limited : bool +}; + +fun expected_modes (Options opt) = #expected_modes opt +fun show_steps (Options opt) = #show_steps opt +fun show_intermediate_results (Options opt) = #show_intermediate_results opt +fun show_proof_trace (Options opt) = #show_proof_trace opt +fun show_modes (Options opt) = #show_modes opt +fun show_mode_inference (Options opt) = #show_mode_inference opt +fun show_compilation (Options opt) = #show_compilation opt +fun skip_proof (Options opt) = #skip_proof opt + +fun is_inductify (Options opt) = #inductify opt +fun is_rpred (Options opt) = #rpred opt +fun is_depth_limited (Options opt) = #depth_limited opt + +val default_options = Options { + expected_modes = NONE, + show_steps = false, + show_intermediate_results = false, + show_proof_trace = false, + show_modes = false, + show_mode_inference = false, + show_compilation = false, + skip_proof = false, + + inductify = false, + rpred = false, + depth_limited = false +} + + +fun print_step options s = + if show_steps options then tracing s else () + +(* tuple processing *) + +fun expand_tuples thy intro = + let + fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) + | rewrite_args (arg::args) (pats, intro_t, ctxt) = + (case HOLogic.strip_tupleT (fastype_of arg) of + (Ts as _ :: _ :: _) => + let + fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) + (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) + | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = + let + val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt + val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) + val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t + val args' = map (Pattern.rewrite_term thy [pat] []) args + in + rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) + end + | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) + val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) + (args, (pats, intro_t, ctxt)) + in + rewrite_args args' (pats, intro_t', ctxt') + end + | _ => rewrite_args args (pats, intro_t, ctxt)) + fun rewrite_prem atom = + let + val (_, args) = strip_comb atom + in rewrite_args args end + val ctxt = ProofContext.init thy + val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt + val intro_t = prop_of intro' + val concl = Logic.strip_imp_concl intro_t + val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) + val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) + val (pats', intro_t', ctxt3) = + fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) + fun rewrite_pat (ct1, ct2) = + (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) + val t_insts' = map rewrite_pat t_insts + val intro'' = Thm.instantiate (T_insts, t_insts') intro + val [intro'''] = Variable.export ctxt3 ctxt [intro''] + val intro'''' = Simplifier.full_simplify + (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) + intro''' + (* splitting conjunctions introduced by Pair_eq*) + fun split_conj prem = + map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem)) + val intro''''' = map_term thy (maps_premises split_conj) intro'''' + in + intro''''' + end + + + +end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 27 14:40:24 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 27 16:01:38 2009 +0100 @@ -49,15 +49,13 @@ mk_sup : term * term -> term, mk_if : term -> term, mk_not : term -> term, - mk_map : typ -> typ -> term -> term -> term, - lift_pred : term -> term + mk_map : typ -> typ -> term -> term -> term }; val pred_compfuns : compilation_funs - val rpred_compfuns : compilation_funs - (* val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory + val randompred_compfuns : compilation_funs + val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory - *) end; structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE = @@ -333,10 +331,12 @@ (* diagnostic display functions *) -fun print_modes modes = - Output.tracing ("Inferred modes:\n" ^ - cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map - string_of_mode ms)) modes)); +fun print_modes options modes = + if show_modes options then + Output.tracing ("Inferred modes:\n" ^ + cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map + string_of_mode ms)) modes)) + else () fun print_pred_mode_table string_of_entry thy pred_mode_table = let @@ -720,12 +720,6 @@ PredData.map (Graph.map_node pred (map_pred_data set)) end -(** data structures for generic compilation for different monads **) - -(* maybe rename functions more generic: - mk_predT -> mk_monadT; dest_predT -> dest_monadT - mk_single -> mk_return (?) -*) datatype compilation_funs = CompilationFuns of { mk_predT : typ -> typ, dest_predT : typ -> typ, @@ -735,8 +729,7 @@ mk_sup : term * term -> term, mk_if : term -> term, mk_not : term -> term, - mk_map : typ -> typ -> term -> term -> term, - lift_pred : term -> term + mk_map : typ -> typ -> term -> term -> term }; fun mk_predT (CompilationFuns funs) = #mk_predT funs @@ -748,7 +741,6 @@ fun mk_if (CompilationFuns funs) = #mk_if funs fun mk_not (CompilationFuns funs) = #mk_not funs fun mk_map (CompilationFuns funs) = #mk_map funs -fun lift_pred (CompilationFuns funs) = #lift_pred funs fun funT_of compfuns (iss, is) T = let @@ -766,9 +758,9 @@ structure PredicateCompFuns = struct -fun mk_predT T = Type (@{type_name "Predicate.pred"}, [T]) +fun mk_predT T = Type (@{type_name Predicate.pred}, [T]) -fun dest_predT (Type (@{type_name "Predicate.pred"}, [T])) = T +fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T | dest_predT T = raise TYPE ("dest_predT", [T], []); fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T); @@ -807,75 +799,65 @@ fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map}, (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp; -val lift_pred = I - val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not, - mk_map = mk_map, lift_pred = lift_pred}; + mk_map = mk_map}; end; -structure RPredCompFuns = +structure RandomPredCompFuns = struct -fun mk_rpredT T = - @{typ "Random.seed"} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ "Random.seed"}) +fun mk_randompredT T = + @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed}) -fun dest_rpredT (Type ("fun", [_, - Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T - | dest_rpredT T = raise TYPE ("dest_rpredT", [T], []); +fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"}, + [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T + | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []); -fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T) +fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T) fun mk_single t = let val T = fastype_of t in - Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t + Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t end; fun mk_bind (x, f) = let val T as (Type ("fun", [_, U])) = fastype_of f in - Const (@{const_name RPred.bind}, fastype_of x --> T --> U) $ x $ f + Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f end -val mk_sup = HOLogic.mk_binop @{const_name RPred.supp} - -fun mk_if cond = Const (@{const_name RPred.if_rpred}, - HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond; +val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union} -fun mk_not t = let val T = mk_rpredT HOLogic.unitT - in Const (@{const_name RPred.not_rpred}, T --> T) $ t end - -fun mk_map T1 T2 tf tp = Const (@{const_name RPred.map}, - (T1 --> T2) --> mk_rpredT T1 --> mk_rpredT T2) $ tf $ tp +fun mk_if cond = Const (@{const_name Quickcheck.if_randompred}, + HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond; -fun lift_pred t = - let - val T = PredicateCompFuns.dest_predT (fastype_of t) - val lift_predT = PredicateCompFuns.mk_predT T --> mk_rpredT T - in - Const (@{const_name "RPred.lift_pred"}, lift_predT) $ t - end; +fun mk_not t = let val T = mk_randompredT HOLogic.unitT + in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end -val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot, +fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map}, + (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp + +val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not, - mk_map = mk_map, lift_pred = lift_pred}; + mk_map = mk_map}; end; (* for external use with interactive mode *) val pred_compfuns = PredicateCompFuns.compfuns -val rpred_compfuns = RPredCompFuns.compfuns; +val randompred_compfuns = RandomPredCompFuns.compfuns; fun lift_random random = let val T = dest_randomT (fastype_of random) in - Const (@{const_name lift_random}, (@{typ Random.seed} --> + Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} --> HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> - RPredCompFuns.mk_rpredT T) $ random + RandomPredCompFuns.mk_randompredT T) $ random end; fun depth_limited_funT_of compfuns (iss, is) T = @@ -1604,7 +1586,7 @@ val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs in (paramTs' @ inargTs @ [@{typ code_numeral}]) ---> - (mk_predT RPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) + (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) end fun rpred_create_definitions preds (name, modes) thy = @@ -2169,7 +2151,7 @@ val moded_clauses = #infer_modes steps options thy extra_modes all_modes param_vs clauses val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes options modes - val _ = print_modes modes + val _ = print_modes options modes (*val _ = print_moded_clauses thy moded_clauses*) val _ = print_step options "Defining executable functions..." val thy' = fold (#create_definitions steps preds) modes thy @@ -2291,7 +2273,7 @@ val add_quickcheck_equations = gen_add_equations {infer_modes = infer_modes_with_generator, create_definitions = rpred_create_definitions, - compile_preds = compile_preds rpred_comp_modifiers RPredCompFuns.compfuns, + compile_preds = compile_preds rpred_comp_modifiers RandomPredCompFuns.compfuns, prove = prove_by_skip, are_not_defined = fn thy => forall (null o rpred_modes_of thy), qname = "rpred_equation"} @@ -2420,7 +2402,7 @@ fun eval thy (options as (depth_limit, random)) t_compr = let - val compfuns = if random then RPredCompFuns.compfuns else PredicateCompFuns.compfuns + val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns val t = analyze_compr thy compfuns options t_compr; val T = dest_predT compfuns (fastype_of t); val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t; @@ -2467,12 +2449,10 @@ val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; -val _ = List.app OuterKeyword.keyword ["depth_limit", "random"] - val options = let - val depth_limit = Scan.optional (P.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE - val random = Scan.optional (P.$$$ "random" >> K true) false + val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE + val random = Scan.optional (Args.$$$ "random" >> K true) false in Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false) end diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,218 @@ +(* Author: Lukas Bulwahn, TU Muenchen + +Book-keeping datastructure for the predicate compiler + +*) +signature PREDICATE_COMPILE_DATA = +sig + type specification_table; + val make_const_spec_table : theory -> specification_table + val get_specification : specification_table -> string -> thm list + val obtain_specification_graph : Predicate_Compile_Aux.options -> theory -> + specification_table -> string -> thm list Graph.T + val normalize_equation : theory -> thm -> thm +end; + +structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = +struct + +open Predicate_Compile_Aux; + +structure Data = TheoryDataFun +( + type T = + {const_spec_table : thm list Symtab.table}; + val empty = + {const_spec_table = Symtab.empty}; + val copy = I; + val extend = I; + fun merge _ + ({const_spec_table = const_spec_table1}, + {const_spec_table = const_spec_table2}) = + {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)} +); + +fun mk_data c = {const_spec_table = c} +fun map_data f {const_spec_table = c} = mk_data (f c) + +type specification_table = thm list Symtab.table + +fun defining_const_of_introrule_term t = + let + val _ $ u = Logic.strip_imp_concl t + val (pred, all_args) = strip_comb u + in case pred of + Const (c, T) => c + | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) + end + +val defining_const_of_introrule = defining_const_of_introrule_term o prop_of + +(*TODO*) +fun is_introlike_term t = true + +val is_introlike = is_introlike_term o prop_of + +fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) = + (case strip_comb u of + (Const (c, T), args) => + if (length (binder_types T) = length args) then + true + else + raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t]) + | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t])) + | check_equation_format_term t = + raise TERM ("check_equation_format_term failed: Not an equation", [t]) + +val check_equation_format = check_equation_format_term o prop_of + +fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) = + (case fst (strip_comb u) of + Const (c, _) => c + | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t])) + | defining_const_of_equation_term t = + raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) + +val defining_const_of_equation = defining_const_of_equation_term o prop_of + +(* Normalizing equations *) + +fun mk_meta_equation th = + case prop_of th of + Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection} + | _ => th + +val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} + +fun full_fun_cong_expand th = + let + val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th))) + val i = length (binder_types (fastype_of f)) - length args + in funpow i (fn th => th RS meta_fun_cong) th end; + +fun declare_names s xs ctxt = + let + val res = Name.names ctxt s xs + in (res, fold Name.declare (map fst res) ctxt) end + +fun split_all_pairs thy th = + let + val ctxt = ProofContext.init thy + val ((_, [th']), ctxt') = Variable.import true [th] ctxt + val t = prop_of th' + val frees = Term.add_frees t [] + val freenames = Term.add_free_names t [] + val nctxt = Name.make_context freenames + fun mk_tuple_rewrites (x, T) nctxt = + let + val Ts = HOLogic.flatten_tupleT T + val (xTs, nctxt') = declare_names x Ts nctxt + val paths = HOLogic.flat_tupleT_paths T + in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end + val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt + val t' = Pattern.rewrite_term thy rewr [] t + val tac = Skip_Proof.cheat_tac thy + val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac) + val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th'' + in + th''' + end; + +fun normalize_equation thy th = + mk_meta_equation th + |> Predicate_Compile_Set.unfold_set_notation + |> full_fun_cong_expand + |> split_all_pairs thy + |> tap check_equation_format + +fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite +((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th + +fun store_thm_in_table ignore_consts thy th= + let + val th = th + |> inline_equations thy + |> Predicate_Compile_Set.unfold_set_notation + |> AxClass.unoverload thy + val (const, th) = + if is_equationlike th then + let + val eq = normalize_equation thy th + in + (defining_const_of_equation eq, eq) + end + else if (is_introlike th) then (defining_const_of_introrule th, th) + else error "store_thm: unexpected definition format" + in + if not (member (op =) ignore_consts const) then + Symtab.cons_list (const, th) + else I + end + +fun make_const_spec_table thy = + let + fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy))) + val table = Symtab.empty + |> store [] Predicate_Compile_Alternative_Defs.get + val ignore_consts = Symtab.keys table + in + table + |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get + |> store ignore_consts Nitpick_Simps.get + |> store ignore_consts Nitpick_Intros.get + end + +fun get_specification table constname = + case Symtab.lookup table constname of + SOME thms => thms + | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed") + +val logic_operator_names = + [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, + @{const_name "op &"}] + +val special_cases = member (op =) [ + @{const_name "False"}, + @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat}, + @{const_name Nat.one_nat_inst.one_nat}, +@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"}, +@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus}, +@{const_name Nat.ord_nat_inst.less_eq_nat}, +@{const_name number_nat_inst.number_of_nat}, + @{const_name Int.Bit0}, + @{const_name Int.Bit1}, + @{const_name Int.Pls}, +@{const_name "Int.zero_int_inst.zero_int"}, +@{const_name "List.filter"}] + +fun case_consts thy s = is_some (Datatype.info_of_case thy s) + +fun print_specification options thy constname specs = + if show_intermediate_results options then + tracing ("Specification of " ^ constname ^ ":\n" ^ + cat_lines (map (Display.string_of_thm_global thy) specs)) + else () + +fun obtain_specification_graph options thy table constname = + let + fun is_nondefining_constname c = member (op =) logic_operator_names c + val is_defining_constname = member (op =) (Symtab.keys table) + fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c) + fun defiants_of specs = + fold (Term.add_const_names o prop_of) specs [] + |> filter is_defining_constname + |> filter_out is_nondefining_constname + |> filter_out has_code_pred_intros + |> filter_out (case_consts thy) + |> filter_out special_cases + fun extend constname = + let + val specs = get_specification table constname + val _ = print_specification options thy constname specs + in (specs, defiants_of specs) end; + in + Graph.extend extend constname Graph.empty + end; + + +end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,437 @@ +(* Author: Lukas Bulwahn, TU Muenchen + +Preprocessing functions to predicates +*) + +signature PREDICATE_COMPILE_FUN = +sig +val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory + val rewrite_intro : theory -> thm -> thm list + val setup_oracle : theory -> theory + val pred_of_function : theory -> string -> string option +end; + +structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = +struct + + +(* Oracle for preprocessing *) + +val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE; + +fun the_oracle () = + case !oracle of + NONE => error "Oracle is not setup" + | SOME (_, oracle) => oracle + +val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #-> + (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end) + + +fun is_funtype (Type ("fun", [_, _])) = true + | is_funtype _ = false; + +fun is_Type (Type _) = true + | is_Type _ = false + +(* returns true if t is an application of an datatype constructor *) +(* which then consequently would be splitted *) +(* else false *) +(* +fun is_constructor thy t = + if (is_Type (fastype_of t)) then + (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of + NONE => false + | SOME info => (let + val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) + val (c, _) = strip_comb t + in (case c of + Const (name, _) => name mem_string constr_consts + | _ => false) end)) + else false +*) + +(* must be exported in code.ML *) +fun is_constr thy = is_some o Code.get_datatype_of_constr thy; + +(* Table from constant name (string) to term of inductive predicate *) +structure Pred_Compile_Preproc = TheoryDataFun +( + type T = string Symtab.table; + val empty = Symtab.empty; + val copy = I; + val extend = I; + fun merge _ = Symtab.merge (op =); +) + +fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name + +fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) + + +fun transform_ho_typ (T as Type ("fun", _)) = + let + val (Ts, T') = strip_type T + in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end +| transform_ho_typ t = t + +fun transform_ho_arg arg = + case (fastype_of arg) of + (T as Type ("fun", _)) => + (case arg of + Free (name, _) => Free (name, transform_ho_typ T) + | _ => error "I am surprised") +| _ => arg + +fun pred_type T = + let + val (Ts, T') = strip_type T + val Ts' = map transform_ho_typ Ts + in + (Ts' @ [T']) ---> HOLogic.boolT + end; + +(* FIXME: create new predicate name -- does not avoid nameclashing *) +fun pred_of f = + let + val (name, T) = dest_Const f + in + if (body_type T = @{typ bool}) then + (Free (Long_Name.base_name name ^ "P", T)) + else + (Free (Long_Name.base_name name ^ "P", pred_type T)) + end + +fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t + | mk_param thy lookup_pred t = + let + val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t)) + in if Predicate_Compile_Aux.is_predT (fastype_of t) then + t + else + let + val (vs, body) = strip_abs t + val names = Term.add_free_names body [] + val vs_names = Name.variant_list names (map fst vs) + val vs' = map2 (curry Free) vs_names (map snd vs) + val body' = subst_bounds (rev vs', body) + val (f, args) = strip_comb body' + val resname = Name.variant (vs_names @ names) "res" + val resvar = Free (resname, body_type (fastype_of body')) + (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param" + val pred_body = list_comb (P, args @ [resvar]) + *) + val pred_body = HOLogic.mk_eq (body', resvar) + val param = fold_rev lambda (vs' @ [resvar]) pred_body + in param end + end +(* creates the list of premises for every intro rule *) +(* theory -> term -> (string list, term list list) *) + +fun dest_code_eqn eqn = let + val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn)) + val (func, args) = strip_comb lhs +in ((func, args), rhs) end; + +fun string_of_typ T = Syntax.string_of_typ_global @{theory} T + +fun string_of_term t = + case t of + Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")" + | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")" + | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")" + | Bound i => "Bound " ^ string_of_int i + | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")" + | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")" + +fun ind_package_get_nparams thy name = + case try (Inductive.the_inductive (ProofContext.init thy)) name of + SOME (_, result) => length (Inductive.params_of (#raw_induct result)) + | NONE => error ("No such predicate: " ^ quote name) + +(* TODO: does not work with higher order functions yet *) +fun mk_rewr_eq (func, pred) = + let + val (argTs, resT) = (strip_type (fastype_of func)) + val nctxt = + Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) []) + val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt + val ([resname], nctxt'') = Name.variants ["r"] nctxt' + val args = map Free (argnames ~~ argTs) + val res = Free (resname, resT) + in Logic.mk_equals + (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res])) + end; + +fun has_split_rule_cname @{const_name "nat_case"} = true + | has_split_rule_cname @{const_name "list_case"} = true + | has_split_rule_cname _ = false + +fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true + | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true + | has_split_rule_term thy _ = false + +fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true + | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true + | has_split_rule_term' thy c = has_split_rule_term thy c + +fun prepare_split_thm ctxt split_thm = + (split_thm RS @{thm iffD2}) + |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]}, + @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] + +fun find_split_thm thy (Const (name, typ)) = + let + fun split_name str = + case first_field "." str + of (SOME (field, rest)) => field :: split_name rest + | NONE => [str] + val splitted_name = split_name name + in + if length splitted_name > 0 andalso + String.isSuffix "_case" (List.last splitted_name) + then + (List.take (splitted_name, length splitted_name - 1)) @ ["split"] + |> space_implode "." + |> PureThy.get_thm thy + |> SOME + handle ERROR msg => NONE + else NONE + end + | find_split_thm _ _ = NONE + +fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if} + | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *) + | find_split_thm' thy c = find_split_thm thy c + +fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) + +fun folds_map f xs y = + let + fun folds_map' acc [] y = [(rev acc, y)] + | folds_map' acc (x :: xs) y = + maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y) + in + folds_map' [] xs y + end; + +fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) = + let + fun mk_prems' (t as Const (name, T)) (names, prems) = + if is_constr thy name orelse (is_none (try lookup_pred t)) then + [(t, (names, prems))] + else [(lookup_pred t, (names, prems))] + | mk_prems' (t as Free (f, T)) (names, prems) = + [(lookup_pred t, (names, prems))] + | mk_prems' (t as Abs _) (names, prems) = + if Predicate_Compile_Aux.is_predT (fastype_of t) then + [(t, (names, prems))] else error "mk_prems': Abs " + (* mk_param *) + | mk_prems' t (names, prems) = + if Predicate_Compile_Aux.is_constrt thy t then + [(t, (names, prems))] + else + if has_split_rule_term' thy (fst (strip_comb t)) then + let + val (f, args) = strip_comb t + val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f)) + (* TODO: contextify things - this line is to unvarify the split_thm *) + (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*) + val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm) + val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) + val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty) + val (_, split_args) = strip_comb split_t + val match = split_args ~~ args + fun mk_prems_of_assm assm = + let + val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) + val var_names = Name.variant_list names (map fst vTs) + val vars = map Free (var_names ~~ (map snd vTs)) + val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) + val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) + in + mk_prems' inner_t (var_names @ names, prems' @ prems) + end + in + maps mk_prems_of_assm assms + end + else + let + val (f, args) = strip_comb t + (* TODO: special procedure for higher-order functions: split arguments in + simple types and function types *) + val resname = Name.variant names "res" + val resvar = Free (resname, body_type (fastype_of t)) + val names' = resname :: names + fun mk_prems'' (t as Const (c, _)) = + if is_constr thy c orelse (is_none (try lookup_pred t)) then + folds_map mk_prems' args (names', prems) |> + map + (fn (argvs, (names'', prems')) => + let + val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs))) + in (names'', prem :: prems') end) + else + let + val pred = lookup_pred t + val nparams = get_nparams pred + val (params, args) = chop nparams args + val params' = map (mk_param thy lookup_pred) params + in + folds_map mk_prems' args (names', prems) + |> map (fn (argvs, (names'', prems')) => + let + val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar])) + in (names'', prem :: prems') end) + end + | mk_prems'' (t as Free (_, _)) = + let + (* higher order argument call *) + val pred = lookup_pred t + in + folds_map mk_prems' args (resname :: names, prems) + |> map (fn (argvs, (names', prems')) => + let + val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar])) + in (names', prem :: prems') end) + end + | mk_prems'' t = + error ("Invalid term: " ^ Syntax.string_of_term_global thy t) + in + map (pair resvar) (mk_prems'' f) + end + in + mk_prems' t (names, prems) + end; + +(* assumption: mutual recursive predicates all have the same parameters. *) +fun define_predicates specs thy = + if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then + ([], thy) + else + let + val consts = map fst specs + val eqns = maps snd specs + (*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*) + (* create prednames *) + val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list + val argss' = map (map transform_ho_arg) argss + val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss')) + val preds = map pred_of funs + val prednames = map (fst o dest_Free) preds + val funnames = map (fst o dest_Const) funs + val fun_pred_names = (funnames ~~ prednames) + (* mapping from term (Free or Const) to term *) + fun lookup_pred (Const (name, T)) = + (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of + SOME c => Const (c, pred_type T) + | NONE => + (case AList.lookup op = fun_pred_names name of + SOME f => Free (f, pred_type T) + | NONE => Const (name, T))) + | lookup_pred (Free (name, T)) = + if member op = (map fst pnames) name then + Free (name, transform_ho_typ T) + else + Free (name, T) + | lookup_pred t = + error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t) + + (* mapping from term (predicate term, not function term!) to int *) + fun get_nparams (Const (name, _)) = + the_default 0 (try (ind_package_get_nparams thy) name) + | get_nparams (Free (name, _)) = + (if member op = prednames name then + length pnames + else 0) + | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) + + (* create intro rules *) + + fun mk_intros ((func, pred), (args, rhs)) = + if (body_type (fastype_of func) = @{typ bool}) then + (*TODO: preprocess predicate definition of rhs *) + [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))] + else + let + val names = Term.add_free_names rhs [] + in mk_prems thy (lookup_pred, get_nparams) rhs (names, []) + |> map (fn (resultt, (names', prems)) => + Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) + end + fun mk_rewr_thm (func, pred) = @{thm refl} + in + case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of + NONE => ([], thy) + | SOME intr_ts => + if is_some (try (map (cterm_of thy)) intr_ts) then + let + val (ind_result, thy') = + Inductive.add_inductive_global (serial ()) + {quiet_mode = false, verbose = false, kind = Thm.internalK, + alt_name = Binding.empty, coind = false, no_elim = false, + no_ind = false, skip_mono = false, fork_mono = false} + (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) + pnames + (map (fn x => (Attrib.empty_binding, x)) intr_ts) + [] thy + val prednames = map (fst o dest_Const) (#preds ind_result) + (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *) + (* add constants to my table *) + val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames + val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' + in + (specs, thy'') + end + else + let + val _ = tracing "Introduction rules of function_predicate are not welltyped" + in ([], thy) end + end + +(* preprocessing intro rules - uses oracle *) + +(* theory -> thm -> thm *) +fun rewrite_intro thy intro = + let + fun lookup_pred (Const (name, T)) = + (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of + SOME c => Const (c, pred_type T) + | NONE => error ("Function " ^ name ^ " is not inductified")) + | lookup_pred (Free (name, T)) = Free (name, T) + | lookup_pred _ = error "lookup function is not defined!" + + fun get_nparams (Const (name, _)) = + the_default 0 (try (ind_package_get_nparams thy) name) + | get_nparams (Free _) = 0 + | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) + + val intro_t = (Logic.unvarify o prop_of) intro + val (prems, concl) = Logic.strip_horn intro_t + val frees = map fst (Term.add_frees intro_t []) + fun rewrite prem names = + let + val t = (HOLogic.dest_Trueprop prem) + val (lit, mk_lit) = case try HOLogic.dest_not t of + SOME t => (t, HOLogic.mk_not) + | NONE => (t, I) + val (P, args) = (strip_comb lit) + in + folds_map ( + fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)]) + else mk_prems thy (lookup_pred, get_nparams) t) args (names, []) + |> map (fn (resargs, (names', prems')) => + let + val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs))) + in (prem'::prems', names') end) + end + val intro_ts' = folds_map rewrite prems frees + |> maps (fn (prems', frees') => + rewrite concl frees' + |> map (fn (concl'::conclprems, _) => + Logic.list_implies ((flat prems') @ conclprems, concl'))) + in + map (Drule.standard o the_oracle () o cterm_of thy) intro_ts' + end; + +end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,189 @@ +(* Author: Lukas Bulwahn, TU Muenchen + +Preprocessing definitions of predicates to introduction rules +*) + +signature PREDICATE_COMPILE_PRED = +sig + (* preprocesses an equation to a set of intro rules; defines new constants *) + (* + val preprocess_pred_equation : thm -> theory -> thm list * theory + *) + val preprocess : string -> theory -> (thm list list * theory) + (* output is the term list of clauses of an unknown predicate *) + val preprocess_term : term -> theory -> (term list * theory) + + (*val rewrite : thm -> thm*) + +end; +(* : PREDICATE_COMPILE_PREPROC_PRED *) +structure Predicate_Compile_Pred = +struct + +open Predicate_Compile_Aux + +fun is_compound ((Const ("Not", _)) $ t) = + error "is_compound: Negation should not occur; preprocessing is defect" + | is_compound ((Const ("Ex", _)) $ _) = true + | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true + | is_compound ((Const ("op &", _)) $ _ $ _) = + error "is_compound: Conjunction should not occur; preprocessing is defect" + | is_compound _ = false + +fun flatten constname atom (defs, thy) = + if is_compound atom then + let + val constname = Name.variant (map (Long_Name.base_name o fst) defs) + ((Long_Name.base_name constname) ^ "_aux") + val full_constname = Sign.full_bname thy constname + val (params, args) = List.partition (is_predT o fastype_of) + (map Free (Term.add_frees atom [])) + val constT = map fastype_of (params @ args) ---> HOLogic.boolT + val lhs = list_comb (Const (full_constname, constT), params @ args) + val def = Logic.mk_equals (lhs, atom) + val ([definition], thy') = thy + |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] + |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] + in + (lhs, ((full_constname, [definition]) :: defs, thy')) + end + else + (atom, (defs, thy)) + +fun flatten_intros constname intros thy = + let + val ctxt = ProofContext.init thy + val ((_, intros), ctxt') = Variable.import true intros ctxt + val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms) + (flatten constname) (map prop_of intros) ([], thy) + val tac = fn _ => Skip_Proof.cheat_tac thy' + val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros' + |> Variable.export ctxt' ctxt + in + (intros'', (local_defs, thy')) + end + +(* TODO: same function occurs in inductive package *) +fun select_disj 1 1 = [] + | select_disj _ 1 = [rtac @{thm disjI1}] + | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1)); + +fun introrulify thy ths = + let + val ctxt = ProofContext.init thy + val ((_, ths'), ctxt') = Variable.import true ths ctxt + fun introrulify' th = + let + val (lhs, rhs) = Logic.dest_equals (prop_of th) + val frees = Term.add_free_names rhs [] + val disjuncts = HOLogic.dest_disj rhs + val nctxt = Name.make_context frees + fun mk_introrule t = + let + val ((ps, t'), nctxt') = focus_ex t nctxt + val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t') + in + (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs)) + end + val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o + Logic.dest_implies o prop_of) @{thm exI} + fun prove_introrule (index, (ps, introrule)) = + let + val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1 + THEN EVERY1 (select_disj (length disjuncts) (index + 1)) + THEN (EVERY (map (fn y => + rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps)) + THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1) + THEN TRY (atac 1) + in + Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac) + end + in + map_index prove_introrule (map mk_introrule disjuncts) + end + in maps introrulify' ths' |> Variable.export ctxt' ctxt end + +val rewrite = + Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}]) + #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) + #> Conv.fconv_rule nnf_conv + #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}]) + +val rewrite_intros = + Simplifier.simplify (HOL_basic_ss addsimps @{thms HOL.simp_thms(9)}) + +fun preprocess (constname, specs) thy = + let + val ctxt = ProofContext.init thy + val intros = + if forall is_pred_equation specs then + introrulify thy (map rewrite specs) + else if forall (is_intro constname) specs then + map rewrite_intros specs + else + error ("unexpected specification for constant " ^ quote constname ^ ":\n" + ^ commas (map (quote o Display.string_of_thm_global thy) specs)) + val (intros', (local_defs, thy')) = flatten_intros constname intros thy + val (intross, thy'') = fold_map preprocess local_defs thy' + in + ((constname, intros') :: flat intross,thy'') + end; + +fun preprocess_term t thy = error "preprocess_pred_term: to implement" + +fun is_Abs (Abs _) = true + | is_Abs _ = false + +fun flat_higher_order_arguments (intross, thy) = + let + fun process constname atom (new_defs, thy) = + let + val (pred, args) = strip_comb atom + val abs_args = filter is_Abs args + fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = + let + val _ = tracing ("Introduce new constant for " ^ + Syntax.string_of_term_global thy abs_arg) + val vars = map Var (Term.add_vars abs_arg []) + val abs_arg' = Logic.unvarify abs_arg + val frees = map Free (Term.add_frees abs_arg' []) + val constname = Name.variant (map (Long_Name.base_name o fst) new_defs) + ((Long_Name.base_name constname) ^ "_hoaux") + val full_constname = Sign.full_bname thy constname + val constT = map fastype_of frees ---> (fastype_of abs_arg') + val const = Const (full_constname, constT) + val lhs = list_comb (const, frees) + val def = Logic.mk_equals (lhs, abs_arg') + val _ = tracing (Syntax.string_of_term_global thy def) + val ([definition], thy') = thy + |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] + |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] + in + (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy')) + end + | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy)) + val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy) + in + (list_comb (pred, args'), (new_defs', thy')) + end + fun flat_intro intro (new_defs, thy) = + let + val constname = fst (dest_Const (fst (strip_comb + (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro)))))) + val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy) + val th = Skip_Proof.make_thm thy intro_ts + in + (th, (new_defs, thy)) + end + fun fold_map_spec f [] s = ([], s) + | fold_map_spec f ((c, ths) :: specs) s = + let + val (ths', s') = f ths s + val (specs', s'') = fold_map_spec f specs s' + in ((c, ths') :: specs', s'') end + val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy) + in + (intross', (new_defs, thy')) + end + +end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,112 @@ +(* Author: Lukas Bulwahn, TU Muenchen + +A quickcheck generator based on the predicate compiler +*) + +signature PREDICATE_COMPILE_QUICKCHECK = +sig + val quickcheck : Proof.context -> term -> int -> term list option + val test_ref : + ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref +end; + +structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = +struct + +open Predicate_Compile_Aux; + +val test_ref = + Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) + +val target = "Quickcheck" + +val options = Options { + expected_modes = NONE, + show_steps = true, + show_intermediate_results = true, + show_proof_trace = false, + show_modes = true, + show_mode_inference = false, + show_compilation = true, + skip_proof = false, + + inductify = false, + rpred = false, + depth_limited = false +} + +fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs +val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns) +val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns) +val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.randompred_compfuns) +val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.randompred_compfuns) + +fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t) + | mk_split_lambda [x] t = lambda x t + | mk_split_lambda xs t = + let + fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) + | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) + in + mk_split_lambda' xs t + end; + +fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B + | strip_imp_prems _ = []; + +fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B + | strip_imp_concl A = A : term; + +fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); + +fun quickcheck ctxt t = + let + val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) + val ctxt' = ProofContext.theory (Context.copy_thy) ctxt + val thy = (ProofContext.theory_of ctxt') + val (vs, t') = strip_abs t + val vs' = Variable.variant_frees ctxt' [] vs + val t'' = subst_bounds (map Free (rev vs'), t') + val (prems, concl) = strip_horn t'' + val constname = "pred_compile_quickcheck" + val full_constname = Sign.full_bname thy constname + val constT = map snd vs' ---> @{typ bool} + val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy + val t = Logic.list_implies + (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), + HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) + val tac = fn _ => Skip_Proof.cheat_tac thy' + val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac + val _ = tracing (Display.string_of_thm ctxt' intro) + val thy'' = thy' + |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) + |> Predicate_Compile.preprocess options full_constname + |> Predicate_Compile_Core.add_equations options [full_constname] + (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) + |> Predicate_Compile_Core.add_quickcheck_equations options [full_constname] + val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname + val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname + val prog = + if member (op =) modes ([], []) then + let + val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], []) + val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) + in Const (name, T) $ Bound 0 end + (*else if member (op =) depth_limited_modes ([], []) then + let + val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) + val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) + in lift_pred (Const (name, T) $ Bound 0) end*) + else error "Predicate Compile Quickcheck failed" + val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog, + mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} + (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) + val _ = tracing (Syntax.string_of_term ctxt' qc_term) + val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) + (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) + thy'' qc_term [] + in + ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield)) + end + +end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_set.ML Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,52 @@ +(* Author: Lukas Bulwahn, TU Muenchen + +Preprocessing sets to predicates +*) + +signature PREDICATE_COMPILE_SET = +sig +(* + val preprocess_intro : thm -> theory -> thm * theory + val preprocess_clause : term -> theory -> term * theory +*) + val unfold_set_notation : thm -> thm; +end; + +structure Predicate_Compile_Set : PREDICATE_COMPILE_SET = +struct +(*FIXME: unfolding Ball in pretty adhoc here *) +val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, +@{thm Ball_def}, @{thm Bex_def}] + +val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas + +(* +fun find_set_theorems ctxt cname = + let + val _ = cname +*) + +(* +fun preprocess_term t ctxt = + case t of + Const ("op :", _) $ x $ A => + case strip_comb A of + (Const (cname, T), params) => + let + val _ = find_set_theorems + in + (t, ctxt) + end + | _ => (t, ctxt) + | _ => (t, ctxt) +*) +(* +fun preprocess_intro th thy = + let + val cnames = find_heads_of_prems + val set_cname = filter (has_set_definition + val _ = define_preds + val _ = prep_pred_def + in +*) +end; diff -r f93390060bbe -r f8d43d5215c2 src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Tue Oct 27 14:40:24 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -theory Predicate_Compile -imports Complex_Main RPred -uses - "../Tools/Predicate_Compile/pred_compile_aux.ML" - "../Tools/Predicate_Compile/predicate_compile_core.ML" - "../Tools/Predicate_Compile/pred_compile_set.ML" - "../Tools/Predicate_Compile/pred_compile_data.ML" - "../Tools/Predicate_Compile/pred_compile_fun.ML" - "../Tools/Predicate_Compile/pred_compile_pred.ML" - "../Tools/Predicate_Compile/predicate_compile.ML" - "../Tools/Predicate_Compile/pred_compile_quickcheck.ML" -begin - -setup {* Predicate_Compile.setup *} -setup {* Quickcheck.add_generator ("pred_compile", Predicate_Compile_Quickcheck.quickcheck) *} - -end \ No newline at end of file diff -r f93390060bbe -r f8d43d5215c2 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Tue Oct 27 14:40:24 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Tue Oct 27 16:01:38 2009 +0100 @@ -1,5 +1,5 @@ theory Predicate_Compile_Alternative_Defs -imports Predicate_Compile +imports Main begin section {* Set operations *} diff -r f93390060bbe -r f8d43d5215c2 src/HOL/ex/Predicate_Compile_Quickcheck.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,12 @@ +(* Author: Lukas Bulwahn, TU Muenchen *) + +header {* A Prototype of Quickcheck based on the Predicate Compiler *} + +theory Predicate_Compile_Quickcheck +imports Main +uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" +begin + +setup {* Quickcheck.add_generator ("predicate_compile", Predicate_Compile_Quickcheck.quickcheck) *} + +end \ No newline at end of file diff -r f93390060bbe -r f8d43d5215c2 src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Oct 27 16:01:38 2009 +0100 @@ -0,0 +1,118 @@ +theory Predicate_Compile_Quickcheck_ex +imports Predicate_Compile_Quickcheck + Predicate_Compile_Alternative_Defs +begin + +section {* Sets *} + + +section {* Context Free Grammar *} + +datatype alphabet = a | b + +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where + "[] \ S\<^isub>1" +| "w \ A\<^isub>1 \ b # w \ S\<^isub>1" +| "w \ B\<^isub>1 \ a # w \ S\<^isub>1" +| "w \ S\<^isub>1 \ a # w \ A\<^isub>1" +| "w \ S\<^isub>1 \ b # w \ S\<^isub>1" +| "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" + +theorem S\<^isub>1_sound: +"w \ S\<^isub>1p \ length [x \ w. x = a] = length [x \ w. x = b]" +(*quickcheck[generator=predicate_compile, size=15]*) +oops + + +inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where + "[] \ S\<^isub>2" +| "w \ A\<^isub>2 \ b # w \ S\<^isub>2" +| "w \ B\<^isub>2 \ a # w \ S\<^isub>2" +| "w \ S\<^isub>2 \ a # w \ A\<^isub>2" +| "w \ S\<^isub>2 \ b # w \ B\<^isub>2" +| "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" + +code_pred [inductify, rpred] S\<^isub>2 . +thm S\<^isub>2.rpred_equation +thm A\<^isub>2.rpred_equation +thm B\<^isub>2.rpred_equation + +values [random] 10 "{x. S\<^isub>2 x}" + +lemma "w \ S\<^isub>2 ==> w \ [] ==> w \ [b, a] ==> w \ {}" +quickcheck[generator=predicate_compile] +oops + +lemma "[x <- w. x = a] = []" +quickcheck[generator=predicate_compile] +oops + + +lemma "length ([x \ w. x = a]) = (0::nat)" +(*quickcheck[generator=predicate_compile]*) +oops + + + +lemma +"w \ S\<^isub>2 ==> length [x \ w. x = a] < Suc (Suc 0)" +(*quickcheck[generator=predicate_compile]*) +oops + + +theorem S\<^isub>2_sound: +"w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" +(*quickcheck[generator=predicate_compile, size=15, iterations=100]*) +oops + +inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where + "[] \ S\<^isub>3" +| "w \ A\<^isub>3 \ b # w \ S\<^isub>3" +| "w \ B\<^isub>3 \ a # w \ S\<^isub>3" +| "w \ S\<^isub>3 \ a # w \ A\<^isub>3" +| "w \ S\<^isub>3 \ b # w \ B\<^isub>3" +| "\v \ B\<^isub>3; w \ B\<^isub>3\ \ a # v @ w \ B\<^isub>3" + +code_pred [inductify] S\<^isub>3 . +thm S\<^isub>3.equation + +values 10 "{x. S\<^isub>3 x}" + +lemma S\<^isub>3_sound: +"w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" +(*quickcheck[generator=predicate_compile, size=10, iterations=1]*) +oops + + +lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" +(*quickcheck[size=10, generator = pred_compile]*) +oops + +theorem S\<^isub>3_complete: +"length [x \ w. x = a] = length [x \ w. b = x] \ w \ S\<^isub>3" +(*quickcheck[generator=SML]*) +(*quickcheck[generator=predicate_compile, size=10, iterations=100]*) +oops + + +inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where + "[] \ S\<^isub>4" +| "w \ A\<^isub>4 \ b # w \ S\<^isub>4" +| "w \ B\<^isub>4 \ a # w \ S\<^isub>4" +| "w \ S\<^isub>4 \ a # w \ A\<^isub>4" +| "\v \ A\<^isub>4; w \ A\<^isub>4\ \ b # v @ w \ A\<^isub>4" +| "w \ S\<^isub>4 \ b # w \ B\<^isub>4" +| "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" + +theorem S\<^isub>4_sound: +"w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" +(*quickcheck[generator = predicate_compile, size=2, iterations=1]*) +oops + +theorem S\<^isub>4_complete: +"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" +(*quickcheck[generator = pred_compile, size=5, iterations=1]*) +oops + + +end \ No newline at end of file diff -r f93390060bbe -r f8d43d5215c2 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Tue Oct 27 14:40:24 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Oct 27 16:01:38 2009 +0100 @@ -2,6 +2,99 @@ imports Main Predicate_Compile_Alternative_Defs begin +subsection {* Basic predicates *} + +inductive False' :: "bool" + +code_pred (mode: []) False' . +code_pred [depth_limited] False' . +code_pred [rpred] False' . + +inductive EmptySet :: "'a \ bool" + +code_pred (mode: [], [1]) EmptySet . + +definition EmptySet' :: "'a \ bool" +where "EmptySet' = {}" + +code_pred (mode: [], [1]) [inductify, show_intermediate_results] EmptySet' . + +inductive EmptyRel :: "'a \ 'b \ bool" + +code_pred (mode: [], [1], [2], [1, 2]) EmptyRel . + +inductive EmptyClosure :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" +for r :: "'a \ 'a \ bool" + +code_pred (mode: [], [1], [2], [1, 2])EmptyClosure . +thm EmptyClosure.equation +(* TODO: inductive package is broken! +inductive False'' :: "bool" +where + "False \ False''" + +code_pred (mode: []) False'' . + +inductive EmptySet'' :: "'a \ bool" +where + "False \ EmptySet'' x" + +code_pred (mode: [1]) EmptySet'' . +code_pred (mode: [], [1]) [inductify] EmptySet'' . +*) +inductive True' :: "bool" +where + "True \ True'" + +code_pred (mode: []) True' . + +consts a' :: 'a + +inductive Fact :: "'a \ 'a \ bool" +where +"Fact a' a'" + +code_pred (mode: [], [1], [2], [1, 2]) Fact . + +inductive zerozero :: "nat * nat => bool" +where + "zerozero (0, 0)" + +code_pred zerozero . +code_pred [rpred, show_compilation] zerozero . + +subsection {* Preprocessor Inlining *} + +definition "equals == (op =)" + +inductive zerozero' where + "equals (x, y) (0, 0) ==> zerozero' (x, y)" + +code_pred (mode: [1]) zerozero' . + +lemma zerozero'_eq: "zerozero' == zerozero" +proof - + have "zerozero' = zerozero" + apply (auto simp add: mem_def) + apply (cases rule: zerozero'.cases) + apply (auto simp add: equals_def intro: zerozero.intros) + apply (cases rule: zerozero.cases) + apply (auto simp add: equals_def intro: zerozero'.intros) + done + from this show "zerozero' == zerozero" by auto +qed + +declare zerozero'_eq [code_pred_inline] + +definition "zerozero'' x == zerozero' x" + +text {* if preprocessing fails, zerozero'' will not have all modes. *} +ML {* Predicate_Compile_Inline_Defs.get @{context} *} +(* TODO: *) +code_pred (mode: [1]) [inductify, show_intermediate_results] zerozero'' . + +subsection {* even predicate *} + inductive even :: "nat \ bool" and odd :: "nat \ bool" where "even 0" | "even n \ odd (Suc n)" @@ -26,7 +119,6 @@ values [depth_limit = 7] "{x. even 6}" values [depth_limit = 2] "{x. odd 7}" values [depth_limit = 8] "{x. odd 7}" - values [depth_limit = 7] 10 "{n. even n}" definition odd' where "odd' x == \ even x" @@ -39,6 +131,14 @@ values [depth_limit = 2] "{x. odd' 7}" values [depth_limit = 9] "{x. odd' 7}" +inductive is_even :: "nat \ bool" +where + "n mod 2 = 0 \ is_even n" + +code_pred is_even . + +subsection {* append predicate *} + inductive append :: "'a list \ 'a list \ 'a list \ bool" where "append [] xs xs" | "append xs ys zs \ append (x # xs) ys (x # zs)" @@ -60,7 +160,7 @@ value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (append_3 ([]::int list))" -subsection {* Tricky case with alternative rules *} +text {* tricky case with alternative rules *} inductive append2 where @@ -78,15 +178,6 @@ from append2.cases[OF append2(1)] append2(2-3) show thesis by blast qed -subsection {* Tricky cases with tuples *} - -inductive zerozero :: "nat * nat => bool" -where - "zerozero (0, 0)" - -code_pred zerozero . -code_pred [rpred] zerozero . - inductive tupled_append :: "'a list \ 'a list \ 'a list \ bool" where "tupled_append ([], xs, xs)" @@ -127,6 +218,8 @@ code_pred [inductify] tupled_append''' . thm tupled_append'''.equation +subsection {* map_ofP predicate *} + inductive map_ofP :: "('a \ 'b) list \ 'a \ 'b \ bool" where "map_ofP ((a, b)#xs) a b" @@ -135,6 +228,8 @@ code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP . thm map_ofP.equation +subsection {* filter predicate *} + inductive filter1 for P where @@ -168,7 +263,7 @@ code_pred filter3 . code_pred [depth_limited] filter3 . thm filter3.depth_limited_equation -(*code_pred [rpred] filter3 .*) + inductive filter4 where "List.filter P xs = ys ==> filter4 P xs ys" @@ -177,7 +272,7 @@ code_pred [depth_limited] filter4 . code_pred [rpred] filter4 . -section {* reverse *} +subsection {* reverse predicate *} inductive rev where "rev [] []" @@ -196,6 +291,8 @@ code_pred tupled_rev . thm tupled_rev.equation +subsection {* partition predicate *} + inductive partition :: "('a \ bool) \ 'a list \ 'a list \ 'a list \ bool" for f where "partition f [] [] []" @@ -206,6 +303,11 @@ code_pred [depth_limited] partition . code_pred [rpred] partition . +values 10 "{(ys, zs). partition is_even + [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" +values 10 "{zs. partition is_even zs [0, 2] [3, 5]}" +values 10 "{zs. partition is_even zs [0, 7] [3, 5]}" + inductive tupled_partition :: "('a \ bool) \ ('a list \ 'a list \ 'a list) \ bool" for f where "tupled_partition f ([], [], [])" @@ -216,23 +318,13 @@ thm tupled_partition.equation - -inductive is_even :: "nat \ bool" -where - "n mod 2 = 0 \ is_even n" - -code_pred is_even . - -values 10 "{(ys, zs). partition is_even - [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" -values 10 "{zs. partition is_even zs [0, 2] [3, 5]}" -values 10 "{zs. partition is_even zs [0, 7] [3, 5]}" - lemma [code_pred_intros]: "r a b \ tranclp r a b" "r a b \ tranclp r b c \ tranclp r a c" by auto +subsection {* transitive predicate *} + code_pred tranclp proof - case tranclp @@ -265,7 +357,7 @@ values 20 "{(n, m). tranclp succ n m}" *) -subsection{* IMP *} +subsection {* IMP *} types var = nat @@ -304,7 +396,7 @@ code_pred tupled_exec . -subsection{* CCS *} +subsection {* CCS *} text{* This example formalizes finite CCS processes without communication or recursion. For simplicity, labels are natural numbers. *} @@ -354,18 +446,15 @@ value [code] "Predicate.the (divmod_rel_1_2 1705 42)" -section {* Executing definitions *} +subsection {* Minimum *} definition Min where "Min s r x \ s x \ (\y. r x y \ x = y)" code_pred [inductify] Min . -subsection {* Examples with lists *} +subsection {* Lexicographic order *} -subsubsection {* Lexicographic order *} - -thm lexord_def code_pred [inductify] lexord . code_pred [inductify, rpred] lexord . thm lexord.equation @@ -392,13 +481,7 @@ values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" -(*values [random] "{xys. test_lexord xys}"*) -(*values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}"*) -(* -lemma "(u, v) : lexord less_than_nat ==> (x @ u, y @ v) : lexord less_than_nat" -quickcheck[generator=pred_compile] -oops -*) + lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv code_pred [inductify] lexn . @@ -414,12 +497,10 @@ code_pred [inductify, rpred] lenlex . thm lenlex.rpred_equation -thm lists.intros code_pred [inductify] lists . - thm lists.equation -section {* AVL Tree Example *} +subsection {* AVL Tree *} datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat fun height :: "'a tree => nat" where @@ -437,7 +518,6 @@ code_pred [rpred] avl . thm avl.rpred_equation -(*values [random] 10 "{t. avl (t::int tree)}"*) fun set_of where @@ -455,10 +535,9 @@ code_pred [inductify] is_ord . thm is_ord.equation -code_pred [rpred] is_ord . -thm is_ord.rpred_equation + -section {* Definitions about Relations *} +subsection {* Definitions about Relations *} code_pred [inductify] converse . thm converse.equation @@ -467,7 +546,7 @@ code_pred [inductify] Image . thm Image.equation (*TODO: *) -ML {* Toplevel.debug := true *} + declare Id_on_def[unfolded UNION_def, code_pred_def] code_pred [inductify] Id_on . @@ -475,7 +554,7 @@ code_pred [inductify] Domain . thm Domain.equation code_pred [inductify] Range . -thm sym_def +thm Range.equation code_pred [inductify] Field . declare Sigma_def[unfolded UNION_def, code_pred_def] declare refl_on_def[unfolded UNION_def, code_pred_def] @@ -483,10 +562,6 @@ thm refl_on.equation code_pred [inductify] total_on . thm total_on.equation -(* -code_pred [inductify] sym . -thm sym.equation -*) code_pred [inductify] antisym . thm antisym.equation code_pred [inductify] trans . @@ -496,12 +571,13 @@ code_pred [inductify] inv_image . thm inv_image.equation -section {* List functions *} +subsection {* Inverting list functions *} code_pred [inductify] length . +code_pred [inductify, rpred] length . thm size_listP.equation -code_pred [inductify, rpred] length . thm size_listP.rpred_equation + values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}" code_pred [inductify] concat . @@ -509,7 +585,6 @@ code_pred [inductify] tl . code_pred [inductify] last . code_pred [inductify] butlast . -(*code_pred [inductify] listsum .*) code_pred [inductify] take . code_pred [inductify] drop . code_pred [inductify] zip . @@ -526,15 +601,8 @@ code_pred [inductify] foldl . code_pred [inductify] filter . code_pred [inductify, rpred] filter . -thm filterP.rpred_equation -definition test where "test xs = filter (\x. x = (1::nat)) xs" -code_pred [inductify] test . -thm testP.equation -code_pred [inductify, rpred] test . -thm testP.rpred_equation - -section {* Context Free Grammar *} +subsection {* Context Free Grammar *} datatype alphabet = a | b @@ -553,79 +621,6 @@ values [random] 5 "{x. S\<^isub>1p x}" -inductive is_a where - "is_a a" - -inductive is_b where - "is_b b" - -code_pred is_a . -code_pred [depth_limited] is_a . -code_pred [rpred] is_a . - -values [random] "{x. is_a x}" -code_pred [depth_limited] is_b . -code_pred [rpred] is_b . - -code_pred [inductify, depth_limited] filter . - -values [depth_limit=5] "{x. filterP is_a [a, b] x}" -values [depth_limit=3] "{x. filterP is_b [a, b] x}" - -lemma "w \ S\<^isub>1 \ length (filter (\x. x = a) w) = 1" -(*quickcheck[generator=pred_compile, size=10]*) -oops - -inductive test_lemma where - "S\<^isub>1p w ==> filterP is_a w r1 ==> size_listP r1 r2 ==> filterP is_b w r3 ==> size_listP r3 r4 ==> r2 \ r4 ==> test_lemma w" -(* -code_pred [rpred] test_lemma . -*) -(* -definition test_lemma' where - "test_lemma' w == (w \ S\<^isub>1 \ (\ length [x <- w. x = a] = length [x <- w. x = b]))" - -code_pred [inductify, rpred] test_lemma' . -thm test_lemma'.rpred_equation -*) -(*thm test_lemma'.rpred_equation*) -(* -values [depth_limit=3 random] "{x. S\<^isub>1 x}" -*) -code_pred [depth_limited] is_b . -(* -code_pred [inductify, depth_limited] filter . -*) -thm filterP.intros -thm filterP.equation -(* -values [depth_limit=3] "{x. filterP is_b [a, b] x}" -find_theorems "test_lemma'_hoaux" -code_pred [depth_limited] test_lemma'_hoaux . -thm test_lemma'_hoaux.depth_limited_equation -values [depth_limit=2] "{x. test_lemma'_hoaux b}" -inductive test1 where - "\ test_lemma'_hoaux x ==> test1 x" -code_pred test1 . -code_pred [depth_limited] test1 . -thm test1.depth_limited_equation -thm test_lemma'_hoaux.depth_limited_equation -thm test1.intros - -values [depth_limit=2] "{x. test1 b}" - -thm filterP.intros -thm filterP.depth_limited_equation -values [depth_limit=3] "{x. filterP test_lemma'_hoaux [a, b] x}" -values [depth_limit=4 random] "{w. test_lemma w}" -values [depth_limit=4 random] "{w. test_lemma' w}" -*) -(* -theorem S\<^isub>1_sound: -"w \ S\<^isub>1p \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=pred_compile, size=15] -oops -*) inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where "[] \ S\<^isub>2" | "w \ A\<^isub>2 \ b # w \ S\<^isub>2" @@ -641,12 +636,6 @@ values [random] 10 "{x. S\<^isub>2 x}" -theorem S\<^isub>2_sound: -"w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" -(*quickcheck[generator=SML]*) -(*quickcheck[generator=pred_compile, size=15, iterations=1]*) -oops - inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where "[] \ S\<^isub>3" | "w \ A\<^isub>3 \ b # w \ S\<^isub>3" @@ -659,31 +648,6 @@ thm S\<^isub>3.equation values 10 "{x. S\<^isub>3 x}" -(* -theorem S\<^isub>3_sound: -"w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=pred_compile, size=10, iterations=1] -oops -*) -lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" -(*quickcheck[size=10, generator = pred_compile]*) -oops -(* -inductive test -where - "length [x \ w. a = x] = length [x \ w. x = b] ==> test w" -ML {* @{term "[x \ w. x = a]"} *} -code_pred (inductify_all) test . - -thm test.equation -*) -(* -theorem S\<^isub>3_complete: -"length [x \ w. x = a] = length [x \ w. b = x] \ w \ S\<^isub>3" -(*quickcheck[generator=SML]*) -quickcheck[generator=pred_compile, size=10, iterations=100] -oops -*) inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where "[] \ S\<^isub>4" @@ -693,25 +657,8 @@ | "\v \ A\<^isub>4; w \ A\<^isub>4\ \ b # v @ w \ A\<^isub>4" | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" -(* -theorem S\<^isub>4_sound: -"w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator = pred_compile, size=2, iterations=1] -oops -*) -theorem S\<^isub>4_complete: -"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" -(*quickcheck[generator = pred_compile, size=5, iterations=1]*) -oops -theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: -"w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -"w \ A\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1" -"w \ B\<^isub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1" -(*quickcheck[generator = pred_compile, size=5, iterations=1]*) -oops - -section {* Lambda *} +subsection {* Lambda *} datatype type = Atom nat @@ -728,7 +675,6 @@ "[]\i\ = None" | "(x # xs)\i\ = (case i of 0 \ Some x | Suc j \ xs \j\)" - inductive nth_el' :: "'a list \ nat \ 'a \ bool" where "nth_el' (x # xs) 0 x" @@ -738,8 +684,7 @@ where Var [intro!]: "nth_el' env x T \ env \ Var x : T" | Abs [intro!]: "T # env \ t : U \ env \ Abs T t : (T \ U)" -(* | App [intro!]: "env \ s : T \ U \ env \ t : T \ env \ (s \ t) : U" *) - | App [intro!]: "env \ s : U \ T \ env \ t : T \ env \ (s \ t) : U" + | App [intro!]: "env \ s : T \ U \ env \ t : T \ env \ (s \ t) : U" primrec lift :: "[dB, nat] => dB" @@ -763,15 +708,4 @@ | appR [simp, intro!]: "s \\<^sub>\ t ==> u \ s \\<^sub>\ u \ t" | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t" -lemma "Gamma \ t : T \ t \\<^sub>\ t' \ Gamma \ t' : T" -(*quickcheck[generator = pred_compile, size = 10, iterations = 1]*) -oops - -lemma filter_eq_ConsD: - "filter P ys = x#xs \ - \us vs. ys = ts @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs" -(*quickcheck[generator = pred_compile]*) -oops - - end \ No newline at end of file