# HG changeset patch # User bulwahn # Date 1256821435 -3600 # Node ID d8bfa9564a523adefb1fc17f4a8cc0920973beb8 # Parent d6eb7f19bfc605250a276356810c2bdb9fcf596b# Parent 6ff4674499ca6c52a91cd114616fb9f6796f0eed merged diff -r 6ff4674499ca -r d8bfa9564a52 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 29 13:37:55 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Oct 29 14:03:55 2009 +0100 @@ -156,10 +156,35 @@ local structure P = OuterParse in +(*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*) +datatype raw_argmode = Argmode of string | Argmode_Tuple of string list + +val parse_argmode' = + ((Args.$$$ "i" || Args.$$$ "o") >> Argmode) || + (Args.$$$ "(" |-- P.enum1 "," (Args.$$$ "i" || Args.$$$ "o") --| Args.$$$ ")" >> Argmode_Tuple) + +fun mk_numeral_mode ss = flat (map_index (fn (i, s) => if s = "i" then [i + 1] else []) ss) + +val parse_smode' = P.$$$ "[" |-- P.enum1 "," parse_argmode' --| P.$$$ "]" + >> (fn m => flat (map_index + (fn (i, Argmode s) => if s = "i" then [(i + 1, NONE)] else [] + | (i, Argmode_Tuple ss) => [(i + 1, SOME (mk_numeral_mode ss))]) m)) + +val parse_smode = (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") + >> map (rpair (NONE : int list option)) + +fun gen_parse_mode smode_parser = + (Scan.optional + ((P.enum "=>" ((Args.$$$ "X" >> K NONE) || (smode_parser >> SOME))) --| Args.$$$ "==>") []) + -- smode_parser + +val parse_mode = gen_parse_mode parse_smode + +val parse_mode' = gen_parse_mode parse_smode' + val opt_modes = Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- - P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") - --| P.$$$ ")" >> SOME) NONE + P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE val scan_params = let @@ -170,8 +195,7 @@ val _ = OuterSyntax.local_theory_to_proof "code_pred" "prove equations for predicate specified by intro/elim rules" - OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> - code_pred_cmd) + OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd) end diff -r 6ff4674499ca -r d8bfa9564a52 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Oct 29 13:37:55 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Oct 29 14:03:55 2009 +0100 @@ -9,6 +9,29 @@ structure Predicate_Compile_Aux = struct + +(* mode *) + +type smode = (int * int list option) list +type mode = smode option list * smode +datatype tmode = Mode of mode * smode * tmode option list; + +fun string_of_smode js = + commas (map + (fn (i, is) => + string_of_int i ^ (case is of NONE => "" + | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js) + +fun string_of_mode (iss, is) = space_implode " -> " (map + (fn NONE => "X" + | SOME js => enclose "[" "]" (string_of_smode js)) + (iss @ [SOME is])); + +fun string_of_tmode (Mode (predmode, termmode, param_modes)) = + "predmode: " ^ (string_of_mode predmode) ^ + (if null param_modes then "" else + "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes)) + (* general syntactic functions *) (*Like dest_conj, but flattens conjunctions however nested*) @@ -136,7 +159,7 @@ (* Different options for compiler *) datatype options = Options of { - expected_modes : (string * int list list) option, + expected_modes : (string * mode list) option, show_steps : bool, show_proof_trace : bool, show_intermediate_results : bool, diff -r 6ff4674499ca -r d8bfa9564a52 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 29 13:37:55 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 29 14:03:55 2009 +0100 @@ -9,24 +9,20 @@ 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 - type smode = (int * int list option) list - type mode = smode option list * smode - datatype tmode = Mode of mode * smode * tmode option list; val register_predicate : (string * thm list * thm * int) -> theory -> theory val register_intros : string * thm list -> theory -> theory val is_registered : theory -> string -> bool - val predfun_intro_of: theory -> string -> mode -> thm - val predfun_elim_of: theory -> string -> mode -> thm - val predfun_name_of: theory -> string -> mode -> string + val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm + val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm + val predfun_name_of: theory -> string -> Predicate_Compile_Aux.mode -> string val all_preds_of : theory -> string list - val modes_of: theory -> string -> mode list - val depth_limited_modes_of: theory -> string -> mode list - val depth_limited_function_name_of : theory -> string -> mode -> string - val generator_modes_of: theory -> string -> mode list - val generator_name_of : theory -> string -> mode -> string - val all_modes_of : theory -> (string * mode list) list - val all_generator_modes_of : theory -> (string * mode list) list - val string_of_mode : mode -> string + val modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string + val generator_modes_of: theory -> string -> Predicate_Compile_Aux.mode list + val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string + val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list + val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list val intros_of: theory -> string -> thm list val nparams_of: theory -> string -> int val add_intro: thm -> theory -> theory @@ -67,8 +63,6 @@ (* debug stuff *) -fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); - fun print_tac s = Seq.single; fun print_tac' options s = @@ -140,9 +134,6 @@ type mode = arg_mode list type tmode = Mode of mode * *) -type smode = (int * int list option) list -type mode = smode option list * smode; -datatype tmode = Mode of mode * smode * tmode option list; fun gen_split_smode (mk_tuple, strip_tuple) smode ts = let @@ -165,32 +156,16 @@ (split_smode' smode (i+1) ts) in split_smode' smode 1 ts end -val split_smode = gen_split_smode (HOLogic.mk_tuple, HOLogic.strip_tuple) -val split_smodeT = gen_split_smode (HOLogic.mk_tupleT, HOLogic.strip_tupleT) +fun split_smode smode ts = gen_split_smode (HOLogic.mk_tuple, HOLogic.strip_tuple) smode ts +fun split_smodeT smode ts = gen_split_smode (HOLogic.mk_tupleT, HOLogic.strip_tupleT) smode ts fun gen_split_mode split_smode (iss, is) ts = let val (t1, t2) = chop (length iss) ts in (t1, split_smode is t2) end -val split_mode = gen_split_mode split_smode -val split_modeT = gen_split_mode split_smodeT - -fun string_of_smode js = - commas (map - (fn (i, is) => - string_of_int i ^ (case is of NONE => "" - | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js) - -fun string_of_mode (iss, is) = space_implode " -> " (map - (fn NONE => "X" - | SOME js => enclose "[" "]" (string_of_smode js)) - (iss @ [SOME is])); - -fun string_of_tmode (Mode (predmode, termmode, param_modes)) = - "predmode: " ^ (string_of_mode predmode) ^ - (if null param_modes then "" else - "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes)) +fun split_mode (iss, is) ts = gen_split_mode split_smode (iss, is) ts +fun split_modeT (iss, is) ts = gen_split_mode split_smodeT (iss, is) ts datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term | Generator of (string * typ); @@ -333,7 +308,7 @@ fun print_modes options modes = if show_modes options then - Output.tracing ("Inferred modes:\n" ^ + tracing ("Inferred modes:\n" ^ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_mode ms)) modes)) else () @@ -344,7 +319,7 @@ ^ (string_of_entry pred mode entry) fun print_pred (pred, modes) = "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes) - val _ = Output.tracing (cat_lines (map print_pred pred_mode_table)) + val _ = tracing (cat_lines (map print_pred pred_mode_table)) in () end; fun string_of_prem thy (Prem (ts, p)) = @@ -423,10 +398,10 @@ case expected_modes options of SOME (s, ms) => (case AList.lookup (op =) modes s of SOME modes => - if not (eq_set (op =) (map (map (rpair NONE)) ms, map snd modes)) then + if not (eq_set (op =) (ms, modes)) then error ("expected modes were not inferred:\n" - ^ "inferred modes for " ^ s ^ ": " - ^ commas (map ((enclose "[" "]") o string_of_smode o snd) modes)) + ^ "inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes) + ^ "\n expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms)) else () | NONE => ()) | NONE => () @@ -661,7 +636,7 @@ fun cons_intro gr = case try (Graph.get_node gr) name of SOME pred_data => Graph.map_node name (map_pred_data - (apfst (fn (intros, elim, nparams) => (thm::intros, elim, nparams)))) gr + (apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr | NONE => let val nparams = the_default (guess_nparams T) (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name) @@ -1052,9 +1027,9 @@ fun print_failed_mode options thy modes p m rs i = if show_mode_inference options then let - val _ = Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ + val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ p ^ " violates mode " ^ string_of_mode m) - val _ = Output.tracing (string_of_clause thy p (nth rs i)) + val _ = tracing (string_of_clause thy p (nth rs i)) in () end else () @@ -1191,6 +1166,28 @@ (t, names) end; +structure Comp_Mod = +struct + +datatype comp_modifiers = Comp_Modifiers of +{ + const_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string, + funT_of : compilation_funs -> mode -> typ -> typ, + additional_arguments : string list -> term list, + wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term, + transform_additional_arguments : indprem -> term list -> term list +} + +fun dest_comp_modifiers (Comp_Modifiers c) = c + +val const_name_of = #const_name_of o dest_comp_modifiers +val funT_of = #funT_of o dest_comp_modifiers +val additional_arguments = #additional_arguments o dest_comp_modifiers +val wrap_compilation = #wrap_compilation o dest_comp_modifiers +val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers + +end; + fun compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss arg = let fun map_params (t as Free (f, T)) = @@ -1198,7 +1195,7 @@ case (the (AList.lookup (op =) (param_vs ~~ iss) f)) of SOME is => let - val T' = #funT_of compilation_modifiers compfuns ([], is) T + val T' = Comp_Mod.funT_of compilation_modifiers compfuns ([], is) T in fst (mk_Eval_of additional_arguments ((Free (f, T'), T), SOME is) []) end | NONE => t else t @@ -1248,9 +1245,9 @@ val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) val f' = case f of - Const (name, T) => Const (#const_name_of compilation_modifiers thy name mode, - #funT_of compilation_modifiers compfuns mode T) - | Free (name, T) => Free (name, #funT_of compilation_modifiers compfuns mode T) + Const (name, T) => Const (Comp_Mod.const_name_of compilation_modifiers thy name mode, + Comp_Mod.funT_of compilation_modifiers compfuns mode T) + | Free (name, T) => Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T) | _ => error ("PredicateCompiler: illegal parameter term") in list_comb (f', params' @ args') @@ -1262,13 +1259,13 @@ let val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*) - val name' = #const_name_of compilation_modifiers thy name mode - val T' = #funT_of compilation_modifiers compfuns mode T + val name' = Comp_Mod.const_name_of compilation_modifiers thy name mode + val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T in (list_comb (Const (name', T'), params' @ inargs @ additional_arguments)) end | (Free (name, T), params) => - list_comb (Free (name, #funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments) + list_comb (Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments) fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments (iss, is) inp (ts, moded_ps) = let @@ -1302,7 +1299,7 @@ val (out_ts'', (names'', constr_vs')) = fold_map distinct_v out_ts' ((names', map (rpair []) vs)) val additional_arguments' = - #transform_additional_arguments compilation_modifiers p additional_arguments + Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments val (compiled_clause, rest) = case p of Prem (us, t) => let @@ -1356,7 +1353,7 @@ val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) val (Us1, Us2) = split_smodeT (snd mode) Ts2 val Ts1' = - map2 (fn NONE => I | SOME is => #funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1 + map2 (fn NONE => I | SOME is => Comp_Mod.funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1 fun mk_input_term (i, NONE) = [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of @@ -1370,17 +1367,17 @@ else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end val in_ts = maps mk_input_term (snd mode) val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1' - val additional_arguments = #additional_arguments compilation_modifiers (all_vs @ param_vs) + val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs) val cl_ts = map (compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls; - val compilation = #wrap_compilation compilation_modifiers compfuns s T mode additional_arguments + val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments (if null cl_ts then mk_bot compfuns (HOLogic.mk_tupleT Us2) else foldr1 (mk_sup compfuns) cl_ts) val fun_const = - Const (#const_name_of compilation_modifiers thy s mode, - #funT_of compilation_modifiers compfuns mode T) + Const (Comp_Mod.const_name_of compilation_modifiers thy s mode, + Comp_Mod.funT_of compilation_modifiers compfuns mode T) in HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (fun_const, params @ in_ts @ additional_arguments), compilation)) @@ -2139,31 +2136,47 @@ (** main function of predicate compiler **) +datatype steps = Steps of + { + compile_preds : theory -> string list -> string list -> (string * typ) list + -> (moded_clause list) pred_mode_table -> term pred_mode_table, + create_definitions: (string * typ) list -> string * mode list -> theory -> theory, + infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list + -> string list -> (string * (term list * indprem list) list) list + -> moded_clause list pred_mode_table, + prove : options -> theory -> (string * (term list * indprem list) list) list + -> (string * typ) list -> (string * mode list) list + -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, + are_not_defined : theory -> string list -> bool, + qname : bstring + } + + fun add_equations_of steps options prednames thy = let + fun dest_steps (Steps s) = s val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") - val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) (*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) val _ = print_step options "Infering modes..." - val moded_clauses = #infer_modes steps options thy extra_modes all_modes param_vs clauses + val moded_clauses = #infer_modes (dest_steps 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 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 + val thy' = fold (#create_definitions (dest_steps steps) preds) modes thy |> Theory.checkpoint val _ = print_step options "Compiling equations..." val compiled_terms = - (#compile_preds steps) thy' all_vs param_vs preds moded_clauses + #compile_preds (dest_steps steps) thy' all_vs param_vs preds moded_clauses val _ = print_compiled_terms options thy' compiled_terms val _ = print_step options "Proving equations..." - val result_thms = #prove steps options thy' clauses preds (extra_modes @ modes) + val result_thms = #prove (dest_steps steps) options thy' clauses preds (extra_modes @ modes) moded_clauses compiled_terms - val qname = #qname steps + val qname = #qname (dest_steps steps) val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)))) val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss @@ -2181,7 +2194,7 @@ SOME v => (G, v) | NONE => (Graph.new_node (key, value_of key) G, value_of key) val (G'', visited') = fold (extend' value_of edges_of) (subtract (op =) visited (edges_of (key, v))) - (G', key :: visited) + (G', key :: visited) in (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited') end; @@ -2190,6 +2203,7 @@ fun gen_add_equations steps options names thy = let + fun dest_steps (Steps s) = s val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy |> Theory.checkpoint; fun strong_conn_of gr keys = @@ -2197,24 +2211,25 @@ val scc = strong_conn_of (PredData.get thy') names val thy'' = fold_rev (fn preds => fn thy => - if #are_not_defined steps thy preds then + if #are_not_defined (dest_steps steps) thy preds then add_equations_of steps options preds thy else thy) scc thy' |> Theory.checkpoint in thy'' end (* different instantiantions of the predicate compiler *) -val predicate_comp_modifiers = - {const_name_of = predfun_name_of, - funT_of = funT_of, +val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers + {const_name_of = predfun_name_of : (theory -> string -> mode -> string), + funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = K [], - wrap_compilation = K (K (K (K (K I)))), - transform_additional_arguments = K I + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) } -val depth_limited_comp_modifiers = +val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers {const_name_of = depth_limited_function_name_of, - funT_of = depth_limited_funT_of, + funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = fn names => let val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"] @@ -2245,38 +2260,38 @@ in [polarity', depth'] end } -val rpred_comp_modifiers = +val rpred_comp_modifiers = Comp_Mod.Comp_Modifiers {const_name_of = generator_name_of, - funT_of = K generator_funT_of, + funT_of = K generator_funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})], - wrap_compilation = K (K (K (K (K I)))), - transform_additional_arguments = K I + wrap_compilation = K (K (K (K (K I)))) + : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), + transform_additional_arguments = K I : (indprem -> term list -> term list) } - val add_equations = gen_add_equations - {infer_modes = infer_modes, + (Steps {infer_modes = infer_modes, create_definitions = create_definitions, compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns, prove = prove, are_not_defined = fn thy => forall (null o modes_of thy), - qname = "equation"} + qname = "equation"}) val add_depth_limited_equations = gen_add_equations - {infer_modes = infer_modes, + (Steps {infer_modes = infer_modes, create_definitions = create_definitions_of_depth_limited_functions, compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, are_not_defined = fn thy => forall (null o depth_limited_modes_of thy), - qname = "depth_limited_equation"} + qname = "depth_limited_equation"}) val add_quickcheck_equations = gen_add_equations - {infer_modes = infer_modes_with_generator, + (Steps {infer_modes = infer_modes_with_generator, create_definitions = rpred_create_definitions, 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"} + qname = "rpred_equation"}) (** user interface **) @@ -2307,7 +2322,7 @@ (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy |> LocalTheory.checkpoint val thy' = ProofContext.theory_of lthy' - val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy') + val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy') fun mk_cases const = let val T = Sign.the_const_type thy const diff -r 6ff4674499ca -r d8bfa9564a52 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Oct 29 13:37:55 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Oct 29 14:03:55 2009 +0100 @@ -45,7 +45,7 @@ unfolding mem_def[symmetric, of _ a2] apply auto unfolding mem_def - apply auto + apply fastsimp done qed diff -r 6ff4674499ca -r d8bfa9564a52 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Oct 29 13:37:55 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Oct 29 14:03:55 2009 +0100 @@ -1,12 +1,12 @@ theory Predicate_Compile_ex -imports Main Predicate_Compile_Alternative_Defs +imports "../Main" Predicate_Compile_Alternative_Defs begin subsection {* Basic predicates *} inductive False' :: "bool" -code_pred (mode: []) False' . +code_pred (mode : []) False' . code_pred [depth_limited] False' . code_pred [rpred] False' . @@ -17,7 +17,7 @@ definition EmptySet' :: "'a \ bool" where "EmptySet' = {}" -code_pred (mode: [], [1]) [inductify, show_intermediate_results] EmptySet' . +code_pred (mode: [], [1]) [inductify] EmptySet' . inductive EmptyRel :: "'a \ 'b \ bool" @@ -26,7 +26,13 @@ inductive EmptyClosure :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r :: "'a \ 'a \ bool" -code_pred (mode: [], [1], [2], [1, 2])EmptyClosure . +code_pred + (mode: [] ==> [], [] ==> [1], [] ==> [2], [] ==> [1, 2], + [1] ==> [], [1] ==> [1], [1] ==> [2], [1] ==> [1, 2], + [2] ==> [], [2] ==> [1], [2] ==> [2], [2] ==> [1, 2], + [1, 2] ==> [], [1, 2] ==> [1], [1, 2] ==> [2], [1, 2] ==> [1, 2]) + EmptyClosure . + thm EmptyClosure.equation (* TODO: inductive package is broken! inductive False'' :: "bool" @@ -60,8 +66,88 @@ where "zerozero (0, 0)" -code_pred zerozero . -code_pred [rpred, show_compilation] zerozero . +code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero . +code_pred [rpred] zerozero . + +subsection {* Alternative Rules *} + +datatype char = C | D | E | F | G | H + +inductive is_C_or_D +where + "(x = C) \ (x = D) ==> is_C_or_D x" + +code_pred (mode: [1]) is_C_or_D . +thm is_C_or_D.equation + +inductive is_D_or_E +where + "(x = D) \ (x = E) ==> is_D_or_E x" + +lemma [code_pred_intros]: + "is_D_or_E D" +by (auto intro: is_D_or_E.intros) + +lemma [code_pred_intros]: + "is_D_or_E E" +by (auto intro: is_D_or_E.intros) + +code_pred (mode: [], [1]) is_D_or_E +proof - + case is_D_or_E + from this(1) show thesis + proof + fix x + assume x: "a1 = x" + assume "x = D \ x = E" + from this show thesis + proof + assume "x = D" from this x is_D_or_E(2) show thesis by simp + next + assume "x = E" from this x is_D_or_E(3) show thesis by simp + qed + qed +qed + +thm is_D_or_E.equation + +inductive is_F_or_G +where + "x = F \ x = G ==> is_F_or_G x" + +lemma [code_pred_intros]: + "is_F_or_G F" +by (auto intro: is_F_or_G.intros) + +lemma [code_pred_intros]: + "is_F_or_G G" +by (auto intro: is_F_or_G.intros) + +inductive is_FGH +where + "is_F_or_G x ==> is_FGH x" +| "is_FGH H" + +text {* Compilation of is_FGH requires elimination rule for is_F_or_G *} + +code_pred (mode: [], [1]) is_FGH +proof - + case is_F_or_G + from this(1) show thesis + proof + fix x + assume x: "a1 = x" + assume "x = F \ x = G" + from this show thesis + proof + assume "x = F" + from this x is_F_or_G(2) show thesis by simp + next + assume "x = G" + from this x is_F_or_G(3) show thesis by simp + qed + qed +qed subsection {* Preprocessor Inlining *} @@ -123,7 +209,7 @@ definition odd' where "odd' x == \ even x" -code_pred [inductify] odd' . +code_pred (mode: [1]) [inductify] odd' . code_pred [inductify, depth_limited] odd' . code_pred [inductify, rpred] odd' . @@ -135,7 +221,7 @@ where "n mod 2 = 0 \ is_even n" -code_pred is_even . +code_pred (mode: [1]) is_even . subsection {* append predicate *} @@ -172,10 +258,19 @@ lemmas [code_pred_intros] = append2_Nil append2.intros(2) -code_pred append2 +code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append2 proof - case append2 - from append2.cases[OF append2(1)] append2(2-3) show thesis by blast + from append2(1) show thesis + proof + fix xs + assume "a1 = []" "a2 = xs" "a3 = xs" + from this append2(2) show thesis by simp + next + fix xs ys zs x + assume "a1 = x # xs" "a2 = ys" "a3 = x # zs" "append2 xs ys zs" + from this append2(3) show thesis by fastsimp + qed qed inductive tupled_append :: "'a list \ 'a list \ 'a list \ bool" @@ -183,7 +278,7 @@ "tupled_append ([], xs, xs)" | "tupled_append (xs, ys, zs) \ tupled_append (x # xs, ys, x # zs)" -code_pred tupled_append . +code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append . code_pred [rpred] tupled_append . thm tupled_append.equation (* @@ -197,7 +292,7 @@ | "[| ys = fst (xa, y); x # zs = snd (xa, y); tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)" -code_pred tupled_append' . +code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append' . thm tupled_append'.equation inductive tupled_append'' :: "'a list \ 'a list \ 'a list \ bool" @@ -205,9 +300,7 @@ "tupled_append'' ([], xs, xs)" | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \ tupled_append'' (x # xs, yszs)" -thm tupled_append''.cases - -code_pred [inductify] tupled_append'' . +code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append'' . thm tupled_append''.equation inductive tupled_append''' :: "'a list \ 'a list \ 'a list \ bool" @@ -215,7 +308,7 @@ "tupled_append''' ([], xs, xs)" | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" -code_pred [inductify] tupled_append''' . +code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append''' . thm tupled_append'''.equation subsection {* map_ofP predicate *} @@ -237,7 +330,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: [1], [1, 2]) filter1 . +code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 . code_pred [depth_limited] filter1 . code_pred [rpred] filter1 . @@ -260,7 +353,7 @@ where "List.filter P xs = ys ==> filter3 P xs ys" -code_pred filter3 . +code_pred (mode: [] ==> [1], [] ==> [1, 2], [1] ==> [1], [1] ==> [1, 2]) filter3 . code_pred [depth_limited] filter3 . thm filter3.depth_limited_equation @@ -268,7 +361,7 @@ where "List.filter P xs = ys ==> filter4 P xs ys" -code_pred filter4 . +code_pred (mode: [1, 2], [1, 2, 3]) filter4 . code_pred [depth_limited] filter4 . code_pred [rpred] filter4 . @@ -288,7 +381,7 @@ "tupled_rev ([], [])" | "tupled_rev (xs, xs') \ tupled_append (xs', [x], ys) \ tupled_rev (x#xs, ys)" -code_pred tupled_rev . +code_pred (mode: [(i, o)], [(o, i)], [i]) tupled_rev . thm tupled_rev.equation subsection {* partition predicate *} @@ -299,7 +392,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: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition . +code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition . code_pred [depth_limited] partition . code_pred [rpred] partition . @@ -314,7 +407,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 tupled_partition . +code_pred (mode: [i] ==> [i], [i] ==> [(i, i, o)], [i] ==> [(i, o, i)], [i] ==> [(o, i, i)], [i] ==> [(i, o, o)]) tupled_partition . thm tupled_partition.equation @@ -325,7 +418,7 @@ subsection {* transitive predicate *} -code_pred tranclp +code_pred (mode: [1] ==> [1, 2], [1] ==> [1], [2] ==> [1, 2], [2] ==> [2], [] ==> [1, 2], [] ==> [1], [] ==> [2], [] ==> []) tranclp proof - case tranclp from this converse_tranclpE[OF this(1)] show thesis by metis @@ -658,6 +751,8 @@ | "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: [], [1]) S\<^isub>4p . + subsection {* Lambda *} datatype type = @@ -708,4 +803,10 @@ | 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: [1, 2], [1, 2, 3]) typing . +thm typing.equation + +code_pred (mode: [1], [1, 2]) beta . +thm beta.equation + end \ No newline at end of file