# HG changeset patch # User bulwahn # Date 1253715613 -7200 # Node ID 90f3ce5d27ae85d65e6aa12200c51f3824040aad # Parent fbd2248507676b5f43b989afabecfa9ae570e019 added first version of quickcheck based on the predicate compiler; added a few quickcheck examples diff -r fbd224850767 -r 90f3ce5d27ae src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Wed Sep 23 16:20:13 2009 +0200 @@ -193,7 +193,15 @@ @{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.nat.nat_case"}, @{const_name "List.list.list_case"}, @{const_name Nat.ord_nat_inst.less_eq_nat}] +@{const_name "Nat.nat.nat_case"}, @{const_name "List.list.list_case"}, +@{const_name "Option.option.option_case"}, +@{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 obtain_specification_graph table constname = let diff -r fbd224850767 -r 90f3ce5d27ae src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Wed Sep 23 16:20:13 2009 +0200 @@ -69,19 +69,19 @@ fun transform_ho_typ (T as Type ("fun", _)) = let val (Ts, T') = strip_type T - in (Ts @ [T']) ---> HOLogic.boolT end + 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", _)) => (* if T = bool might be a relation already *) + (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 + let val (Ts, T') = strip_type T val Ts' = map transform_ho_typ Ts in @@ -194,22 +194,24 @@ 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 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) + 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) = - [(lookup_pred 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 (names, prems) = @@ -247,7 +249,7 @@ 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 then + 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')) => @@ -259,6 +261,7 @@ val pred = lookup_pred t val nparams = get_nparams pred val (params, args) = chop nparams args + val _ = tracing ("mk_prems'': " ^ (Syntax.string_of_term_global thy t) ^ " has " ^ string_of_int nparams ^ " parameters.") val params' = map (mk_param lookup_pred) params in folds_map mk_prems' args (names', prems) @@ -284,7 +287,7 @@ end in mk_prems' t (names, prems) - end; + end; (* assumption: mutual recursive predicates all have the same parameters. *) fun define_predicates specs thy = @@ -298,7 +301,7 @@ (* 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 =) (flat argss' \\ flat 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 @@ -344,26 +347,30 @@ Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) end fun mk_rewr_thm (func, pred) = @{thm refl} - - val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss)) - val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts - (* define new inductive predicates *) - val (ind_result, thy') = - Inductive.add_inductive_global (serial_string ()) - {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 thy'' = thy' - |> Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) - in - thy'' + in + case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of + NONE => thy + | SOME intr_ts => let + val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts + in + if is_some (try (map (cterm_of thy)) intr_ts) then + let + val (ind_result, thy') = + Inductive.add_inductive_global (serial_string ()) + {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 *) + in Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' end + else + thy + end end (* preprocessing intro rules - uses oracle *) @@ -374,7 +381,7 @@ fun lookup_pred (Const (name, T)) = (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of SOME c => Const (c, pred_type T) - | NONE => Const (name, T)) + | NONE => error ("Function " ^ name ^ " is not inductified")) | lookup_pred (Free (name, T)) = Free (name, T) | lookup_pred _ = error "lookup function is not defined!" @@ -387,17 +394,20 @@ val _ = tracing (Syntax.string_of_term_global thy intro_t) val (prems, concl) = Logic.strip_horn intro_t val frees = map fst (Term.add_frees intro_t []) - fun opt_dest_Not t = the_default t (try HOLogic.dest_not t) fun rewrite prem names = let - val (P, args) = (strip_comb o opt_dest_Not o HOLogic.dest_Trueprop) prem + 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 (list_comb (P, resargs)) + 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 diff -r fbd224850767 -r 90f3ce5d27ae src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Wed Sep 23 16:20:13 2009 +0200 @@ -68,57 +68,64 @@ | select_disj _ 1 = [rtac @{thm disjI1}] | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1)); -fun introrulify thy th = +fun introrulify thy ths = let - val ctxt = (ProofContext.init thy) - val ((_, [th']), ctxt') = Variable.import true [th] ctxt - 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 = + val ctxt = ProofContext.init thy + val ((_, ths'), ctxt') = Variable.import true ths ctxt + fun introrulify' th = let - val ((ps, t'), nctxt') = focus_ex t nctxt - val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t') + 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 - (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs)) + map_index prove_introrule (map mk_introrule disjuncts) 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) - |> singleton (Variable.export ctxt' ctxt) - 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 - maps (introrulify thy o rewrite) specs + introrulify thy (map rewrite specs) else if forall (is_intro constname) specs then - specs + 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 _ = priority "Defining local predicates and their intro rules..." + val _ = tracing ("Introduction rules of definitions before flattening: " + ^ commas (map (Display.string_of_thm ctxt) intros)) + val _ = tracing "Defining local predicates and their intro rules..." val (intros', (local_defs, thy')) = flatten_intros constname intros thy val (intross, thy'') = fold_map preprocess local_defs thy' in diff -r fbd224850767 -r 90f3ce5d27ae src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Wed Sep 23 16:20:13 2009 +0200 @@ -0,0 +1,93 @@ +(* Author: Lukas Bulwahn, TU Muenchen + +A quickcheck generator based on the predicate compiler +*) + +signature PRED_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) ref +end; + +structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK = +struct + +val test_ref = 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 {...} => setmp quick_and_dirty true (SkipProof.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 full_constname + |> Predicate_Compile_Core.add_equations [full_constname] + |> Predicate_Compile_Core.add_sizelim_equations [full_constname] + |> Predicate_Compile_Core.add_quickcheck_equations [full_constname] + val sizelim_modes = Predicate_Compile_Core.sizelim_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_rpredT (HOLogic.mk_tupleT (map snd vs'))) + in Const (name, T) $ Bound 0 end + else if member (op =) sizelim_modes ([], []) then + let + val name = Predicate_Compile_Core.sizelim_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) ("Pred_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 fbd224850767 -r 90f3ce5d27ae src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 23 16:20:13 2009 +0200 @@ -4,6 +4,7 @@ signature PREDICATE_COMPILE = sig val setup : theory -> theory + val preprocess : string -> theory -> theory end; structure Predicate_Compile : PREDICATE_COMPILE = @@ -33,28 +34,43 @@ val _ = priority "Compiling predicates to flat introrules..." val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess (get_specs prednames) thy') - val _ = tracing ("intross: " ^ commas (map (Display.string_of_thm_global thy'') (flat intross))) + val _ = tracing ("Flattened introduction rules: " ^ + commas (map (Display.string_of_thm_global thy'') (flat intross))) val _ = priority "Replacing functions in introrules..." - val intross' = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross + (* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *) + val intross' = + case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of + SOME intross' => intross' + | NONE => let val _ = warning "Function replacement failed!" in intross end + val _ = tracing ("Introduction rules with replaced functions: " ^ + commas (map (Display.string_of_thm_global thy'') (flat intross'))) val intross'' = burrow (maps remove_pointless_clauses) intross' + val intross'' = burrow (map (AxClass.overload thy'')) intross'' + val _ = priority "Registering intro rules..." val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy'' in thy''' end; +fun preprocess const thy = + let + val _ = Output.tracing ("Fetching definitions from theory...") + val table = Pred_Compile_Data.make_const_spec_table thy + val gr = Pred_Compile_Data.obtain_specification_graph table const + val _ = Output.tracing (commas (Graph.all_succs gr [const])) + val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr + in fold_rev (preprocess_strong_conn_constnames gr) + (Graph.strong_conn gr) thy + end + fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy = if inductify_all then let val thy = ProofContext.theory_of lthy val const = Code.read_const thy raw_const - val _ = Output.tracing ("fetching definition from theory") - val table = Pred_Compile_Data.make_const_spec_table thy - val gr = Pred_Compile_Data.obtain_specification_graph table const - val _ = Output.tracing (commas (Graph.all_succs gr [const])) - val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr - val lthy' = LocalTheory.theory (fold_rev (preprocess_strong_conn_constnames gr) - (Graph.strong_conn gr)) lthy + val lthy' = LocalTheory.theory (preprocess const) lthy |> LocalTheory.checkpoint + val _ = tracing "Starting Predicate Compile Core..." in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end else Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy diff -r fbd224850767 -r 90f3ce5d27ae src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 23 16:20:13 2009 +0200 @@ -23,6 +23,10 @@ val predfun_name_of: theory -> string -> mode -> string val all_preds_of : theory -> string list val modes_of: theory -> string -> mode list + val sizelim_modes_of: theory -> string -> mode list + val sizelim_function_name_of : theory -> string -> mode -> string + val generator_modes_of: theory -> string -> mode list + val generator_name_of : theory -> string -> mode -> string val string_of_mode : mode -> string val intros_of: theory -> string -> thm list val nparams_of: theory -> string -> int @@ -82,6 +86,7 @@ theory -> (moded_clause list) pred_mode_table -> unit val print_compiled_terms : theory -> term pred_mode_table -> unit (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*) + val pred_compfuns : compilation_funs val rpred_compfuns : compilation_funs val dest_funT : typ -> typ * typ (* val depending_preds_of : theory -> thm list -> string list *) @@ -128,7 +133,7 @@ (* reference to preprocessing of InductiveSet package *) -val ind_set_codegen_preproc = Inductive_Set.codegen_preproc; +val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*) (** fundamentals **) @@ -246,12 +251,13 @@ fun mk_casesrule ctxt nparams introrules = let - val intros = map (Logic.unvarify o prop_of) introrules + val ((_, intros_th), ctxt1) = Variable.import false introrules ctxt + val intros = map prop_of intros_th val (pred, (params, args)) = strip_intro_concl nparams (hd intros) - val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt + val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) - val (argnames, ctxt2) = Variable.variant_fixes - (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1 + val (argnames, ctxt3) = Variable.variant_fixes + (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt2 val argvs = map2 (curry Free) argnames (map fastype_of args) fun mk_case intro = let @@ -353,6 +359,10 @@ val modes_of = (map fst) o #functions oo the_pred_data +val sizelim_modes_of = (map fst) o #sizelim_functions oo the_pred_data + +val rpred_modes_of = (map fst) o #generators oo the_pred_data + fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) val is_compiled = not o null o #functions oo the_pred_data @@ -646,17 +656,19 @@ in if not (member (op =) (Graph.keys (PredData.get thy)) name) then PredData.map - (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy + (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy else thy end fun register_intros pre_intros thy = let - val (_, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros)))) - val nparams = guess_nparams T - val pre_elim = - (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy))) - (mk_casesrule (ProofContext.init thy) nparams pre_intros) + val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros)))) + val _ = Output.tracing ("Registering introduction rules of " ^ c) + val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) pre_intros)) + val nparams = guess_nparams T + val pre_elim = + (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy))) + (mk_casesrule (ProofContext.init thy) nparams pre_intros) in register_predicate (pre_intros, pre_elim, nparams) thy end fun set_generator_name pred mode name = @@ -716,24 +728,9 @@ (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs)) end; -fun sizelim_funT_of compfuns (iss, is) T = - let - val Ts = binder_types T - val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts - val paramTs' = map2 (fn SOME is => sizelim_funT_of compfuns ([], is) | NONE => I) iss paramTs - in - (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs)) - end; - fun mk_fun_of compfuns thy (name, T) mode = Const (predfun_name_of thy name mode, funT_of compfuns mode T) -fun mk_sizelim_fun_of compfuns thy (name, T) mode = - Const (sizelim_function_name_of thy name mode, sizelim_funT_of compfuns mode T) - -fun mk_generator_of compfuns thy (name, T) mode = - Const (generator_name_of thy name mode, sizelim_funT_of compfuns mode T) - structure PredicateCompFuns = struct @@ -852,6 +849,7 @@ end; (* for external use with interactive mode *) +val pred_compfuns = PredicateCompFuns.compfuns val rpred_compfuns = RPredCompFuns.compfuns; fun lift_random random = @@ -862,7 +860,22 @@ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> RPredCompFuns.mk_rpredT T) $ random end; - + +fun sizelim_funT_of compfuns (iss, is) T = + let + val Ts = binder_types T + val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts + val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs + in + (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs)) + end; + +fun mk_sizelim_fun_of compfuns thy (name, T) mode = + Const (sizelim_function_name_of thy name mode, sizelim_funT_of compfuns mode T) + +fun mk_generator_of compfuns thy (name, T) mode = + Const (generator_name_of thy name mode, sizelim_funT_of compfuns mode T) + (* Mode analysis *) (*** check if a term contains only constructor functions ***) @@ -1058,7 +1071,7 @@ SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) (case p of Prem (us, _) => vs union terms_vs us | _ => vs) (filter_out (equal p) ps) - | NONE => + | _ => let val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length)) in @@ -1069,7 +1082,7 @@ | NONE => let val _ = Output.tracing ("ps:" ^ (commas (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps))) - in error "mode analysis failed" end + in (*error "mode analysis failed"*)NONE end end) else NONE) @@ -1232,27 +1245,42 @@ | compile_param_ext _ _ _ _ = error "compile params" *) -fun compile_param size thy compfuns (NONE, t) = t - | compile_param size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = +fun compile_param neg_in_sizelim size thy compfuns (NONE, t) = t + | compile_param neg_in_sizelim size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = let val (f, args) = strip_comb (Envir.eta_contract t) val (params, args') = chop (length ms) args - val params' = map (compile_param size thy compfuns) (ms ~~ params) + val params' = map (compile_param neg_in_sizelim size thy compfuns) (ms ~~ params) val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of val f' = case f of Const (name, T) => mk_fun_of compfuns thy (name, T) (iss, is') - | Free (name, T) => Free (name, funT_of compfuns (iss, is') T) + | Free (name, T) => + case neg_in_sizelim of + SOME _ => Free (name, sizelim_funT_of compfuns (iss, is') T) + | NONE => Free (name, funT_of compfuns (iss, is') T) + | _ => error ("PredicateCompiler: illegal parameter term") - in list_comb (f', params' @ args') end - -fun compile_expr size thy ((Mode (mode, is, ms)), t) = + in + (case neg_in_sizelim of SOME size_t => + (fn t => + let + val Ts = fst (split_last (binder_types (fastype_of t))) + val names = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) + in + list_abs (names ~~ Ts, list_comb (t, (map Bound ((length Ts) - 1 downto 0)) @ [size_t])) + end) + | NONE => I) + (list_comb (f', params' @ args')) + end + +fun compile_expr neg_in_sizelim size thy ((Mode (mode, is, ms)), t) = case strip_comb t of (Const (name, T), params) => let - val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params) + val params' = map (compile_param neg_in_sizelim size thy PredicateCompFuns.compfuns) (ms ~~ params) val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of in list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params') @@ -1264,16 +1292,18 @@ list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args) end; -fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) = +fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) inargs = case strip_comb t of (Const (name, T), params) => let - val params' = map (compile_param size thy compfuns) (ms ~~ params) + val params' = map (compile_param NONE size thy PredicateCompFuns.compfuns) (ms ~~ params) in - list_comb (mk_generator_of compfuns thy (name, T) mode, params') + list_comb (mk_generator_of compfuns thy (name, T) mode, params' @ inargs) end - | (Free (name, T), args) => - list_comb (Free (name, sizelim_funT_of RPredCompFuns.compfuns ([], is) T), args) + | (Free (name, T), params) => + lift_pred compfuns + (list_comb (Free (name, sizelim_funT_of PredicateCompFuns.compfuns ([], is) T), params @ inargs)) + (** specific rpred functions -- move them to the correct place in this file *) @@ -1292,7 +1322,72 @@ end | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term" *) +fun mk_Eval_of size ((x, T), NONE) names = (x, names) + | mk_Eval_of size ((x, T), SOME mode) names = + let + val Ts = binder_types T + (*val argnames = Name.variant_list names + (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); + val args = map Free (argnames ~~ Ts) + val (inargs, outargs) = split_smode mode args*) + fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", 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 mk_arg (i, T) = + let + val vname = Name.variant names ("x" ^ string_of_int i) + val default = Free (vname, T) + in + case AList.lookup (op =) mode i of + NONE => (([], [default]), [default]) + | SOME NONE => (([default], []), [default]) + | SOME (SOME pis) => + case HOLogic.strip_tupleT T of + [] => error "pair mode but unit tuple" (*(([default], []), [default])*) + | [_] => error "pair mode but not a tuple" (*(([default], []), [default])*) + | Ts => + let + val vnames = Name.variant_list names + (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j) + (1 upto length Ts)) + val args = map Free (vnames ~~ Ts) + fun split_args (i, arg) (ins, outs) = + if member (op =) pis i then + (arg::ins, outs) + else + (ins, arg::outs) + val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], []) + fun tuple args = if null args then [] else [HOLogic.mk_tuple args] + in ((tuple inargs, tuple outargs), args) end + end + val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts)) + val (inargs, outargs) = pairself flat (split_list inoutargs) + val size_t = case size of NONE => [] | SOME size_t => [size_t] + val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ size_t), mk_tuple outargs) + val t = fold_rev mk_split_lambda args r + in + (t, names) + end; +fun compile_arg size thy param_vs iss arg = + let + val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of + fun map_params (t as Free (f, T)) = + if member (op =) param_vs f then + case (the (AList.lookup (op =) (param_vs ~~ iss) f)) of + SOME is => let val T' = funT_of PredicateCompFuns.compfuns ([], is) T + in fst (mk_Eval_of size ((Free (f, T'), T), SOME is) []) end + | NONE => t + else t + | map_params t = t + in map_aterms map_params arg end + fun compile_clause compfuns size final_term thy all_vs param_vs (iss, is) inp (ts, moded_ps) = let fun check_constrt t (names, eqs) = @@ -1331,11 +1426,12 @@ Prem (us, t) => let val (in_ts, out_ts''') = split_smode is us; + val in_ts = map (compile_arg size thy param_vs iss) in_ts val args = case size of NONE => in_ts | SOME size_t => in_ts @ [size_t] val u = lift_pred compfuns - (list_comb (compile_expr size thy (mode, t), args)) + (list_comb (compile_expr NONE size thy (mode, t), args)) val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1344,7 +1440,7 @@ let val (in_ts, out_ts''') = split_smode is us val u = lift_pred compfuns - (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr NONE thy (mode, t), in_ts))) + (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr size NONE thy (mode, t), in_ts))) val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) @@ -1361,14 +1457,14 @@ val args = case size of NONE => in_ts | SOME size_t => in_ts @ [size_t] - val u = list_comb (compile_gen_expr size thy compfuns (mode, t), args) + val u = compile_gen_expr size thy compfuns (mode, t) args val rest = compile_prems out_ts''' vs' names'' ps in (u, rest) end | Generator (v, T) => let - val u = lift_random (HOLogic.mk_random T @{term "1::code_numeral"}) + val u = lift_random (HOLogic.mk_random T (the size)) val rest = compile_prems [Free (v, T)] vs' names'' ps; in (u, rest) @@ -1387,7 +1483,7 @@ val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) val (Us1, Us2) = split_smodeT (snd mode) Ts2 val funT_of = if use_size then sizelim_funT_of else funT_of - val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1 + val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1 val size_name = Name.variant (all_vs @ param_vs) "size" fun mk_input_term (i, NONE) = [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] @@ -1439,58 +1535,6 @@ (fn NONE => "X" | SOME k' => string_of_int k') (ks @ [SOME k]))) arities)); -fun mk_Eval_of ((x, T), NONE) names = (x, names) - | mk_Eval_of ((x, T), SOME mode) names = - let - val Ts = binder_types T - (*val argnames = Name.variant_list names - (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); - val args = map Free (argnames ~~ Ts) - val (inargs, outargs) = split_smode mode args*) - fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", 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 mk_arg (i, T) = - let - val vname = Name.variant names ("x" ^ string_of_int i) - val default = Free (vname, T) - in - case AList.lookup (op =) mode i of - NONE => (([], [default]), [default]) - | SOME NONE => (([default], []), [default]) - | SOME (SOME pis) => - case HOLogic.strip_tupleT T of - [] => error "pair mode but unit tuple" (*(([default], []), [default])*) - | [_] => error "pair mode but not a tuple" (*(([default], []), [default])*) - | Ts => - let - val vnames = Name.variant_list names - (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j) - (1 upto length Ts)) - val args = map Free (vnames ~~ Ts) - fun split_args (i, arg) (ins, outs) = - if member (op =) pis i then - (arg::ins, outs) - else - (ins, arg::outs) - val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], []) - fun tuple args = if null args then [] else [HOLogic.mk_tuple args] - in ((tuple inargs, tuple outargs), args) end - end - val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts)) - val (inargs, outargs) = pairself flat (split_list inoutargs) - val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs), mk_tuple outargs) - val t = fold_rev mk_split_lambda args r - in - (t, names) - end; - fun create_intro_elim_rule (mode as (iss, is)) defthm mode_id funT pred thy = let val Ts = binder_types (fastype_of pred) @@ -1524,7 +1568,7 @@ val param_names' = Name.variant_list (param_names @ argnames) (map (fn i => "p" ^ string_of_int i) (1 upto (length iss))) val param_vs = map Free (param_names' ~~ Ts1) - val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ iss) [] + val (params', names) = fold_map (mk_Eval_of NONE) ((params ~~ Ts1) ~~ iss) [] val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args)) val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args)) val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params') @@ -1627,7 +1671,7 @@ val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names val (xinout, xargs) = split_list xinoutargs val (xins, xouts) = pairself flat (split_list xinout) - val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names + val (xparams', names') = fold_map (mk_Eval_of NONE) ((xparams ~~ Ts1) ~~ iss) names fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t | mk_split_lambda [x] t = lambda x t | mk_split_lambda xs t = @@ -1670,14 +1714,23 @@ in fold create_definition modes thy end; - + +fun generator_funT_of (iss, is) T = + let + val Ts = binder_types T + val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts + val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs + in + (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT RPredCompFuns.compfuns (mk_tupleT outargTs)) + end + fun rpred_create_definitions preds (name, modes) thy = let val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = let val mode_cname = create_constname_of_mode thy "gen_" name mode - val funT = sizelim_funT_of RPredCompFuns.compfuns mode T + val funT = generator_funT_of mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] |> set_generator_name name mode mode_cname @@ -2166,6 +2219,7 @@ fun add_equations_of steps prednames thy = let val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") + val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = prepare_intrs thy prednames val _ = Output.tracing "Infering modes..." @@ -2229,7 +2283,7 @@ create_definitions = create_definitions, compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false, prove = prove, - are_not_defined = (fn thy => forall (null o modes_of thy)), + are_not_defined = fn thy => forall (null o modes_of thy), qname = "equation"} val add_sizelim_equations = gen_add_equations @@ -2237,7 +2291,7 @@ create_definitions = sizelim_create_definitions, compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true, prove = prove_by_skip, - are_not_defined = (fn thy => fn preds => true), (* TODO *) + are_not_defined = fn thy => forall (null o sizelim_modes_of thy), qname = "sizelim_equation" } @@ -2246,7 +2300,7 @@ create_definitions = rpred_create_definitions, compile_preds = compile_preds RPredCompFuns.compfuns mk_generator_of true, prove = prove_by_skip, - are_not_defined = (fn thy => fn preds => true), (* TODO *) + are_not_defined = fn thy => forall (null o rpred_modes_of thy), qname = "rpred_equation"} (** user interface **) @@ -2304,7 +2358,8 @@ in goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> (if rpred then - (add_sizelim_equations [const] #> add_quickcheck_equations [const]) + (add_equations [const] #> + add_sizelim_equations [const] #> add_quickcheck_equations [const]) else add_equations [const])) end in @@ -2339,7 +2394,7 @@ | m :: _ :: _ => (warning ("Multiple modes possible for comprehension " ^ Syntax.string_of_term_global thy t_compr); m); val (inargs, outargs) = split_smode user_mode' args; - val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs); + val t_pred = list_comb (compile_expr NONE NONE thy (m, list_comb (pred, params)), inargs); val t_eval = if null outargs then t_pred else let val outargs_bounds = map (fn Bound i => i) outargs; @@ -2372,7 +2427,14 @@ in if k = ~1 orelse length ts < k then elemsT else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr end; - + (* +fun random_values ctxt k t = + let + val thy = ProofContext.theory_of ctxt + val _ = + in + end; + *) fun values_cmd modes k raw_t state = let val ctxt = Toplevel.context_of state; @@ -2385,6 +2447,7 @@ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end; + local structure P = OuterParse in val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; diff -r fbd224850767 -r 90f3ce5d27ae src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Wed Sep 23 16:20:13 2009 +0200 @@ -8,8 +8,10 @@ "../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", Pred_Compile_Quickcheck.quickcheck) *} end \ No newline at end of file diff -r fbd224850767 -r 90f3ce5d27ae src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:13 2009 +0200 @@ -88,11 +88,11 @@ case tranclp from this converse_tranclpE[OF this(1)] show thesis by metis qed - +(* code_pred (inductify_all) (rpred) tranclp . thm tranclp.equation thm tranclp.rpred_equation - +*) inductive succ :: "nat \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" @@ -190,13 +190,24 @@ subsection {* Examples with lists *} +inductive filterP for Pa where +"(filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) [] []" +| "[| (res::'a list) = (y::'a) # (resa::'a list); (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) resa; Pa y |] +==> filterP Pa (y # xt) res" +| "[| (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) (res::'a list); ~ Pa (y::'a) |] ==> filterP Pa (y # xt) res" + +(* +code_pred (inductify_all) (rpred) filterP . +thm filterP.rpred_equation +*) + code_pred (inductify_all) lexord . thm lexord.equation -(* -lemma "(u, v) : lexord r ==> (x @ u, x @ v) : lexord r" -quickcheck -*) + +lemma "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" +(*quickcheck[generator=pred_compile]*) +oops lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv @@ -214,7 +225,7 @@ thm lists.equation -datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat +datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat fun height :: "'a tree => nat" where "height ET = 0" | "height (MKT x l r h) = max (height l) (height r) + 1" @@ -228,6 +239,9 @@ code_pred (inductify_all) avl . thm avl.equation +lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\(y::'a::type). False)" +unfolding bot_fun_inst.bot_fun[symmetric] bot_bool_eq[symmetric] bot_fun_eq by simp + fun set_of where "set_of ET = {}" @@ -241,17 +255,13 @@ declare Un_def[code_pred_def] -lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\(y::'a::type). False)" -unfolding bot_fun_inst.bot_fun[symmetric] -unfolding bot_bool_eq[symmetric] -unfolding bot_fun_eq by simp - code_pred (inductify_all) set_of . thm set_of.equation - +(* FIXME *) +(* code_pred (inductify_all) is_ord . thm is_ord.equation - +*) section {* Definitions about Relations *} code_pred (inductify_all) converse . @@ -277,10 +287,158 @@ thm S\<^isub>1p.equation -code_pred (inductify_all) (rpred) S\<^isub>1p . +theorem S\<^isub>1_sound: +"w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[generator=pred_compile] +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_all) (rpred) S\<^isub>2 . +ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name "B\<^isub>2"} *} +*) +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=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" + +ML {* reset Predicate_Compile_Core.do_proofs *} +(* +code_pred (inductify_all) S\<^isub>3 . +*) +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 + +theorem S\<^isub>3_complete: +"length [x \ w. x = a] = length [x \ w. x = b] \ 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" +| "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 = pred_compile, size=2, iterations=1] +sorry + +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] +sorry + +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]*) +sorry + -thm S\<^isub>1p.rpred_equation +section {* Lambda *} +datatype type = + Atom nat + | Fun type type (infixr "\" 200) + +datatype dB = + Var nat + | App dB dB (infixl "\" 200) + | Abs type dB + +primrec + nth_el :: "'a list \ nat \ 'a option" ("_\_\" [90, 0] 91) +where + "[]\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" +| "nth_el' xs i y \ nth_el' (x # xs) (Suc i) y" +*) +inductive typing :: "type list \ dB \ type \ bool" ("_ \ _ : _" [50, 50, 50] 50) + where + Var [intro!]: "nth_el env x = Some 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" + +primrec + lift :: "[dB, nat] => dB" +where + "lift (Var i) k = (if i < k then Var i else Var (i + 1))" + | "lift (s \ t) k = lift s k \ lift t k" + | "lift (Abs T s) k = Abs T (lift s (k + 1))" +primrec + subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) +where + subst_Var: "(Var i)[s/k] = + (if k < i then Var (i - 1) else if i = k then s else Var i)" + | subst_App: "(t \ u)[s/k] = t[s/k] \ u[s/k]" + | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])" + +inductive beta :: "[dB, dB] => bool" (infixl "\\<^sub>\" 50) + where + beta [simp, intro!]: "Abs T s \ t \\<^sub>\ s[t/0]" + | appL [simp, intro!]: "s \\<^sub>\ t ==> s \ u \\<^sub>\ t \ u" + | 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 = 1000] +oops +(* FIXME *) +(* +inductive test for P where +"[| filter P vs = res |] +==> test P vs res" + +code_pred test . +*) +(* +export_code test_for_1_yields_1_2 in SML file - +code_pred (inductify_all) (rpred) test . + +thm test.equation +*) + +ML {*set Toplevel.debug *} + +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