--- 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
--- 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,
--- 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
--- 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
--- 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 \<Rightarrow> bool"
where "EmptySet' = {}"
-code_pred (mode: [], [1]) [inductify, show_intermediate_results] EmptySet' .
+code_pred (mode: [], [1]) [inductify] EmptySet' .
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
@@ -26,7 +26,13 @@
inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
for r :: "'a \<Rightarrow> 'a \<Rightarrow> 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) \<or> (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) \<or> (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 \<or> 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 \<or> 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 \<or> 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 == \<not> 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 \<Longrightarrow> 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 \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -183,7 +278,7 @@
"tupled_append ([], xs, xs)"
| "tupled_append (xs, ys, zs) \<Longrightarrow> 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 \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -205,9 +300,7 @@
"tupled_append'' ([], xs, xs)"
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> 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 \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -215,7 +308,7 @@
"tupled_append''' ([], xs, xs)"
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> 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)"
| "\<not> 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') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> 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 \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> 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 \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
| "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> 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 \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
+code_pred (mode: [], [1]) S\<^isub>4p .
+
subsection {* Lambda *}
datatype type =
@@ -708,4 +803,10 @@
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> 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