--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Oct 01 08:25:23 2010 +0200
@@ -12,6 +12,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -25,6 +26,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -34,6 +36,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -202,6 +205,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Fri Oct 01 08:25:23 2010 +0200
@@ -58,6 +58,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s1", "a1", "b1"], 2)],
replacing = [(("s1", "limited_s1"), "quickcheck")],
@@ -81,6 +82,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s2", "a2", "b2"], 3)],
replacing = [(("s2", "limited_s2"), "quickcheck")],
@@ -103,6 +105,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s3", "a3", "b3"], 6)],
replacing = [(("s3", "limited_s3"), "quickcheck")],
@@ -117,6 +120,7 @@
(*
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -143,6 +147,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s4", "a4", "b4"], 6)],
replacing = [(("s4", "limited_s4"), "quickcheck")],
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Fri Oct 01 08:25:23 2010 +0200
@@ -86,6 +86,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -97,7 +98,7 @@
setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[generator = code, iterations = 100000, report]
+(*quickcheck[generator = code, iterations = 100000, report]*)
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
@@ -112,8 +113,24 @@
s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+section {* Manual setup to find the counterexample *}
+
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["hotel"], 4)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+ manual_reorder = []}) *}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["hotel"], 5)],
replacing = [(("hotel", "limited_hotel"), "quickcheck")],
@@ -124,4 +141,75 @@
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
+section {* Simulating a global depth limit manually by limiting all predicates *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+ "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+ "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+section {* Using a global limit for limiting the execution *}
+
+text {* A global depth limit of 13 does not suffice to find the counterexample. *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = SOME 13,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+text {* But a global depth limit of 14 does. *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = SOME 14,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Fri Oct 01 08:25:23 2010 +0200
@@ -83,6 +83,7 @@
setup {* Code_Prolog.map_code_options (K
{ ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
replacing = [(("typing", "limited_typing"), "quickcheck"),
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Oct 01 08:25:23 2010 +0200
@@ -6,6 +6,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
limited_predicates = [(["appendP"], 4), (["revP"], 4)],
replacing =
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri Oct 01 08:25:23 2010 +0200
@@ -1538,5 +1538,11 @@
code_pred implies_itself .
+text {* Case expressions *}
+
+definition
+ "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
+
+code_pred [inductify] map_pairs .
end
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Oct 01 08:25:23 2010 +0200
@@ -100,6 +100,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
(["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Oct 01 08:25:23 2010 +0200
@@ -9,6 +9,7 @@
datatype prolog_system = SWI_PROLOG | YAP
type code_options =
{ensure_groundness : bool,
+ limit_globally : int option,
limited_types : (typ * int) list,
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
@@ -58,38 +59,45 @@
type code_options =
{ensure_groundness : bool,
+ limit_globally : int option,
limited_types : (typ * int) list,
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
manual_reorder : ((string * int) * int list) list}
-fun set_ensure_groundness {ensure_groundness, limited_types, limited_predicates,
+fun set_ensure_groundness {ensure_groundness, limit_globally, limited_types, limited_predicates,
replacing, manual_reorder} =
- {ensure_groundness = true, limited_types = limited_types,
+ {ensure_groundness = true, limit_globally = limit_globally, limited_types = limited_types,
limited_predicates = limited_predicates, replacing = replacing,
manual_reorder = manual_reorder}
-fun map_limit_predicates f {ensure_groundness, limited_types, limited_predicates,
+fun map_limit_predicates f {ensure_groundness, limit_globally, limited_types, limited_predicates,
replacing, manual_reorder} =
- {ensure_groundness = ensure_groundness, limited_types = limited_types,
+ {ensure_groundness = ensure_groundness, limit_globally = limit_globally, limited_types = limited_types,
limited_predicates = f limited_predicates, replacing = replacing,
manual_reorder = manual_reorder}
-
+
+fun merge_global_limit (NONE, NONE) = NONE
+ | merge_global_limit (NONE, SOME n) = SOME n
+ | merge_global_limit (SOME n, NONE) = SOME n
+ | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))
+
structure Options = Theory_Data
(
type T = code_options
- val empty = {ensure_groundness = false,
+ val empty = {ensure_groundness = false, limit_globally = NONE,
limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []}
val extend = I;
fun merge
- ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
- limited_predicates = limited_predicates1, replacing = replacing1,
- manual_reorder = manual_reorder1},
- {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
- limited_predicates = limited_predicates2, replacing = replacing2,
- manual_reorder = manual_reorder2}) =
+ ({ensure_groundness = ensure_groundness1, limit_globally = limit_globally1,
+ limited_types = limited_types1, limited_predicates = limited_predicates1,
+ replacing = replacing1, manual_reorder = manual_reorder1},
+ {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2,
+ limited_types = limited_types2, limited_predicates = limited_predicates2,
+ replacing = replacing2, manual_reorder = manual_reorder2}) =
{ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+ limit_globally = merge_global_limit (limit_globally1, limit_globally2),
limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2),
@@ -188,7 +196,7 @@
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
-
+
(* translation from introduction rules to internal representation *)
fun mk_conform f empty avoid name =
@@ -591,13 +599,14 @@
((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem)
end
-fun add_limited_predicates limited_predicates =
+fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
+
+fun add_limited_predicates limited_predicates (p, constant_table) =
let
- fun add (rel_names, limit) (p, constant_table) =
+ fun add (rel_names, limit) p =
let
val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
val clauses' = map (mk_depth_limited rel_names) clauses
- fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
fun mk_entry_clause rel_name =
let
val nargs = length (snd (fst
@@ -606,9 +615,9 @@
in
(("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
end
- in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end
+ in (p @ (map mk_entry_clause rel_names) @ clauses') end
in
- fold add limited_predicates
+ (fold add limited_predicates p, constant_table)
end
@@ -663,10 +672,29 @@
val rename_vars_program = map rename_vars_clause
+(* limit computation globally by some threshold *)
+
+fun limit_globally ctxt limit const_name (p, constant_table) =
+ let
+ val rel_names = fold (fn ((r, _), _) => insert (op =) r) p []
+ val p' = map (mk_depth_limited rel_names) p
+ val rel_name = translate_const constant_table const_name
+ val nargs = length (snd (fst
+ (the (find_first (fn ((rel, _), _) => rel = rel_name) p))))
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
+ val entry_clause = ((rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
+ val p'' = filter_out (fn ((rel, _), _) => rel = rel_name) p
+ in
+ (entry_clause :: p' @ p'', constant_table)
+ end
+
(* post processing of generated prolog program *)
-fun post_process ctxt options (p, constant_table) =
+fun post_process ctxt options const_name (p, constant_table) =
(p, constant_table)
+ |> (case #limit_globally options of
+ SOME limit => limit_globally ctxt limit const_name
+ | NONE => I)
|> (if #ensure_groundness options then
add_ground_predicates ctxt (#limited_types options)
else I)
@@ -915,7 +943,7 @@
val ctxt' = ProofContext.init_global thy'
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
- |> post_process ctxt' options
+ |> post_process ctxt' options name
val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table
val args' = map (translate_term ctxt constant_table') all_args
val _ = tracing "Running prolog program..."
@@ -991,7 +1019,7 @@
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, true) ctxt' full_constname
- |> post_process ctxt' (set_ensure_groundness options)
+ |> post_process ctxt' (set_ensure_groundness options) full_constname
val _ = tracing "Running prolog program..."
val system_config = System_Config.get (Context.Proof ctxt)
val tss = run (#timeout system_config, #prolog_system system_config)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Oct 01 08:25:23 2010 +0200
@@ -147,6 +147,7 @@
(* simple transformations *)
val split_conjuncts_in_assms : Proof.context -> thm -> thm
val expand_tuples : theory -> thm -> thm
+ val case_betapply : theory -> term -> term
val eta_contract_ho_arguments : theory -> thm -> thm
val remove_equalities : theory -> thm -> thm
val remove_pointless_clauses : thm -> thm list
@@ -859,6 +860,85 @@
intro'''''
end
+(** making case distributivity rules **)
+(*** this should be part of the datatype package ***)
+
+fun datatype_names_of_case_name thy case_name =
+ map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
+
+fun make_case_distribs new_type_names descr sorts thy =
+ let
+ val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
+ fun make comb =
+ let
+ val Type ("fun", [T, T']) = fastype_of comb;
+ val (Const (case_name, _), fs) = strip_comb comb
+ val used = Term.add_tfree_names comb []
+ val U = TFree (Name.variant used "'t", HOLogic.typeS)
+ val x = Free ("x", T)
+ val f = Free ("f", T' --> U)
+ fun apply_f f' =
+ let
+ val Ts = binder_types (fastype_of f')
+ val bs = map Bound ((length Ts - 1) downto 0)
+ in
+ fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
+ end
+ val fs' = map apply_f fs
+ val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
+ in
+ HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
+ end
+ in
+ map make case_combs
+ end
+
+fun case_rewrites thy Tcon =
+ let
+ val info = Datatype.the_info thy Tcon
+ val descr = #descr info
+ val sorts = #sorts info
+ val typ_names = the_default [Tcon] (#alt_names info)
+ in
+ map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
+ (make_case_distribs typ_names [descr] sorts thy)
+ end
+
+fun instantiated_case_rewrites thy Tcon =
+ let
+ val rew_ths = case_rewrites thy Tcon
+ val ctxt = ProofContext.init_global thy
+ fun instantiate th =
+ let
+ val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
+ val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
+ val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
+ val T = TFree (tname, HOLogic.typeS)
+ val T' = TFree (tname', HOLogic.typeS)
+ val U = TFree (uname, HOLogic.typeS)
+ val y = Free (yname, U)
+ val f' = absdummy (U --> T', Bound 0 $ y)
+ val th' = Thm.certify_instantiate
+ ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
+ [((fst (dest_Var f), (U --> T') --> T'), f')]) th
+ val [th'] = Variable.export ctxt' ctxt [th']
+ in
+ th'
+ end
+ in
+ map instantiate rew_ths
+ end
+
+fun case_betapply thy t =
+ let
+ val case_name = fst (dest_Const (fst (strip_comb t)))
+ val Tcons = datatype_names_of_case_name thy case_name
+ val ths = maps (instantiated_case_rewrites thy) Tcons
+ in
+ MetaSimplifier.rewrite_term thy
+ (map (fn th => th RS @{thm eq_reflection}) ths) [] t
+ end
+
(*** conversions ***)
fun imp_prems_conv cv ct =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Oct 01 08:25:23 2010 +0200
@@ -185,10 +185,9 @@
val (f, args) = strip_comb t
val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
- val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
- val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
- val (_, split_args) = strip_comb split_t
- val match = split_args ~~ args
+ val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val t' = case_betapply thy t
+ val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
fun flatten_of_assm assm =
let
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Oct 01 08:25:23 2010 +0200
@@ -19,73 +19,6 @@
open Predicate_Compile_Aux
-
-fun datatype_names_of_case_name thy case_name =
- map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
-
-fun make_case_distribs new_type_names descr sorts thy =
- let
- val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
- fun make comb =
- let
- val Type ("fun", [T, T']) = fastype_of comb;
- val (Const (case_name, _), fs) = strip_comb comb
- val used = Term.add_tfree_names comb []
- val U = TFree (Name.variant used "'t", HOLogic.typeS)
- val x = Free ("x", T)
- val f = Free ("f", T' --> U)
- fun apply_f f' =
- let
- val Ts = binder_types (fastype_of f')
- val bs = map Bound ((length Ts - 1) downto 0)
- in
- fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
- end
- val fs' = map apply_f fs
- val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
- in
- HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
- end
- in
- map make case_combs
- end
-
-fun case_rewrites thy Tcon =
- let
- val info = Datatype.the_info thy Tcon
- val descr = #descr info
- val sorts = #sorts info
- val typ_names = the_default [Tcon] (#alt_names info)
- in
- map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
- (make_case_distribs typ_names [descr] sorts thy)
- end
-
-fun instantiated_case_rewrites thy Tcon =
- let
- val rew_ths = case_rewrites thy Tcon
- val ctxt = ProofContext.init_global thy
- fun instantiate th =
- let
- val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
- val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
- val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
- val T = TFree (tname, HOLogic.typeS)
- val T' = TFree (tname', HOLogic.typeS)
- val U = TFree (uname, HOLogic.typeS)
- val y = Free (yname, U)
- val f' = absdummy (U --> T', Bound 0 $ y)
- val th' = Thm.certify_instantiate
- ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
- [((fst (dest_Var f), (U --> T') --> T'), f')]) th
- val [th'] = Variable.export ctxt' ctxt [th']
- in
- th'
- end
- in
- map instantiate rew_ths
- end
-
fun is_compound ((Const (@{const_name Not}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
| is_compound ((Const (@{const_name Ex}, _)) $ _) = true
@@ -99,17 +32,13 @@
NONE => NONE
| SOME raw_split_thm =>
let
- val case_name = fst (dest_Const (fst (strip_comb atom)))
val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
(* TODO: contextify things - this line is to unvarify the split_thm *)
(*val ((_, [isplit_thm]), _) =
Variable.import true [split_thm] (ProofContext.init_global thy)*)
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
- val Tcons = datatype_names_of_case_name thy case_name
- val ths = maps (instantiated_case_rewrites thy) Tcons
- val atom' = MetaSimplifier.rewrite_term thy
- (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
+ val atom' = case_betapply thy atom
val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
val names' = Term.add_free_names atom' names
fun mk_subst_rhs assm =
--- a/src/HOLCF/Cfun.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOLCF/Cfun.thy Fri Oct 01 08:25:23 2010 +0200
@@ -373,13 +373,7 @@
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
-proof (rule cont2cont_LAM)
- fix x :: 'a show "cont (\<lambda>y. f x y)"
- using f by (rule cont_fst_snd_D2)
-next
- fix y :: 'b show "cont (\<lambda>x. f x y)"
- using f by (rule cont_fst_snd_D1)
-qed
+using assms by (simp add: cont2cont_LAM prod_cont_iff)
lemma cont2cont_LAM_discrete [simp, cont2cont]:
"(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
--- a/src/HOLCF/Fixrec.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOLCF/Fixrec.thy Fri Oct 01 08:25:23 2010 +0200
@@ -118,9 +118,9 @@
"match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
definition
- match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
+ match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
where
- "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
+ "match_Pair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
definition
match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
@@ -162,9 +162,9 @@
"x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
by (simp_all add: match_UU_def)
-lemma match_cpair_simps [simp]:
- "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
-by (simp_all add: match_cpair_def)
+lemma match_Pair_simps [simp]:
+ "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
+by (simp_all add: match_Pair_def)
lemma match_spair_simps [simp]:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
@@ -248,7 +248,7 @@
(@{const_name sinl}, @{const_name match_sinl}),
(@{const_name sinr}, @{const_name match_sinr}),
(@{const_name spair}, @{const_name match_spair}),
- (@{const_name Pair}, @{const_name match_cpair}),
+ (@{const_name Pair}, @{const_name match_Pair}),
(@{const_name ONE}, @{const_name match_ONE}),
(@{const_name TT}, @{const_name match_TT}),
(@{const_name FF}, @{const_name match_FF}),
--- a/src/HOLCF/Library/List_Cpo.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOLCF/Library/List_Cpo.thy Fri Oct 01 08:25:23 2010 +0200
@@ -185,14 +185,7 @@
assumes g: "cont (\<lambda>x. g x)"
assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
-proof -
- have "\<And>y ys. cont (\<lambda>x. h x (fst (y, ys)) (snd (y, ys)))"
- by (rule h [THEN cont_fst_snd_D1])
- hence h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" by simp
- note h2 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
- note h3 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
- from f g h1 h2 h3 show ?thesis by (rule cont2cont_list_case)
-qed
+using assms by (simp add: cont2cont_list_case prod_cont_iff)
text {* The simple version (due to Joachim Breitner) is needed if the
element type of the list is not a cpo. *}
--- a/src/HOLCF/Library/Sum_Cpo.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOLCF/Library/Sum_Cpo.thy Fri Oct 01 08:25:23 2010 +0200
@@ -173,17 +173,7 @@
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
assumes h: "cont (\<lambda>x. h x)"
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-proof -
- note f1 = f [THEN cont_fst_snd_D1]
- note f2 = f [THEN cont_fst_snd_D2]
- note g1 = g [THEN cont_fst_snd_D1]
- note g2 = g [THEN cont_fst_snd_D2]
- show ?thesis
- apply (rule cont_apply [OF h])
- apply (rule cont_sum_case2 [OF f2 g2])
- apply (rule cont_sum_case1 [OF f1 g1])
- done
-qed
+using assms by (simp add: cont2cont_sum_case prod_cont_iff)
subsection {* Compactness and chain-finiteness *}
--- a/src/HOLCF/Product_Cpo.thy Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOLCF/Product_Cpo.thy Fri Oct 01 08:25:23 2010 +0200
@@ -234,7 +234,7 @@
lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
-lemma cont2cont_split:
+lemma cont2cont_prod_case:
assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
@@ -248,6 +248,25 @@
apply (rule f1)
done
+lemma prod_contI:
+ assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
+ assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
+ shows "cont f"
+proof -
+ have "cont (\<lambda>(x, y). f (x, y))"
+ by (intro cont2cont_prod_case f1 f2 cont2cont)
+ thus "cont f"
+ by (simp only: split_eta)
+qed
+
+lemma prod_cont_iff:
+ "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
+apply safe
+apply (erule cont_compose [OF _ cont_pair1])
+apply (erule cont_compose [OF _ cont_pair2])
+apply (simp only: prod_contI)
+done
+
lemma cont_fst_snd_D1:
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
by (drule cont_compose [OF _ cont_pair1], simp)
@@ -256,23 +275,11 @@
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
by (drule cont_compose [OF _ cont_pair2], simp)
-lemma cont2cont_split' [simp, cont2cont]:
+lemma cont2cont_prod_case' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
assumes g: "cont (\<lambda>x. g x)"
- shows "cont (\<lambda>x. split (f x) (g x))"
-proof -
- note f1 = f [THEN cont_fst_snd_D1]
- note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
- note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
- show ?thesis
- unfolding split_def
- apply (rule cont_apply [OF g])
- apply (rule cont_apply [OF cont_fst f2])
- apply (rule cont_apply [OF cont_snd f3])
- apply (rule cont_const)
- apply (rule f1)
- done
-qed
+ shows "cont (\<lambda>x. prod_case (f x) (g x))"
+using assms by (simp add: cont2cont_prod_case prod_cont_iff)
text {* The simple version (due to Joachim Breitner) is needed if
either element type of the pair is not a cpo. *}
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 01 08:25:23 2010 +0200
@@ -36,7 +36,7 @@
val beta_rules =
@{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
- @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_split'};
+ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'};
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
--- a/src/HOLCF/Tools/fixrec.ML Thu Sep 30 18:37:29 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Fri Oct 01 08:25:23 2010 +0200
@@ -10,8 +10,6 @@
-> (Attrib.binding * term) list -> local_theory -> local_theory
val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
-> (Attrib.binding * string) list -> local_theory -> local_theory
- val add_fixpat: Thm.binding * term list -> theory -> theory
- val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
val add_matchers: (string * string) list -> theory -> theory
val fixrec_simp_tac: Proof.context -> int -> tactic
val setup: theory -> theory
@@ -218,43 +216,43 @@
taken (t, [])
end;
-(* builds a monadic term for matching a constructor pattern *)
-fun pre_build match_name pat rhs vs taken =
- case pat of
- Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
- pre_build match_name f rhs (v::vs) taken
- | Const(@{const_name Rep_CFun},_)$f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in pre_build match_name f rhs' (v::vs) taken' end
- | f$(v as Free(n,T)) =>
- pre_build match_name f rhs (v::vs) taken
- | f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in pre_build match_name f rhs' (v::vs) taken' end
- | Const(c,T) =>
- let
- val n = Name.variant taken "v";
- fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
- | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
- | result_type T _ = T;
- val v = Free(n, result_type T vs);
- val m = Const(match_name c, matcherT (T, fastype_of rhs));
- val k = big_lambdas vs rhs;
- in
- (m`v`k, v, n::taken)
- end
- | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
- | _ => fixrec_err "pre_build: invalid pattern";
+(* builds a monadic term for matching a pattern *)
+(* returns (rhs, free variable, used varnames) *)
+fun compile_pat match_name pat rhs taken =
+ let
+ fun comp_pat p rhs taken =
+ if is_Free p then (rhs, p, taken)
+ else comp_con (fastype_of p) p rhs [] taken
+ (* compiles a monadic term for a constructor pattern *)
+ and comp_con T p rhs vs taken =
+ case p of
+ Const(@{const_name Rep_CFun},_) $ f $ x =>
+ let val (rhs', v, taken') = comp_pat x rhs taken
+ in comp_con T f rhs' (v::vs) taken' end
+ | f $ x =>
+ let val (rhs', v, taken') = comp_pat x rhs taken
+ in comp_con T f rhs' (v::vs) taken' end
+ | Const (c, cT) =>
+ let
+ val n = Name.variant taken "v"
+ val v = Free(n, T)
+ val m = Const(match_name c, matcherT (cT, fastype_of rhs))
+ val k = big_lambdas vs rhs
+ in
+ (m`v`k, v, n::taken)
+ end
+ | _ => raise TERM ("fixrec: invalid pattern ", [p])
+ in
+ comp_pat pat rhs taken
+ end;
(* builds a monadic term for matching a function definition pattern *)
(* returns (name, arity, matcher) *)
-fun building match_name pat rhs vs taken =
+fun compile_lhs match_name pat rhs vs taken =
case pat of
- Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
- building match_name f rhs (v::vs) taken
- | Const(@{const_name Rep_CFun}, _)$f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in building match_name f rhs' (v::vs) taken' end
+ Const(@{const_name Rep_CFun}, _) $ f $ x =>
+ let val (rhs', v, taken') = compile_pat match_name x rhs taken;
+ in compile_lhs match_name f rhs' (v::vs) taken' end
| Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
| Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
| _ => fixrec_err ("function is not declared as constant in theory: "
@@ -263,11 +261,11 @@
fun strip_alls t =
if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
-fun match_eq match_name eq =
+fun compile_eq match_name eq =
let
val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
in
- building match_name lhs (mk_succeed rhs) [] (taken_names eq)
+ compile_lhs match_name lhs (mk_succeed rhs) [] (taken_names eq)
end;
(* returns the sum (using +++) of the terms in ms *)
@@ -290,10 +288,10 @@
end;
(* this is the pattern-matching compiler function *)
-fun compile_pats match_name eqs =
+fun compile_eqs match_name eqs =
let
val ((names, arities), mats) =
- apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
+ apfst ListPair.unzip (ListPair.unzip (map (compile_eq match_name) eqs));
val cname =
case distinct (op =) names of
[n] => n
@@ -379,7 +377,7 @@
case Symtab.lookup matcher_tab c of SOME m => m
| NONE => fixrec_err ("unknown pattern constructor: " ^ c);
- val matches = map (compile_pats match_name) (map (map snd) blocks);
+ val matches = map (compile_eqs match_name) (map (map snd) blocks);
val spec' = map (pair Attrib.empty_binding) matches;
val (lthy, cnames, fixdef_thms, unfold_thms) =
add_fixdefs fixes spec' lthy;
@@ -409,34 +407,6 @@
end; (* local *)
-(*************************************************************************)
-(******************************** Fixpat *********************************)
-(*************************************************************************)
-
-fun fix_pat thy t =
- let
- val T = fastype_of t;
- val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
- val cname = case chead_of t of Const(c,_) => c | _ =>
- fixrec_err "function is not declared as constant in theory";
- val unfold_thm = Global_Theory.get_thm thy (cname^".unfold");
- val simp = Goal.prove_global thy [] [] eq
- (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
- in simp end;
-
-fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
- let
- val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead";
- val atts = map (prep_attrib thy) srcs;
- val ts = map (prep_term thy) strings;
- val simps = map (fix_pat thy) ts;
- in
- (snd o Global_Theory.add_thmss [((name, simps), atts)]) thy
- end;
-
-val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
-val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
-
(*************************************************************************)
(******************************** Parsers ********************************)
@@ -447,10 +417,6 @@
((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
>> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-val _ =
- Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
- (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
-
val setup =
Method.setup @{binding fixrec_simp}
(Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))