# HG changeset patch # User bulwahn # Date 1258013442 -3600 # Node ID 4ec42d38224f094b984afe7a78d91968524d9d91 # Parent 24a91a380ee32f1fe826c0b6448517a1331081b9 changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned diff -r 24a91a380ee3 -r 4ec42d38224f src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 09:10:37 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 09:10:42 2009 +0100 @@ -1,7 +1,7 @@ (* Title: HOL/Tools/Predicate_Compile/predicate_compile.ML Author: Lukas Bulwahn, TU Muenchen -FIXME. +Entry point for the predicate compiler; definition of Toplevel commands code_pred and values *) signature PREDICATE_COMPILE = @@ -105,15 +105,16 @@ (Graph.strong_conn gr) thy end -fun extract_options ((modes, raw_options), const) = +fun extract_options (((expected_modes, proposed_modes), raw_options), const) = let fun chk s = member (op =) raw_options s in Options { - expected_modes = Option.map ((pair const) o (map fst)) modes, - user_proposals = - the_default [] (Option.map (map_filter - (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) modes), + expected_modes = Option.map (pair const) expected_modes, + proposed_modes = if not (null proposed_modes) then [(const, map fst proposed_modes)] else [], + proposed_names = + map_filter + (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name)) proposed_modes, show_steps = chk "show_steps", show_intermediate_results = chk "show_intermediate_results", show_proof_trace = chk "show_proof_trace", @@ -128,17 +129,18 @@ } end -fun code_pred_cmd ((modes, raw_options), raw_const) lthy = +fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy = let val thy = ProofContext.theory_of lthy val const = Code.read_const thy raw_const - val options = extract_options ((modes, raw_options), const) + val options = extract_options (((expected_modes, proposed_modes), raw_options), const) in if (is_inductify options) then let val lthy' = LocalTheory.theory (preprocess options const) lthy |> LocalTheory.checkpoint - val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of + val const = + case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of SOME c => c | NONE => const val _ = print_step options "Starting Predicate Compile Core..." @@ -159,7 +161,7 @@ in (* Parser for mode annotations *) - +(* FIXME: remove old parser *) (*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*) datatype raw_argmode = Argmode of string | Argmode_Tuple of string list @@ -205,8 +207,12 @@ Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE val opt_modes = - Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- - P.enum1 "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE + Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |-- + P.enum1 "," mode_and_opt_proposal --| P.$$$ ")") [] + +val opt_expected_modes = + Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |-- + P.enum "," new_parse_mode3 --| P.$$$ ")" >> SOME) NONE (* Parser for options *) @@ -219,10 +225,10 @@ val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; -val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME) +val opt_mode = (P.$$$ "_" >> K NONE) || (new_parse_mode3 >> SOME) val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- - P.enum ", " opt_smode --| P.$$$ "]" >> SOME) NONE + P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE val value_options = let @@ -238,7 +244,8 @@ val _ = OuterSyntax.local_theory_to_proof "code_pred" "prove equations for predicate specified by intro/elim rules" - OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd) + OuterKeyword.thy_goal + (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd) val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term diff -r 24a91a380ee3 -r 4ec42d38224f src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 09:10:37 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 09:10:42 2009 +0100 @@ -37,6 +37,19 @@ datatype mode' = Bool | Input | Output | Pair of mode' * mode' | Fun of mode' * mode' +(* equality of instantiatedness with respect to equivalences: + Pair Input Input == Input and Pair Output Output == Output *) +fun eq_mode' (Fun (m1, m2), Fun (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4) + | eq_mode' (Pair (m1, m2), Pair (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4) + | eq_mode' (Pair (m1, m2), Input) = eq_mode' (m1, Input) andalso eq_mode' (m2, Input) + | eq_mode' (Pair (m1, m2), Output) = eq_mode' (m1, Output) andalso eq_mode' (m2, Output) + | eq_mode' (Input, Pair (m1, m2)) = eq_mode' (Input, m1) andalso eq_mode' (Input, m2) + | eq_mode' (Output, Pair (m1, m2)) = eq_mode' (Output, m1) andalso eq_mode' (Output, m2) + | eq_mode' (Input, Input) = true + | eq_mode' (Output, Output) = true + | eq_mode' (Bool, Bool) = true + | eq_mode' _ = false + (* name: binder_modes? *) fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode' | strip_fun_mode Bool = [] @@ -60,7 +73,6 @@ | string_of_mode3 mode = string_of_mode2 mode in string_of_mode3 mode' end - fun translate_mode T (iss, is) = let val Ts = binder_types T @@ -86,45 +98,31 @@ mk_mode (param_modes @ translate_smode Ts2 is) end; +fun translate_mode' nparams mode' = + let + fun err () = error "translate_mode': given mode cannot be translated" + val (m1, m2) = chop nparams (strip_fun_mode mode') + val translate_to_tupled_mode = + (map_filter I) o (map_index (fn (i, m) => + if eq_mode' (m, Input) then SOME (i + 1) + else if eq_mode' (m, Output) then NONE + else err ())) + val translate_to_smode = + (map_filter I) o (map_index (fn (i, m) => + if eq_mode' (m, Input) then SOME (i + 1, NONE) + else if eq_mode' (m, Output) then NONE + else SOME (i + 1, SOME (translate_to_tupled_mode (dest_tuple_mode m))))) + fun translate_to_param_mode m = + case rev (dest_fun_mode m) of + Bool :: _ :: _ => SOME (translate_to_smode (strip_fun_mode m)) + | _ => if eq_mode' (m, Input) then NONE else err () + in + (map translate_to_param_mode m1, translate_to_smode m2) + end + fun string_of_mode thy constname mode = string_of_mode' (translate_mode (Sign.the_const_type thy constname) mode) -fun eq_mode' (Fun (m1, m2), Fun (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4) - | eq_mode' (Pair (m1, m2), Pair (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4) - | eq_mode' (Pair (m1, m2), Input) = eq_mode' (m1, Input) andalso eq_mode' (m2, Input) - | eq_mode' (Pair (m1, m2), Output) = eq_mode' (m1, Output) andalso eq_mode' (m2, Output) - | eq_mode' (Input, Pair (m1, m2)) = eq_mode' (Input, m1) andalso eq_mode' (Input, m2) - | eq_mode' (Output, Pair (m1, m2)) = eq_mode' (Output, m1) andalso eq_mode' (Output, m2) - | eq_mode' (Input, Input) = true - | eq_mode' (Output, Output) = true - | eq_mode' (Bool, Bool) = true - | eq_mode' _ = false -(* FIXME: remove! *) -fun eq_mode'_mode (mode', (iss, is)) = - let - val arg_modes = strip_fun_mode mode' - val (arg_modes1, arg_modes2) = chop (length iss) arg_modes - fun eq_arg Input NONE = true - | eq_arg _ NONE = false - | eq_arg mode (SOME is) = - let - val modes = dest_tuple_mode mode - in - forall (fn i => nth modes (i - 1) = Input) is - andalso forall (fn i => nth modes (i - 1) = Output) - (subtract (op =) is (1 upto length modes)) - end - fun eq_mode'_smode mode' is = - forall (fn (i, t) => eq_arg (nth mode' (i - 1)) t) is - andalso forall (fn i => (nth mode' (i - 1) = Output)) - (subtract (op =) (map fst is) (1 upto length mode')) - in - forall (fn (m, NONE) => m = Input | (m, SOME is) => eq_mode'_smode (strip_fun_mode m) is) - (arg_modes1 ~~ iss) - andalso eq_mode'_smode arg_modes2 is - end - - (* general syntactic functions *) (*Like dest_conj, but flattens conjunctions however nested*) @@ -133,8 +131,6 @@ 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 @@ -178,6 +174,8 @@ in nparams end; (*** check if a term contains only constructor functions ***) +(* FIXME: constructor terms are supposed to be seen in the way the code generator + sees constructors.*) fun is_constrt thy = let val cnstrs = flat (maps @@ -266,7 +264,8 @@ datatype options = Options of { expected_modes : (string * mode' list) option, - user_proposals : ((string * mode') * string) list, + proposed_modes : (string * mode' list) list, + proposed_names : ((string * mode') * string) list, show_steps : bool, show_proof_trace : bool, show_intermediate_results : bool, @@ -282,8 +281,9 @@ }; fun expected_modes (Options opt) = #expected_modes opt -fun user_proposal (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode') - (#user_proposals opt) (name, mode) +fun proposed_modes (Options opt) name = AList.lookup (op =) (#proposed_modes opt) name +fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode') + (#proposed_names opt) (name, mode) fun show_steps (Options opt) = #show_steps opt fun show_intermediate_results (Options opt) = #show_intermediate_results opt @@ -300,7 +300,8 @@ val default_options = Options { expected_modes = NONE, - user_proposals = [], + proposed_modes = [], + proposed_names = [], show_steps = false, show_intermediate_results = false, show_proof_trace = false, diff -r 24a91a380ee3 -r 4ec42d38224f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 09:10:37 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 09:10:42 2009 +0100 @@ -9,7 +9,7 @@ val setup : theory -> theory val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state - val values_cmd : string list -> Predicate_Compile_Aux.smode option list option + val values_cmd : string list -> Predicate_Compile_Aux.mode' option list option -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit val register_predicate : (string * thm list * thm * int) -> theory -> theory val register_intros : string * thm list -> theory -> theory @@ -957,7 +957,6 @@ (iss ~~ args1))) end end)) (AList.lookup op = modes name) - in case strip_comb (Envir.eta_contract t) of (Const (name, _), args) => the_default default (mk_modes name args) @@ -1513,7 +1512,7 @@ (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) []) val system_proposal = prefix ^ (Long_Name.base_name name) ^ (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ string_of_mode (snd mode) - val name = the_default system_proposal (user_proposal options name (translate_mode T mode)) + val name = the_default system_proposal (proposed_names options name (translate_mode T mode)) in Sign.full_bname thy name end; @@ -2076,7 +2075,7 @@ else Sidecond t | _ => Sidecond t) -fun prepare_intrs thy prednames intros = +fun prepare_intrs options thy prednames intros = let val intrs = map prop_of intros val nparams = nparams_of thy (hd prednames) @@ -2136,7 +2135,11 @@ (Rs as _ :: _, Type ("bool", [])) => map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us) end - val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds + val all_modes = map (fn (s, T) => + case proposed_modes options s of + NONE => (s, modes_of_typ T) + | SOME modes' => (s, map (translate_mode' nparams) modes')) + preds in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end; (* sanity check of introduction rules *) @@ -2244,7 +2247,7 @@ (*val _ = check_intros_elim_match thy prednames*) (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = - prepare_intrs thy prednames (maps (intros_of thy) prednames) + prepare_intrs options thy prednames (maps (intros_of thy) prednames) val _ = print_step options "Infering modes..." val moded_clauses = #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses @@ -2505,7 +2508,7 @@ val user_mode' = map (rpair NONE) user_mode val all_modes_of = if random then all_random_modes_of else all_modes_of fun fits_to is NONE = true - | fits_to is (SOME pm) = (is = pm) + | fits_to is (SOME pm) = (is = (snd (translate_mode' 0 pm))) fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) = fits_to is pm andalso valid (ms @ ms') pms | valid (NONE :: ms') pms = valid ms' pms @@ -2579,14 +2582,7 @@ in if k = ~1 orelse length ts < k then elemsT else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont end; - (* -fun random_values ctxt k t = - let - val thy = ProofContext.theory_of ctxt - val _ = - in - end; - *) + fun values_cmd print_modes param_user_modes options k raw_t state = let val ctxt = Toplevel.context_of state; diff -r 24a91a380ee3 -r 4ec42d38224f src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 09:10:37 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 09:10:42 2009 +0100 @@ -3,24 +3,10 @@ begin section {* Set operations *} -(* -definition Empty where "Empty == {}" -declare empty_def[symmetric, code_pred_inline] -*) + declare eq_reflection[OF empty_def, code_pred_inline] -(* -definition Union where "Union A B == A Un B" - -lemma [code_pred_intros]: "A x ==> Union A B x" -and [code_pred_intros] : "B x ==> Union A B x" -unfolding Union_def Un_def Collect_def mem_def by auto - -code_pred Union -unfolding Union_def Un_def Collect_def mem_def by auto - -declare Union_def[symmetric, code_pred_inline] -*) declare eq_reflection[OF Un_def, code_pred_inline] +declare eq_reflection[OF UNION_def, code_pred_inline] section {* Alternative list definitions *} @@ -49,7 +35,6 @@ done qed - subsection {* Alternative rules for list_all2 *} lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []" diff -r 24a91a380ee3 -r 4ec42d38224f src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 09:10:37 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 09:10:42 2009 +0100 @@ -6,28 +6,28 @@ inductive False' :: "bool" -code_pred (mode: bool) False' . +code_pred (expected_modes: bool) False' . code_pred [depth_limited] False' . code_pred [random] False' . inductive EmptySet :: "'a \ bool" -code_pred (mode: o => bool, i => bool) EmptySet . +code_pred (expected_modes: o => bool, i => bool) EmptySet . definition EmptySet' :: "'a \ bool" where "EmptySet' = {}" -code_pred (mode: o => bool, i => bool) [inductify] EmptySet' . +code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' . inductive EmptyRel :: "'a \ 'b \ bool" -code_pred (mode: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel . +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel . inductive EmptyClosure :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r :: "'a \ 'a \ bool" code_pred - (mode: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool, + (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool, (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool, (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool, (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool, @@ -43,21 +43,21 @@ where "False \ False''" -code_pred (mode: []) False'' . +code_pred (expected_modes: []) False'' . inductive EmptySet'' :: "'a \ bool" where "False \ EmptySet'' x" -code_pred (mode: [1]) EmptySet'' . -code_pred (mode: [], [1]) [inductify] EmptySet'' . +code_pred (expected_modes: [1]) EmptySet'' . +code_pred (expected_modes: [], [1]) [inductify] EmptySet'' . *) inductive True' :: "bool" where "True \ True'" -code_pred (mode: bool) True' . +code_pred (expected_modes: bool) True' . consts a' :: 'a @@ -65,13 +65,13 @@ where "Fact a' a'" -code_pred (mode: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact . +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact . inductive zerozero :: "nat * nat => bool" where "zerozero (0, 0)" -code_pred (mode: i => bool, i * o => bool, o * i => bool, o => bool) zerozero . +code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero . code_pred [random] zerozero . inductive JamesBond :: "nat => int => code_numeral => bool" @@ -96,7 +96,7 @@ where "(x = C) \ (x = D) ==> is_C_or_D x" -code_pred (mode: i => bool) is_C_or_D . +code_pred (expected_modes: i => bool) is_C_or_D . thm is_C_or_D.equation inductive is_D_or_E @@ -111,7 +111,7 @@ "is_D_or_E E" by (auto intro: is_D_or_E.intros) -code_pred (mode: o => bool, i => bool) is_D_or_E +code_pred (expected_modes: o => bool, i => bool) is_D_or_E proof - case is_D_or_E from this(1) show thesis @@ -149,7 +149,7 @@ text {* Compilation of is_FGH requires elimination rule for is_F_or_G *} -code_pred (mode: o => bool, i => bool) is_FGH +code_pred (expected_modes: o => bool, i => bool) is_FGH proof - case is_F_or_G from this(1) show thesis @@ -175,7 +175,7 @@ inductive zerozero' :: "nat * nat => bool" where "equals (x, y) (0, 0) ==> zerozero' (x, y)" -code_pred (mode: i => bool) zerozero' . +code_pred (expected_modes: i => bool) zerozero' . lemma zerozero'_eq: "zerozero' x == zerozero x" proof - @@ -195,7 +195,7 @@ text {* if preprocessing fails, zerozero'' will not have all modes. *} -code_pred (mode: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' . +code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' . subsection {* Numerals *} @@ -233,7 +233,7 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" -code_pred (mode: i => bool, o => bool) even . +code_pred (expected_modes: i => bool, o => bool) even . code_pred [depth_limited] even . code_pred [random] even . @@ -256,7 +256,7 @@ definition odd' where "odd' x == \ even x" -code_pred (mode: i => bool) [inductify] odd' . +code_pred (expected_modes: i => bool) [inductify] odd' . code_pred [inductify, depth_limited] odd' . code_pred [inductify, random] odd' . @@ -268,7 +268,7 @@ where "n mod 2 = 0 \ is_even n" -code_pred (mode: i => bool) is_even . +code_pred (expected_modes: i => bool) is_even . subsection {* append predicate *} @@ -276,8 +276,8 @@ "append [] xs xs" | "append xs ys zs \ append (x # xs) ys (x # zs)" -code_pred (mode: i => i => o => bool, o => o => i => bool as "slice", o => i => i => bool as prefix, - i => o => i => bool as suffix, i => i => i => bool) append . +code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix, + i => o => i => bool as suffix) append . code_pred [depth_limited] append . code_pred [random] append . code_pred [annotated] append . @@ -294,7 +294,7 @@ values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" values [random] 1 "{(ys, zs). append [1::nat, 2] ys zs}" -value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" +value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (slice ([]::int list))" @@ -310,7 +310,7 @@ lemmas [code_pred_intros] = append2_Nil append2.intros(2) -code_pred (mode: i => i => o => bool, o => o => i => bool, o => i => i => bool, +code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool, i => o => i => bool, i => i => i => bool) append2 proof - case append2 @@ -331,7 +331,7 @@ "tupled_append ([], xs, xs)" | "tupled_append (xs, ys, zs) \ tupled_append (x # xs, ys, x # zs)" -code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool, +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, i * o * i => bool, i * i * i => bool) tupled_append . code_pred [random] tupled_append . thm tupled_append.equation @@ -346,7 +346,7 @@ | "[| ys = fst (xa, y); x # zs = snd (xa, y); tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)" -code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool, +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, i * o * i => bool, i * i * i => bool) tupled_append' . thm tupled_append'.equation @@ -355,7 +355,7 @@ "tupled_append'' ([], xs, xs)" | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \ tupled_append'' (x # xs, yszs)" -code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool, +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, i * o * i => bool, i * i * i => bool) [inductify] tupled_append'' . thm tupled_append''.equation @@ -364,7 +364,7 @@ "tupled_append''' ([], xs, xs)" | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" -code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool, +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, i * o * i => bool, i * i * i => bool) [inductify] tupled_append''' . thm tupled_append'''.equation @@ -375,7 +375,7 @@ "map_ofP ((a, b)#xs) a b" | "map_ofP xs a b \ map_ofP (x#xs) a b" -code_pred (mode: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP . +code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP . thm map_ofP.equation subsection {* filter predicate *} @@ -387,7 +387,7 @@ | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)" | "\ P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys" -code_pred (mode: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 . +code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 . code_pred [depth_limited] filter1 . code_pred [random] filter1 . @@ -399,7 +399,7 @@ | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)" | "\ P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys" -code_pred (mode: i => i => i => bool, i => i => o => bool) filter2 . +code_pred (expected_modes: i => i => i => bool, i => i => o => bool) filter2 . code_pred [depth_limited] filter2 . code_pred [random] filter2 . thm filter2.equation @@ -410,7 +410,7 @@ where "List.filter P xs = ys ==> filter3 P xs ys" -code_pred (mode: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter3 . +code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter3 . code_pred [depth_limited] filter3 . thm filter3.depth_limited_equation @@ -418,7 +418,7 @@ where "List.filter P xs = ys ==> filter4 P xs ys" -code_pred (mode: i => i => o => bool, i => i => i => bool) filter4 . +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 . code_pred [depth_limited] filter4 . code_pred [random] filter4 . @@ -428,7 +428,7 @@ "rev [] []" | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" -code_pred (mode: i => o => bool, o => i => bool, i => i => bool) rev . +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev . thm rev.equation @@ -438,7 +438,7 @@ "tupled_rev ([], [])" | "tupled_rev (xs, xs') \ tupled_append (xs', [x], ys) \ tupled_rev (x#xs, ys)" -code_pred (mode: i * o => bool, o * i => bool, i * i => bool) tupled_rev . +code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev . thm tupled_rev.equation subsection {* partition predicate *} @@ -449,7 +449,7 @@ | "f x \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" -code_pred (mode: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool, +code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool, (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) partition . code_pred [depth_limited] partition . code_pred [random] partition . @@ -465,7 +465,7 @@ | "f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, x # ys, zs)" | "\ f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, ys, x # zs)" -code_pred (mode: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool, +code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool, (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition . thm tupled_partition.equation @@ -477,7 +477,7 @@ subsection {* transitive predicate *} -code_pred (mode: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl, +code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl, (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool, (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp proof - @@ -577,9 +577,8 @@ values 5 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" -(* FIXME: values 3 "{(a,q). step (par nil nil) a q}" -*) + inductive tupled_step :: "(proc \ nat \ proc) \ bool" where @@ -686,7 +685,7 @@ | "is_ord (MKT n l r h) = ((\n' \ set_of l. n' < n) \ (\n' \ set_of r. n < n') \ is_ord l \ is_ord r)" -code_pred (mode: i => o => bool, i => i => bool) [inductify] set_of . +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of . thm set_of.equation code_pred [inductify] is_ord . @@ -702,19 +701,15 @@ thm rel_comp.equation code_pred [inductify] Image . thm Image.equation -(*TODO: *) - -declare Id_on_def[unfolded UNION_def, code_pred_def] - -code_pred [inductify] Id_on . +code_pred (expected_modes: (o => bool) => o => bool, (o => bool) => i * o => bool, + (o => bool) => o * i => bool, (o => bool) => i => bool) [inductify] Id_on . thm Id_on.equation code_pred [inductify] Domain . thm Domain.equation code_pred [inductify] Range . 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] +thm Field.equation code_pred [inductify] refl_on . thm refl_on.equation code_pred [inductify] total_on . @@ -737,13 +732,13 @@ (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*) -code_pred (mode: i => o => bool, o => i => bool, i => i => bool) [inductify] concat . +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat . thm concatP.equation values "{ys. concatP [[1, 2], [3, (4::int)]] ys}" values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}" -code_pred [inductify, depth_limited] concat . +code_pred [inductify, depth_limited] List.concat . thm concatP.depth_limited_equation values [depth_limit = 3] 3 @@ -758,12 +753,12 @@ values [depth_limit = 5] 3 "{xs. concatP xs [(1::int), 2]}" -code_pred (mode: i => o => bool, i => i => bool) [inductify] hd . +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd . thm hdP.equation values "{x. hdP [1, 2, (3::int)] x}" values "{(xs, x). hdP [1, 2, (3::int)] 1}" -code_pred (mode: i => o => bool, i => i => bool) [inductify] tl . +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl . thm tlP.equation values "{x. tlP [1, 2, (3::nat)] x}" values "{x. tlP [1, 2, (3::int)] [3]}" @@ -876,7 +871,7 @@ | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" -code_pred (mode: o => bool, i => bool) S\<^isub>4p . +code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p . subsection {* Lambda *} @@ -928,12 +923,15 @@ | appR [simp, intro!]: "s \\<^sub>\ t ==> u \ s \\<^sub>\ u \ t" | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t" -code_pred (mode: i => i => o => bool, i => i => i => bool) typing . +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . thm typing.equation -code_pred (mode: i => o => bool as reduce, i => i => bool) beta . +code_pred (modes: i => o => bool as reduce) beta . thm beta.equation + +values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \\<^sub>\ x}" + code_pred [random] typing . values [random] 1 "{(\, t, T). \ \ t : T}"