--- a/CONTRIBUTORS Fri Sep 21 11:42:14 2012 +0200
+++ b/CONTRIBUTORS Fri Sep 21 11:47:16 2012 +0200
@@ -26,6 +26,8 @@
* June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
Simproc for rewriting set comprehensions into pointfree expressions.
+* May 2012: Andreas Lochbihler, KIT
+ Theory of almost everywhere constant functions.
Contributions to Isabelle2012
-----------------------------
--- a/NEWS Fri Sep 21 11:42:14 2012 +0200
+++ b/NEWS Fri Sep 21 11:47:16 2012 +0200
@@ -109,6 +109,13 @@
* Library/Debug.thy and Library/Parallel.thy: debugging and parallel
execution for code generated towards Isabelle/ML.
+* Library/FinFun.thy: theory of almost everywhere constant functions
+(supersedes the AFP entry "Code Generation for Functions as Data").
+
+* Library/Phantom.thy: generic phantom type to make a type parameter
+appear in a constant's type. This alternative to adding TYPE('a) as
+another parameter avoids unnecessary closures in generated code.
+
* Simproc "finite_Collect" rewrites set comprehensions into pointfree
expressions.
--- a/src/HOL/Codatatype/BNF_Wrap.thy Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Wrap.thy Fri Sep 21 11:47:16 2012 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Codatatype/BNF_Wrap.thy
- Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
Copyright 2012
Wrapping datatypes.
@@ -17,6 +17,11 @@
lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
by (erule iffI) (erule contrapos_pn)
+lemma iff_contradict:
+"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
+"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
+by blast+
+
ML_file "Tools/bnf_wrap_tactics.ML"
ML_file "Tools/bnf_wrap.ML"
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 11:47:16 2012 +0200
@@ -56,7 +56,6 @@
val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
val ordIso_transitive = @{thm ordIso_transitive};
val ordLeq_csum2 = @{thm ordLeq_csum2};
-val set_mp = @{thm set_mp};
val subset_UNIV = @{thm subset_UNIV};
val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
val trans_o_apply = @{thm trans[OF o_apply]};
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 11:47:16 2012 +0200
@@ -77,7 +77,6 @@
val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
val wits_of_bnf: BNF -> nonemptiness_witness list
- val no_reflexive: thm list -> thm list
val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
@@ -513,13 +512,6 @@
val smart_max_inline_size = 25; (*FUDGE*)
-fun is_refl thm =
- op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm)))
- handle TERM _ => false;
-
-val no_refl = filter_out is_refl;
-val no_reflexive = filter_out Thm.is_reflexive;
-
(* Define new BNFs *)
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 11:47:16 2012 +0200
@@ -33,8 +33,6 @@
open BNF_Util
open BNF_Tactics
-val set_mp = @{thm set_mp};
-
fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
@@ -75,9 +73,9 @@
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac map_cong,
REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
@@ -89,7 +87,7 @@
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
stac @{thm fst_conv}, atac]) set_naturals,
rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
@@ -99,7 +97,7 @@
rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
rtac @{thm relcompI}, rtac @{thm converseI},
REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
+ rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, etac sym,
etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
end;
@@ -128,11 +126,11 @@
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
+ rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
rtac map_cong, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp RS sym), rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
@@ -155,32 +153,32 @@
else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
REPEAT_DETERM_N n o rtac @{thm fst_fstO},
in_tac @{thm fstO_in},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac map_cong,
REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
etac set_mp, atac],
in_tac @{thm fstO_in},
rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac map_cong,
REPEAT_DETERM_N n o rtac o_apply,
in_tac @{thm sndO_in},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
REPEAT_DETERM_N n o rtac @{thm snd_sndO},
in_tac @{thm sndO_in},
rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE, hyp_subst_tac,
rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
@@ -188,7 +186,7 @@
REPEAT_DETERM o eresolve_tac [bexE, conjE],
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
+ rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
end;
--- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 11:47:16 2012 +0200
@@ -22,7 +22,9 @@
val coitersN: string
val corecN: string
val corecsN: string
+ val disc_coiter_iffN: string
val disc_coitersN: string
+ val disc_corec_iffN: string
val disc_corecsN: string
val exhaustN: string
val fldN: string
@@ -237,6 +239,9 @@
val discN = "disc"
val disc_coitersN = discN ^ "_" ^ coitersN
val disc_corecsN = discN ^ "_" ^ corecsN
+val iffN = "_iff"
+val disc_coiter_iffN = discN ^ "_" ^ coiterN ^ iffN
+val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
val selN = "sel"
val sel_coitersN = selN ^ "_" ^ coitersN
val sel_corecsN = selN ^ "_" ^ corecsN
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 11:47:16 2012 +0200
@@ -66,6 +66,10 @@
fun merge_type_args (As, As') =
if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
+fun is_triv_implies thm =
+ op aconv (Logic.dest_implies (Thm.prop_of thm))
+ handle TERM _ => false;
+
fun type_args_constrained_of (((cAs, _), _), _) = cAs;
fun type_binding_of (((_, b), _), _) = b;
fun mixfix_of ((_, mx), _) = mx;
@@ -81,6 +85,7 @@
no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
+ (* TODO: integration with function package ("size") *)
val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
else ();
@@ -222,8 +227,9 @@
val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1)));
val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
- val ((iter_only as (gss, _, _), rec_only as (hss, _, _)),
- (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))) =
+ val (((iter_only as (gss, _, _), rec_only as (hss, _, _)),
+ (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
+ names_lthy) =
if lfp then
let
val y_Tsss =
@@ -231,7 +237,7 @@
ns mss fp_iter_fun_Ts;
val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css;
- val ((gss, ysss), _) =
+ val ((gss, ysss), lthy) =
lthy
|> mk_Freess "f" g_Tss
||>> mk_Freesss "x" y_Tsss;
@@ -248,13 +254,13 @@
val hss = map2 (map2 retype_free) h_Tss gss;
val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss;
- val (zssss_tl, _) =
+ val (zssss_tl, lthy) =
lthy
|> mk_Freessss "y" (map (map (map tl)) z_Tssss);
val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
in
- (((gss, g_Tss, yssss), (hss, h_Tss, zssss)),
- ([], [], [], (([], []), ([], [])), (([], []), ([], []))))
+ ((((gss, g_Tss, yssss), (hss, h_Tss, zssss)),
+ ([], [], [], (([], []), ([], [])), (([], []), ([], [])))), lthy)
end
else
let
@@ -283,7 +289,7 @@
val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts;
- val ((((Free (z, _), cs), pss), gssss), _) =
+ val ((((Free (z, _), cs), pss), gssss), lthy) =
lthy
|> yield_singleton (mk_Frees "z") dummyT
||>> mk_Frees "a" Cs
@@ -298,7 +304,7 @@
val (s_Tssss, h_sum_prod_Ts, h_Tssss, ph_Tss) = mk_types dest_corec_sumT fp_rec_fun_Ts;
val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss;
- val ((sssss, hssss_tl), _) =
+ val ((sssss, hssss_tl), lthy) =
lthy
|> mk_Freessss "q" s_Tssss
||>> mk_Freessss "h" (map (map (map tl)) h_Tssss);
@@ -318,9 +324,9 @@
val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss;
in (pfss, cqfsss) end;
in
- ((([], [], []), ([], [], [])),
- ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)),
- (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
+ (((([], [], []), ([], [], [])),
+ ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)),
+ (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
end;
fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
@@ -512,13 +518,13 @@
val args = map build_arg TUs;
in Term.list_comb (mapx, args) end;
+ val mk_simp_thmss =
+ map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn iter_likes =>
+ injects @ distincts @ cases @ rec_likes @ iter_likes);
+
fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
iter_defs, rec_defs), lthy) =
let
- val inject_thmss = map #2 wrap_ress;
- val distinct_thmss = map #3 wrap_ress;
- val case_thmss = map #4 wrap_ress;
-
val (((phis, phis'), vs'), names_lthy) =
lthy
|> mk_Frees' "P" (map mk_pred1T fpTs)
@@ -589,8 +595,7 @@
val goal =
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 (curry (op $)) phis vs)));
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis vs)));
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
@@ -614,7 +619,7 @@
val giters = map (lists_bmoc gss) iters;
val hrecs = map (lists_bmoc hss) recs;
- fun mk_iter_like_goal fss fiter_like xctr f xs fxs =
+ fun mk_goal fss fiter_like xctr f xs fxs =
fold_rev (fold_rev Logic.all) (xs :: fss)
(mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
@@ -640,8 +645,8 @@
val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss;
val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
- val iterss_goal = map5 (map4 o mk_iter_like_goal gss) giters xctrss gss xsss gxsss;
- val recss_goal = map5 (map4 o mk_iter_like_goal hss) hrecs xctrss hss xsss hxsss;
+ val iter_goalss = map5 (map4 o mk_goal gss) giters xctrss gss xsss gxsss;
+ val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
val iter_tacss =
map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
@@ -649,31 +654,29 @@
val rec_tacss =
map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
ctr_defss;
+
+ fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
in
- (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
- iterss_goal iter_tacss,
- map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
- recss_goal rec_tacss)
+ (map2 (map2 prove) iter_goalss iter_tacss,
+ map2 (map2 prove) rec_goalss rec_tacss)
end;
- val simp_thmss =
- map4 (fn injects => fn distincts => fn cases => fn recs =>
- injects @ distincts @ cases @ recs) inject_thmss distinct_thmss case_thmss rec_thmss;
+ val simp_thmss = mk_simp_thmss wrap_ress rec_thmss iter_thmss;
val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
(* TODO: Also note "recs", "simps", and "splits" if "nn > 1" (for compatibility with the
- old package)? *)
+ old package)? And for codatatypes as well? *)
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
|> map (fn (thmN, thms, attrs) =>
- ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
+ ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
val notes =
[(inductN, map single induct_thms,
fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
- (itersN, iter_thmss, K simp_attrs),
+ (itersN, iter_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
(recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
(simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
@@ -687,9 +690,11 @@
fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
ctr_defss, coiter_defs, corec_defs), lthy) =
let
- val selsss0 = map #1 wrap_ress;
- val discIss = map #5 wrap_ress;
- val sel_thmsss = map #6 wrap_ress;
+ val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
+ val selsss = map #2 wrap_ress;
+ val disc_thmsss = map #6 wrap_ress;
+ val discIss = map #7 wrap_ress;
+ val sel_thmsss = map #8 wrap_ress;
val (vs', _) =
lthy
@@ -704,17 +709,17 @@
`(conj_dests nn) coinduct_thm
end;
- val (coiter_thmss, corec_thmss) =
- let
- val z = the_single zs;
- val gcoiters = map (lists_bmoc pgss) coiters;
- val hcorecs = map (lists_bmoc phss) corecs;
+ fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
+
+ val z = the_single zs;
+ val gcoiters = map (lists_bmoc pgss) coiters;
+ val hcorecs = map (lists_bmoc phss) corecs;
- fun mk_cond_goal pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
-
- fun mk_coiter_like_goal pfss c cps fcoiter_like n k ctr m cfs' =
+ val (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss) =
+ let
+ fun mk_goal pfss c cps fcoiter_like n k ctr m cfs' =
fold_rev (fold_rev Logic.all) ([c] :: pfss)
- (Logic.list_implies (seq_conds mk_cond_goal n k cps,
+ (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
fun build_call fiter_likes maybe_tack (T, U) =
@@ -739,10 +744,10 @@
val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss;
val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
- val coiterss_goal =
- map8 (map4 oooo mk_coiter_like_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
- val corecss_goal =
- map8 (map4 oooo mk_coiter_like_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
+ val coiter_goalss =
+ map8 (map4 oooo mk_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
+ val corec_goalss =
+ map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
val coiter_tacss =
map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
@@ -750,58 +755,118 @@
val corec_tacss =
map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
ctr_defss;
+
+ fun prove goal tac =
+ Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
+
+ val coiter_thmss = map2 (map2 prove) coiter_goalss coiter_tacss;
+ val corec_thmss =
+ map2 (map2 prove) corec_goalss corec_tacss
+ |> map (map (unfold_defs lthy @{thms sum_case_if}));
+
+ val coiter_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
+ val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss;
+
+ val filter_safesss =
+ map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
+ curry (op ~~));
+
+ val safe_coiter_thmss = filter_safesss coiter_safesss coiter_thmss;
+ val safe_corec_thmss = filter_safesss corec_safesss corec_thmss;
in
- (map2 (map2 (fn goal => fn tac =>
- Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
- coiterss_goal coiter_tacss,
- map2 (map2 (fn goal => fn tac =>
- Skip_Proof.prove lthy [] [] goal (tac o #context)
- |> unfold_defs lthy @{thms sum_case_if} |> Thm.close_derivation))
- corecss_goal corec_tacss)
+ (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss)
end;
- fun mk_disc_coiter_like_thms [_] = K []
- | mk_disc_coiter_like_thms thms = map2 (curry (op RS)) thms;
+ val (disc_coiter_iff_thmss, disc_corec_iff_thmss) =
+ let
+ fun mk_goal c cps fcoiter_like n k disc =
+ mk_Trueprop_eq (disc $ (fcoiter_like $ c),
+ if n = 1 then @{const True}
+ else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
+
+ val coiter_goalss = map6 (map2 oooo mk_goal) cs cpss gcoiters ns kss discss;
+ val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
+
+ fun mk_case_split' cp =
+ Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
+
+ val case_splitss' = map (map mk_case_split') cpss;
+
+ val coiter_tacss =
+ map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' coiter_thmss disc_thmsss;
+ val corec_tacss =
+ map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
+
+ fun prove goal tac =
+ Skip_Proof.prove lthy [] [] goal (tac o #context)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy no_defs_lthy);
+
+ fun proves [_] [_] = []
+ | proves goals tacs = map2 prove goals tacs;
+ in
+ (map2 proves coiter_goalss coiter_tacss,
+ map2 proves corec_goalss corec_tacss)
+ end;
+
+ fun mk_disc_coiter_like_thms coiter_likes discIs =
+ map (op RS) (filter_out (is_triv_implies o snd) (coiter_likes ~~ discIs));
val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
- fun mk_sel_coiter_like_thm coiter_like_thm sel0 sel_thm =
+ fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
let
- val (domT, ranT) = dest_funT (fastype_of sel0);
+ val (domT, ranT) = dest_funT (fastype_of sel);
val arg_cong' =
Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
- [NONE, NONE, SOME (certify lthy sel0)] arg_cong
+ [NONE, NONE, SOME (certify lthy sel)] arg_cong
|> Thm.varifyT_global;
val sel_thm' = sel_thm RSN (2, trans);
in
coiter_like_thm RS arg_cong' RS sel_thm'
end;
- val sel_coiter_thmsss =
- map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss0 sel_thmsss;
- val sel_corec_thmsss =
- map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss0 sel_thmsss;
+ fun mk_sel_coiter_like_thms coiter_likess =
+ map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_likess selsss sel_thmsss |> map flat;
+
+ val sel_coiter_thmss = mk_sel_coiter_like_thms coiter_thmss;
+ val sel_corec_thmss = mk_sel_coiter_like_thms corec_thmss;
+
+ fun zip_coiter_like_thms coiter_likes disc_coiter_likes sel_coiter_likes =
+ coiter_likes @ disc_coiter_likes @ sel_coiter_likes;
+
+ val simp_thmss =
+ mk_simp_thmss wrap_ress
+ (map3 zip_coiter_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
+ (map3 zip_coiter_like_thms safe_coiter_thmss disc_coiter_thmss sel_coiter_thmss);
+
+ val anonymous_notes =
+ [(flat safe_coiter_thmss @ flat safe_corec_thmss, simp_attrs)]
+ |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val common_notes =
(if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
|> map (fn (thmN, thms, attrs) =>
- ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
+ ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
val notes =
[(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
(coitersN, coiter_thmss, []),
- (disc_coitersN, disc_coiter_thmss, []),
- (sel_coitersN, map flat sel_coiter_thmsss, []),
(corecsN, corec_thmss, []),
- (disc_corecsN, disc_corec_thmss, []),
- (sel_corecsN, map flat sel_corec_thmsss, [])]
+ (disc_coiter_iffN, disc_coiter_iff_thmss, simp_attrs),
+ (disc_coitersN, disc_coiter_thmss, simp_attrs),
+ (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
+ (disc_corecsN, disc_corec_thmss, simp_attrs),
+ (sel_coitersN, sel_coiter_thmss, simp_attrs),
+ (sel_corecsN, sel_corec_thmss, simp_attrs),
+ (simpsN, simp_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
map_filter (fn (_, []) => NONE | (b, thms) =>
SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
[(thms, [])])) (fp_bs ~~ thmss));
in
- lthy |> Local_Theory.notes (common_notes @ notes) |> snd
+ lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
end;
fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 21 11:47:16 2012 +0200
@@ -9,6 +9,7 @@
sig
val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
+ val mk_disc_coiter_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
@@ -69,24 +70,31 @@
unfold_defs_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
-val iter_like_thms =
+val iter_like_unfold_thms =
@{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
split_conv};
fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt =
unfold_defs_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
- iter_like_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1;
+ iter_like_unfold_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1;
val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
+val coiter_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN
subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
- unfold_defs_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
+ unfold_defs_tac ctxt (pre_map_def :: coiter_like_unfold_thms @ map_ids) THEN
unfold_defs_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
+fun mk_disc_coiter_like_iff_tac case_splits' coiter_likes discs ctxt =
+ EVERY (map3 (fn case_split_tac => fn coiter_like_thm => fn disc =>
+ case_split_tac 1 THEN unfold_defs_tac ctxt [coiter_like_thm] THEN
+ asm_simp_tac (ss_only @{thms simp_thms(7,8,12,14,22,24)}) 1 THEN
+ (if is_refl disc then all_tac else rtac disc 1))
+ (map rtac case_splits' @ [K all_tac]) coiter_likes discs);
+
val solve_prem_prem_tac =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
@@ -99,8 +107,7 @@
fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
- SELECT_GOAL (unfold_defs_tac ctxt
- (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
+ SELECT_GOAL (unfold_defs_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
solve_prem_prem_tac]) (rev kks)) 1;
fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 11:47:16 2012 +0200
@@ -2266,9 +2266,8 @@
(tcoalg_thm RS bis_diag_thm))))
|> Thm.close_derivation;
- (*### FIXME: get rid of mem_Id_eq_eq? or Id_def'? *)
val pred_of_rel_thms =
- rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv mem_Id_eq_eq snd_conv split_conv};
+ rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct;
val pred_coinduct_upto = unfold_defs lthy pred_of_rel_thms rel_coinduct_upto;
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 11:47:16 2012 +0200
@@ -129,25 +129,20 @@
open BNF_FP
open BNF_GFP_Util
-val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]};
val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
-val list_inject_subst_id = @{thm list.inject[THEN subst, of "%x. x"]};
+val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
val nat_induct = @{thm nat_induct};
val o_apply_trans_sym = o_apply RS trans RS sym;
val ord_eq_le_trans = @{thm ord_eq_le_trans};
val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
@{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
-val set_mp = @{thm set_mp};
-val set_rev_mp = @{thm set_rev_mp};
val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
-val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
-val subst_id = @{thm subst[of _ _ "%x. x"]};
val sum_case_weak_cong = @{thm sum_case_weak_cong};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
fun mk_coalg_set_tac coalg_def =
- dtac (coalg_def RS subst_id) 1 THEN
+ dtac (coalg_def RS iffD1) 1 THEN
REPEAT_DETERM (etac conjE 1) THEN
EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
@@ -291,7 +286,7 @@
dtac (rel_O_Gr RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
- REPEAT_DETERM o dtac Pair_eq_subst_id,
+ REPEAT_DETERM o dtac Pair_eqD,
REPEAT_DETERM o etac conjE,
hyp_subst_tac,
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -319,7 +314,7 @@
end;
fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
- EVERY' [stac bis_rel, dtac (bis_rel RS subst_id),
+ EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
@@ -333,7 +328,7 @@
rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
- EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS subst_id),
+ EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
CONJ_WRAP' (fn (rel_cong, rel_O) =>
@@ -343,7 +338,7 @@
REPEAT_DETERM_N (length rel_congs) o rtac refl,
rtac rel_O,
etac @{thm relcompE},
- REPEAT_DETERM o dtac Pair_eq_subst_id,
+ REPEAT_DETERM o dtac Pair_eqD,
etac conjE, hyp_subst_tac,
REPEAT_DETERM o etac allE, rtac @{thm relcompI},
etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
@@ -391,17 +386,17 @@
rtac (mk_nth_conv n i)] 1;
fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
- EVERY' [rtac (@{thm equiv_def} RS ssubst_id),
+ EVERY' [rtac (@{thm equiv_def} RS iffD2),
- rtac conjI, rtac (@{thm refl_on_def} RS ssubst_id),
+ rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
- rtac conjI, rtac (@{thm sym_def} RS ssubst_id),
+ rtac conjI, rtac (@{thm sym_def} RS iffD2),
rtac allI, rtac allI, rtac impI, rtac set_mp,
rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
- rtac (@{thm trans_def} RS ssubst_id),
+ rtac (@{thm trans_def} RS iffD2),
rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
etac @{thm relcompI}, atac] 1;
@@ -535,7 +530,7 @@
hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
- [rtac (mk_UnIN n i), dtac (def RS subst_id),
+ [rtac (mk_UnIN n i), dtac (def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
REPEAT_DETERM_N m o (rtac conjI THEN' atac),
CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
@@ -547,9 +542,9 @@
fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- dtac Pair_eq_subst_id,
+ dtac Pair_eqD,
etac conjE, hyp_subst_tac,
- dtac (isNode_def RS subst_id),
+ dtac (isNode_def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE],
rtac (equalityD2 RS set_mp),
rtac (strT_def RS arg_cong RS trans),
@@ -573,8 +568,8 @@
rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
- dtac conjunct2, dtac Pair_eq_subst_id, etac conjE,
- hyp_subst_tac, dtac (isNode_def RS subst_id),
+ dtac conjunct2, dtac Pair_eqD, etac conjE,
+ hyp_subst_tac, dtac (isNode_def RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, conjE],
rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
(ks ~~ (carT_defs ~~ isNode_defs));
@@ -719,8 +714,8 @@
CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
- rtac (rv_Nil RS arg_cong RS ssubst_id),
- rtac (mk_sum_casesN n i RS ssubst_id),
+ rtac (rv_Nil RS arg_cong RS iffD2),
+ rtac (mk_sum_casesN n i RS iffD2),
CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
(ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
REPEAT_DETERM o rtac allI,
@@ -729,8 +724,8 @@
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn (i, (from_to_sbd, coalg_set)) =>
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
- rtac (rv_Cons RS arg_cong RS ssubst_id),
- rtac (mk_sum_casesN n i RS arg_cong RS trans RS ssubst_id),
+ rtac (rv_Cons RS arg_cong RS iffD2),
+ rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
etac coalg_set, atac])
@@ -802,7 +797,7 @@
hyp_subst_tac,
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
(fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
- dtac list_inject_subst_id THEN' etac conjE THEN'
+ dtac list_inject_iffD1 THEN' etac conjE THEN'
(if k = i'
then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
else etac (mk_InN_not_InM i' k RS notE)))
@@ -822,10 +817,10 @@
dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
- dtac list_inject_subst_id THEN' etac conjE THEN'
+ dtac list_inject_iffD1 THEN' etac conjE THEN'
(if k = i
then EVERY' [dtac (mk_InN_inject n i),
- dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+ dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
atac, atac, hyp_subst_tac] THEN'
CONJ_WRAP' (fn i'' =>
EVERY' [rtac impI, dtac (sym RS trans),
@@ -957,7 +952,7 @@
rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
- DETERM o EVERY' [rtac trans, rtac o_apply, rtac ssubst, rtac @{thm Pair_eq}, rtac conjI,
+ DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
rtac trans, rtac @{thm Shift_def},
rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
@@ -965,9 +960,9 @@
rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- dtac list_inject_subst_id, etac conjE,
+ dtac list_inject_iffD1, etac conjE,
if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
- dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+ dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
@@ -980,9 +975,9 @@
dtac (Lev_Suc RS equalityD1 RS set_mp),
CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- dtac list_inject_subst_id, etac conjE,
+ dtac list_inject_iffD1, etac conjE,
if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
- dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+ dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
atac, atac, hyp_subst_tac, atac]
else etac (mk_InN_not_InM i' i'' RS notE)])
(rev ks),
@@ -1067,7 +1062,7 @@
CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
- EVERY' [rtac ssubst_id, rtac mor_UNIV,
+ EVERY' [rtac iffD2, rtac mor_UNIV,
CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) =>
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans),
rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
@@ -1082,7 +1077,7 @@
let
val n = length Rep_injects;
in
- EVERY' [rtac rev_mp, ftac (bis_def RS subst_id),
+ EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
@@ -1456,7 +1451,7 @@
fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
mor_unique pick_cols hset_defs =
- EVERY' [rtac (@{thm wpull_def} RS ssubst_id), REPEAT_DETERM o rtac allI, rtac impI,
+ EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
rtac box_equals, rtac mor_unique,
rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 11:47:16 2012 +0200
@@ -86,15 +86,12 @@
val id_apply = @{thm id_apply};
val meta_mp = @{thm meta_mp};
val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val set_mp = @{thm set_mp};
-val set_rev_mp = @{thm set_rev_mp};
val subset_UNIV = @{thm subset_UNIV};
val subset_trans = @{thm subset_trans};
-val subst_id = @{thm subst[of _ _ "\<lambda>x. x"]};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
fun mk_alg_set_tac alg_def =
- dtac (alg_def RS subst_id) 1 THEN
+ dtac (alg_def RS iffD1) 1 THEN
REPEAT_DETERM (etac conjE 1) THEN
EVERY' [etac bspec, rtac CollectI] 1 THEN
REPEAT_DETERM (etac conjI 1) THEN atac 1;
@@ -161,8 +158,8 @@
(EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
in
(stac mor_def THEN'
- dtac (alg_def RS subst_id) THEN'
- dtac (alg_def RS subst_id) THEN'
+ dtac (alg_def RS iffD1) THEN'
+ dtac (alg_def RS iffD1) THEN'
REPEAT o etac conjE THEN'
rtac conjI THEN'
CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
@@ -281,7 +278,7 @@
(rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN'
rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN'
REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN'
- CONJ_WRAP_GEN' (EVERY' [rtac ssubst, rtac @{thm Pair_eq}, rtac conjI]) minH_tac in_congs) 1
+ CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
end;
fun mk_min_algs_mono_tac min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 11:47:16 2012 +0200
@@ -121,10 +121,18 @@
val ctrans: thm
val o_apply: thm
+ val set_mp: thm
+ val set_rev_mp: thm
+ val Pair_eqD: thm
+ val Pair_eqI: thm
val mk_sym: thm -> thm
val mk_trans: thm -> thm -> thm
val mk_unabs_def: int -> thm -> thm
+ val is_refl: thm -> bool
+ val no_refl: thm list -> thm list
+ val no_reflexive: thm list -> thm list
+
val fold_defs: Proof.context -> thm list -> thm -> thm
val unfold_defs: Proof.context -> thm list -> thm -> thm
@@ -514,6 +522,10 @@
(*TODO: antiquote heavily used theorems once*)
val ctrans = @{thm ordLeq_transitive};
val o_apply = @{thm o_apply};
+val set_mp = @{thm set_mp};
+val set_rev_mp = @{thm set_rev_mp};
+val Pair_eqD = @{thm iffD1[OF Pair_eq]};
+val Pair_eqI = @{thm iffD2[OF Pair_eq]};
fun mk_nthN 1 t 1 = t
| mk_nthN _ t 1 = HOLogic.mk_fst t
@@ -592,6 +604,13 @@
fun mk_unabs_def 0 thm = thm
| mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]};
+fun is_refl thm =
+ op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm)))
+ handle TERM _ => false;
+
+val no_refl = filter_out is_refl;
+val no_reflexive = filter_out Thm.is_reflexive;
+
fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 21 11:47:16 2012 +0200
@@ -9,11 +9,13 @@
sig
val mk_half_pairss: 'a list -> ('a * 'a) list list
val mk_ctr: typ list -> term -> term
+ val mk_disc_or_sel: typ list -> term -> term
val base_name_of_ctr: term -> string
val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
((bool * term list) * term) *
(binding list * (binding list list * (binding * term) list list)) -> local_theory ->
- (term list list * thm list * thm list * thm list * thm list * thm list list) * local_theory
+ (term list * term list list * thm list * thm list * thm list * thm list list * thm list *
+ thm list list) * local_theory
val parse_wrap_options: bool parser
val parse_bound_term: (binding * string) parser
end;
@@ -38,6 +40,7 @@
val discsN = "discs";
val distinctN = "distinct";
val exhaustN = "exhaust";
+val expandN = "expand";
val injectN = "inject";
val nchotomyN = "nchotomy";
val selsN = "sels";
@@ -58,10 +61,18 @@
fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
fun mk_half_pairss' _ [] = []
- | mk_half_pairss' indent (y :: ys) =
- indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys);
+ | mk_half_pairss' indent (x :: xs) =
+ indent @ fold_rev (cons o single o pair x) xs (mk_half_pairss' ([] :: indent) xs);
+
+fun mk_half_pairss xs = mk_half_pairss' [[]] xs;
-fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
+fun join_halves n half_xss other_half_xss =
+ let
+ val xsss =
+ map2 (map2 append) (Library.chop_groups n half_xss)
+ (transpose (Library.chop_groups n other_half_xss))
+ val xs = interleave (flat half_xss) (flat other_half_xss);
+ in (xs, xsss |> `transpose) end;
fun mk_undefined T = Const (@{const_name undefined}, T);
@@ -70,21 +81,24 @@
Term.subst_atomic_types (Ts0 ~~ Ts) ctr
end;
+fun mk_disc_or_sel Ts t =
+ Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+
fun base_name_of_ctr c =
Long_Name.base_name (case head_of c of
Const (s, _) => s
| Free (s, _) => s
| _ => error "Cannot extract name of constructor");
+fun rap u t = betapply (t, u);
+
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
(raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
- (* TODO: attributes (simp, case_names, etc.) *)
(* TODO: case syntax *)
- (* TODO: integration with function package ("size") *)
val n = length raw_ctrs;
val ks = 1 upto n;
@@ -157,20 +171,17 @@
val casex = mk_case As B;
val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
- val ((((((((xss, xss'), yss), fs), gs), (v, v')), w), (p, p')), names_lthy) = no_defs_lthy |>
+ val ((((((((xss, xss'), yss), fs), gs), (u, u')), v), (p, p')), names_lthy) = no_defs_lthy |>
mk_Freess' "x" ctr_Tss
||>> mk_Freess "y" ctr_Tss
||>> mk_Frees "f" case_Ts
||>> mk_Frees "g" case_Ts
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") dataT
- ||>> yield_singleton (mk_Frees "w") dataT
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "u") dataT
+ ||>> yield_singleton (mk_Frees "v") dataT
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
val q = Free (fst p', mk_pred1T B);
- fun ap_v t = t $ v;
- fun mk_v_eq_v () = HOLogic.mk_eq (v, v);
-
val xctrs = map2 (curry Term.list_comb) ctrs xss;
val yctrs = map2 (curry Term.list_comb) ctrs yss;
@@ -183,28 +194,37 @@
val fcase = Term.list_comb (casex, eta_fs);
val gcase = Term.list_comb (casex, eta_gs);
- val exist_xs_v_eq_ctrs =
- map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
+ val ufcase = fcase $ u;
+ val vfcase = fcase $ v;
+ val vgcase = gcase $ v;
+
+ fun mk_u_eq_u () = HOLogic.mk_eq (u, u);
+
+ val u_eq_v = mk_Trueprop_eq (u, v);
+
+ val exist_xs_u_eq_ctrs =
+ map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
val unique_disc_no_def = TrueI; (*arbitrary marker*)
val alternate_disc_no_def = FalseE; (*arbitrary marker*)
- fun alternate_disc_lhs get_disc k =
+ fun alternate_disc_lhs get_udisc k =
HOLogic.mk_not
(case nth disc_bindings (k - 1) of
- NONE => nth exist_xs_v_eq_ctrs (k - 1)
- | SOME b => get_disc b (k - 1) $ v);
+ NONE => nth exist_xs_u_eq_ctrs (k - 1)
+ | SOME b => get_udisc b (k - 1));
- val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
+ val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
+ sel_defss, lthy') =
if no_dests then
- (true, [], [], [], [], [], no_defs_lthy)
+ (true, [], [], [], [], [], [], [], [], [], no_defs_lthy)
else
let
fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT);
- fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
+ fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
- fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k));
+ fun alternate_disc k = Term.lambda u (alternate_disc_lhs (K o rap u o disc_free) (3 - k));
fun mk_default T t =
let
@@ -236,8 +256,8 @@
quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
" vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
in
- mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ v,
- Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v)
+ mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u,
+ Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ u)
end;
val sel_bindings = flat sel_bindingss;
@@ -259,14 +279,14 @@
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
no_defs_lthy
- |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr =>
+ |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr =>
fn NONE =>
- if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), unique_disc_no_def)
- else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl)
+ if n = 1 then pair (Term.lambda u (mk_u_eq_u ()), unique_disc_no_def)
+ else if m = 0 then pair (Term.lambda u exist_xs_u_eq_ctr, refl)
else pair (alternate_disc k, alternate_disc_no_def)
| SOME b => Specification.definition (SOME (b, NONE, NoSyn),
- ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd)
- ks ms exist_xs_v_eq_ctrs disc_bindings
+ ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
+ ks ms exist_xs_u_eq_ctrs disc_bindings
||>> apfst split_list o fold_map (fn (b, proto_sels) =>
Specification.definition (SOME (b, NONE, NoSyn),
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
@@ -281,23 +301,27 @@
val discs0 = map (Morphism.term phi) raw_discs;
val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
- fun mk_disc_or_sel Ts c =
- Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c;
-
val discs = map (mk_disc_or_sel As) discs0;
val selss = map (map (mk_disc_or_sel As)) selss0;
+
+ val udiscs = map (rap u) discs;
+ val uselss = map (map (rap u)) selss;
+
+ val vdiscs = map (rap v) discs;
+ val vselss = map (map (rap v)) selss;
in
- (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy')
+ (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
+ sel_defss, lthy')
end;
fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
val exhaust_goal =
- let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in
- fold_rev Logic.all [p, v] (mk_imp_p (map2 mk_prem xctrs xss))
+ let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
+ fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss))
end;
- val injectss_goal =
+ val inject_goalss =
let
fun mk_goal _ _ [] [] = []
| mk_goal xctr yctr xs ys =
@@ -307,7 +331,7 @@
map4 mk_goal xctrs yctrs xss yss
end;
- val half_distinctss_goal =
+ val half_distinct_goalss =
let
fun mk_goal ((xs, xc), (xs', xc')) =
fold_rev Logic.all (xs @ xs')
@@ -320,7 +344,7 @@
map3 (fn xs => fn xctr => fn xf =>
fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
- val goalss = [exhaust_goal] :: injectss_goal @ half_distinctss_goal @ [cases_goal];
+ val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
fun after_qed thmss lthy =
let
@@ -329,35 +353,34 @@
val inject_thms = flat inject_thmss;
- val exhaust_thm' =
- let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in
- Drule.instantiate' [] [SOME (certify lthy v)]
- (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm))
- end;
+ val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
+
+ fun inst_thm t thm =
+ Drule.instantiate' [] [SOME (certify lthy t)]
+ (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes thm));
+
+ val uexhaust_thm = inst_thm u exhaust_thm;
val exhaust_cases = map base_name_of_ctr ctrs;
val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
- val (distinct_thmsss', distinct_thmsss) =
- map2 (map2 append) (Library.chop_groups n half_distinct_thmss)
- (transpose (Library.chop_groups n other_half_distinct_thmss))
- |> `transpose;
- val distinct_thms = interleave (flat half_distinct_thmss) (flat other_half_distinct_thmss);
+ val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
+ join_halves n half_distinct_thmss other_half_distinct_thmss;
val nchotomy_thm =
let
val goal =
- HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v',
- Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs));
+ HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u',
+ Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs));
in
Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
end;
- val (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
- collapse_thms, case_eq_thms) =
+ val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
+ disc_exhaust_thms, collapse_thms, expand_thms, case_eq_thms) =
if no_dests then
- ([], [], [], [], [], [], [], [])
+ ([], [], [], [], [], [], [], [], [], [])
else
let
fun make_sel_thm xs' case_thm sel_def =
@@ -382,9 +405,9 @@
fun mk_unique_disc_def () =
let
val m = the_single ms;
- val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs);
+ val goal = mk_Trueprop_eq (mk_u_eq_u (), the_single exist_xs_u_eq_ctrs);
in
- Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm')
+ Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -392,12 +415,12 @@
fun mk_alternate_disc_def k =
let
val goal =
- mk_Trueprop_eq (alternate_disc_lhs (K (nth discs)) (3 - k),
- nth exist_xs_v_eq_ctrs (k - 1));
+ mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
+ nth exist_xs_u_eq_ctrs (k - 1));
in
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
- (nth distinct_thms (2 - k)) exhaust_thm')
+ (nth distinct_thms (2 - k)) uexhaust_thm)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -431,103 +454,117 @@
val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss);
- val disc_exclude_thms =
- if has_alternate_disc_def then
- []
- else
- let
- fun mk_goal [] = []
- | mk_goal [((_, true), (_, true))] = []
- | mk_goal [(((_, disc), _), ((_, disc'), _))] =
- [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)),
- HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))];
- fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
+ val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
+ let
+ fun mk_goal [] = []
+ | mk_goal [((_, udisc), (_, udisc'))] =
+ [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc,
+ HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
+
+ fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
+
+ val infos = ms ~~ discD_thms ~~ udiscs;
+ val half_pairss = mk_half_pairss infos;
+
+ val half_goalss = map mk_goal half_pairss;
+ val half_thmss =
+ map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
+ fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
+ half_goalss half_pairss (flat disc_thmss');
- val infos = ms ~~ discD_thms ~~ discs ~~ no_discs;
- val half_pairss = mk_half_pairss infos;
+ val other_half_goalss = map (mk_goal o map swap) half_pairss;
+ val other_half_thmss =
+ map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
+ other_half_goalss;
+ in
+ join_halves n half_thmss other_half_thmss
+ |>> has_alternate_disc_def ? K []
+ end;
- val halvess_goal = map mk_goal half_pairss;
- val half_thmss =
- map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] =>
- fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
- halvess_goal half_pairss (flat disc_thmss');
-
- val other_halvess_goal = map (mk_goal o map swap) half_pairss;
- val other_half_thmss =
- map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
- other_halvess_goal;
- in
- interleave (flat half_thmss) (flat other_half_thmss)
- end;
+ val disc_exhaust_thm =
+ let
+ fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
+ val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
+ in
+ Skip_Proof.prove lthy [] [] goal (fn _ =>
+ mk_disc_exhaust_tac n exhaust_thm discI_thms)
+ end;
val disc_exhaust_thms =
- if has_alternate_disc_def orelse no_discs_at_all then
- []
- else
- let
- fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))];
- val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs));
- in
- [Skip_Proof.prove lthy [] [] goal (fn _ =>
- mk_disc_exhaust_tac n exhaust_thm discI_thms)]
- end;
+ if has_alternate_disc_def orelse no_discs_at_all then [] else [disc_exhaust_thm];
+
+ val (collapse_thms, collapse_thm_opts) =
+ let
+ fun mk_goal ctr udisc usels =
+ let
+ val prem = HOLogic.mk_Trueprop udisc;
+ val concl =
+ mk_Trueprop_eq ((null usels ? swap) (Term.list_comb (ctr, usels), u));
+ in
+ if prem aconv concl then NONE
+ else SOME (Logic.all u (Logic.mk_implies (prem, concl)))
+ end;
+ val goals = map3 mk_goal ctrs udiscs uselss;
+ in
+ map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_collapse_tac ctxt m discD sel_thms)
+ |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
+ |> `(map_filter I)
+ end;
- val collapse_thms =
- if no_dests then
- []
- else
- let
- fun mk_goal ctr disc sels =
- let
- val prem = HOLogic.mk_Trueprop (betapply (disc, v));
- val concl =
- mk_Trueprop_eq ((null sels ? swap)
- (Term.list_comb (ctr, map ap_v sels), v));
- in
- if prem aconv concl then NONE
- else SOME (Logic.all v (Logic.mk_implies (prem, concl)))
- end;
- val goals = map3 mk_goal ctrs discs selss;
- in
- map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_collapse_tac ctxt m discD sel_thms)
- |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
- |> map_filter I
- end;
+ val expand_thms =
+ let
+ fun mk_prems k udisc usels vdisc vsels =
+ (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
+ (if null usels then
+ []
+ else
+ [Logic.list_implies
+ (if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc],
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map2 (curry HOLogic.mk_eq) usels vsels)))]);
+
+ val uncollapse_thms =
+ map (fn NONE => Drule.dummy_thm | SOME thm => thm RS sym) collapse_thm_opts;
+
+ val goal =
+ Library.foldr Logic.list_implies
+ (map5 mk_prems ks udiscs uselss vdiscs vselss, u_eq_v);
+ in
+ [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_expand_tac ctxt n ms (inst_thm u disc_exhaust_thm)
+ (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
+ disc_exclude_thmsss')]
+ |> Proof_Context.export names_lthy lthy
+ end;
val case_eq_thms =
- if no_dests then
- []
- else
- let
- fun mk_body f sels = Term.list_comb (f, map ap_v sels);
- val goal =
- mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss));
- in
- [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)]
- |> Proof_Context.export names_lthy lthy
- end;
+ let
+ fun mk_body f usels = Term.list_comb (f, usels);
+ val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
+ in
+ [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_case_eq_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
+ |> Proof_Context.export names_lthy lthy
+ end;
in
- (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
- collapse_thms, case_eq_thms)
+ (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
+ disc_exhaust_thms, collapse_thms, expand_thms, case_eq_thms)
end;
val (case_cong_thm, weak_case_cong_thm) =
let
fun mk_prem xctr xs f g =
- fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr),
+ fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
mk_Trueprop_eq (f, g)));
- val v_eq_w = mk_Trueprop_eq (v, w);
-
val goal =
- Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
- mk_Trueprop_eq (fcase $ v, gcase $ w));
- val weak_goal = Logic.mk_implies (v_eq_w, mk_Trueprop_eq (fcase $ v, fcase $ w));
+ Logic.list_implies (u_eq_v :: map4 mk_prem xctrs xss fs gs,
+ mk_Trueprop_eq (ufcase, vgcase));
+ val weak_goal = Logic.mk_implies (u_eq_v, mk_Trueprop_eq (ufcase, vfcase));
in
- (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac exhaust_thm' case_thms),
+ (Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms),
Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1)))
|> pairself (singleton (Proof_Context.export names_lthy lthy))
end;
@@ -535,12 +572,12 @@
val (split_thm, split_asm_thm) =
let
fun mk_conjunct xctr xs f_xs =
- list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (v, xctr), q $ f_xs));
+ list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
fun mk_disjunct xctr xs f_xs =
- list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (v, xctr),
+ list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
HOLogic.mk_not (q $ f_xs)));
- val lhs = q $ (fcase $ v);
+ val lhs = q $ ufcase;
val goal =
mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
@@ -550,7 +587,7 @@
val split_thm =
Skip_Proof.prove lthy [] [] goal
- (fn _ => mk_split_tac exhaust_thm' case_thms inject_thmss distinct_thmsss)
+ (fn _ => mk_split_tac uexhaust_thm case_thms inject_thmss distinct_thmsss)
|> singleton (Proof_Context.export names_lthy lthy)
val split_asm_thm =
Skip_Proof.prove lthy [] [] asm_goal (fn {context = ctxt, ...} =>
@@ -573,6 +610,7 @@
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
(distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
+ (expandN, expand_thms, []),
(injectN, inject_thms, iff_attrs @ induct_simp_attrs),
(nchotomyN, [nchotomy_thm], []),
(selsN, all_sel_thms, simp_attrs),
@@ -588,7 +626,7 @@
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
in
- ((selss, inject_thms, distinct_thms, case_thms, discI_thms, sel_thmss),
+ ((discs, selss, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms, sel_thmss),
lthy |> Local_Theory.notes (notes' @ notes) |> snd)
end;
in
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Fri Sep 21 11:47:16 2012 +0200
@@ -13,6 +13,8 @@
tactic
val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
+ val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
+ thm list list list -> thm list list list -> tactic
val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
val mk_nchotomy_tac: int -> thm -> tactic
val mk_other_half_disc_exclude_tac: thm -> tactic
@@ -27,63 +29,88 @@
open BNF_Util
open BNF_Tactics
+val meta_mp = @{thm meta_mp};
+
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
fun mk_nchotomy_tac n exhaust =
(rtac allI THEN' rtac exhaust THEN'
EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
-fun mk_unique_disc_def_tac m exhaust' =
- EVERY' [rtac iffI, rtac exhaust', REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
+fun mk_unique_disc_def_tac m uexhaust =
+ EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
-fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' =
+fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
- rtac distinct, rtac exhaust'] @
+ rtac distinct, rtac uexhaust] @
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
|> k = 1 ? swap |> op @)) 1;
-fun mk_half_disc_exclude_tac m discD disc'_thm =
- (dtac discD THEN'
- REPEAT_DETERM_N m o etac exE THEN'
- hyp_subst_tac THEN'
- rtac disc'_thm) 1;
+fun mk_half_disc_exclude_tac m discD disc' =
+ (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1;
-fun mk_other_half_disc_exclude_tac half_thm =
- (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
+fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1;
fun mk_disc_exhaust_tac n exhaust discIs =
(rtac exhaust THEN'
EVERY' (map2 (fn k => fn discI =>
- dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
+ dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs)) 1;
-fun mk_collapse_tac ctxt m discD sel_thms =
+fun mk_collapse_tac ctxt m discD sels =
(dtac discD THEN'
(if m = 0 then
atac
else
- REPEAT_DETERM_N m o etac exE THEN'
- hyp_subst_tac THEN'
- SELECT_GOAL (unfold_defs_tac ctxt sel_thms) THEN'
- rtac refl)) 1;
+ REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
+ SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1;
-fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss =
- (rtac exhaust' THEN'
- EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
- EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_disc_thms @ sel_thms)),
- rtac case_thm])
- case_thms (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) disc_thmss') sel_thmss)) 1;
+fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
+ disc_excludesss' =
+ if ms = [0] then
+ rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1
+ else
+ let
+ val ks = 1 upto n;
+ val maybe_atac = if n = 1 then K all_tac else atac;
+ in
+ (rtac udisc_exhaust THEN'
+ EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
+ EVERY' [if m = 0 then K all_tac else subst_tac ctxt [uuncollapse] THEN' maybe_atac,
+ rtac sym, rtac vdisc_exhaust,
+ EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
+ EVERY'
+ (if k' = k then
+ if m = 0 then
+ [hyp_subst_tac, rtac refl]
+ else
+ [subst_tac ctxt [vuncollapse], maybe_atac,
+ if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
+ REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, asm_simp_tac (ss_only [])]
+ else
+ [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
+ etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
+ atac, atac]))
+ ks disc_excludess disc_excludess' uncollapses)])
+ ks ms disc_excludesss disc_excludesss' uncollapses)) 1
+ end;
-fun mk_case_cong_tac exhaust' case_thms =
- (rtac exhaust' THEN'
- EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1;
+fun mk_case_eq_tac ctxt n uexhaust cases discss' selss =
+ (rtac uexhaust THEN'
+ EVERY' (map3 (fn casex => fn if_discs => fn sels =>
+ EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex])
+ cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
+
+fun mk_case_cong_tac uexhaust cases =
+ (rtac uexhaust THEN'
+ EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1;
val naked_ctxt = Proof_Context.init_global @{theory HOL};
-fun mk_split_tac exhaust' case_thms injectss distinctsss =
- rtac exhaust' 1 THEN
+fun mk_split_tac uexhaust cases injectss distinctsss =
+ rtac uexhaust 1 THEN
ALLGOALS (fn k => (hyp_subst_tac THEN'
- simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @
+ simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
flat (nth distinctsss (k - 1))))) k) THEN
ALLGOALS (blast_tac naked_ctxt);
--- a/src/HOL/IMP/ACom.thy Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/IMP/ACom.thy Fri Sep 21 11:47:16 2012 +0200
@@ -21,15 +21,15 @@
fun post :: "'a acom \<Rightarrow>'a" where
"post (SKIP {P}) = P" |
"post (x ::= e {P}) = P" |
-"post (c1; c2) = post c2" |
-"post (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = P" |
-"post ({Inv} WHILE b DO {Pc} c {P}) = P"
+"post (C1; C2) = post C2" |
+"post (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = Q" |
+"post ({Inv} WHILE b DO {P} C {Q}) = Q"
fun strip :: "'a acom \<Rightarrow> com" where
"strip (SKIP {P}) = com.SKIP" |
"strip (x ::= e {P}) = (x ::= e)" |
-"strip (c1;c2) = (strip c1; strip c2)" |
-"strip (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
+"strip (C1;C2) = (strip C1; strip C2)" |
+"strip (IF b THEN {P1} C1 ELSE {P2} C2 {P}) = (IF b THEN strip C1 ELSE strip C2)" |
"strip ({Inv} WHILE b DO {Pc} c {P}) = (WHILE b DO strip c)"
fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
@@ -51,41 +51,41 @@
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
"map_acom f (SKIP {P}) = SKIP {f P}" |
"map_acom f (x ::= e {P}) = (x ::= e {f P})" |
-"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
-"map_acom f (IF b THEN {p1} c1 ELSE {p2} c2 {P}) =
- (IF b THEN {f p1} map_acom f c1 ELSE {f p2} map_acom f c2 {f P})" |
-"map_acom f ({Inv} WHILE b DO {p} c {P}) =
- ({f Inv} WHILE b DO {f p} map_acom f c {f P})"
+"map_acom f (C1;C2) = (map_acom f C1; map_acom f C2)" |
+"map_acom f (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+ (IF b THEN {f P1} map_acom f C1 ELSE {f P2} map_acom f C2 {f Q})" |
+"map_acom f ({Inv} WHILE b DO {P} C {Q}) =
+ ({f Inv} WHILE b DO {f P} map_acom f C {f Q})"
-lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
-by (induction c) simp_all
+lemma post_map_acom[simp]: "post(map_acom f C) = f(post C)"
+by (induction C) simp_all
-lemma strip_acom[simp]: "strip (map_acom f c) = strip c"
-by (induction c) auto
+lemma strip_acom[simp]: "strip (map_acom f C) = strip C"
+by (induction C) auto
lemma map_acom_SKIP:
- "map_acom f c = SKIP {S'} \<longleftrightarrow> (\<exists>S. c = SKIP {S} \<and> S' = f S)"
-by (cases c) auto
+ "map_acom f C = SKIP {S'} \<longleftrightarrow> (\<exists>S. C = SKIP {S} \<and> S' = f S)"
+by (cases C) auto
lemma map_acom_Assign:
- "map_acom f c = x ::= e {S'} \<longleftrightarrow> (\<exists>S. c = x::=e {S} \<and> S' = f S)"
-by (cases c) auto
+ "map_acom f C = x ::= e {S'} \<longleftrightarrow> (\<exists>S. C = x::=e {S} \<and> S' = f S)"
+by (cases C) auto
lemma map_acom_Seq:
- "map_acom f c = c1';c2' \<longleftrightarrow>
- (\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')"
-by (cases c) auto
+ "map_acom f C = C1';C2' \<longleftrightarrow>
+ (\<exists>C1 C2. C = C1;C2 \<and> map_acom f C1 = C1' \<and> map_acom f C2 = C2')"
+by (cases C) auto
lemma map_acom_If:
- "map_acom f c = IF b THEN {p1'} c1' ELSE {p2'} c2' {S'} \<longleftrightarrow>
- (\<exists>S p1 p2 c1 c2. c = IF b THEN {p1} c1 ELSE {p2} c2 {S} \<and>
- map_acom f c1 = c1' \<and> map_acom f c2 = c2' \<and> p1' = f p1 \<and> p2' = f p2 \<and> S' = f S)"
-by (cases c) auto
+ "map_acom f C = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'} \<longleftrightarrow>
+ (\<exists>P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} \<and>
+ map_acom f C1 = C1' \<and> map_acom f C2 = C2' \<and> P1' = f P1 \<and> P2' = f P2 \<and> Q' = f Q)"
+by (cases C) auto
lemma map_acom_While:
- "map_acom f w = {I'} WHILE b DO {p'} c' {P'} \<longleftrightarrow>
- (\<exists>I p P c. w = {I} WHILE b DO {p} c {P} \<and> map_acom f c = c' \<and> I' = f I \<and> p' = f p \<and> P' = f P)"
+ "map_acom f w = {I'} WHILE b DO {p'} C' {P'} \<longleftrightarrow>
+ (\<exists>I p P C. w = {I} WHILE b DO {p} C {P} \<and> map_acom f C = C' \<and> I' = f I \<and> p' = f p \<and> P' = f P)"
by (cases w) auto
@@ -106,16 +106,16 @@
lemma strip_eq_If:
"strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow>
- (EX p1 p2 C1 C2 P. C = IF b THEN {p1} C1 ELSE {p2} C2 {P} & strip C1 = c1 & strip C2 = c2)"
+ (EX P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} & strip C1 = c1 & strip C2 = c2)"
by (cases C) simp_all
lemma strip_eq_While:
"strip C = WHILE b DO c1 \<longleftrightarrow>
- (EX I p C1 P. C = {I} WHILE b DO {p} C1 {P} & strip C1 = c1)"
+ (EX I P C1 Q. C = {I} WHILE b DO {P} C1 {Q} & strip C1 = c1)"
by (cases C) simp_all
-lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}"
-by(induction C)(auto)
+lemma set_annos_anno[simp]: "set (annos (anno a c)) = {a}"
+by(induction c)(auto)
lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
apply(induct C2 arbitrary: C1)
--- a/src/HOL/IMP/Collecting.thy Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy Fri Sep 21 11:47:16 2012 +0200
@@ -1,5 +1,5 @@
theory Collecting
-imports Complete_Lattice ACom
+imports Complete_Lattice Big_Step ACom
begin
subsection "Collecting Semantics of Commands"
@@ -138,6 +138,7 @@
lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
by(induction c d rule: less_eq_acom.induct) auto
+
subsubsection "Collecting semantics"
fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
@@ -182,4 +183,55 @@
lemma strip_CS[simp]: "strip(CS c) = c"
by(simp add: CS_def index_lfp[simplified])
+
+subsubsection "Relation to big-step semantics"
+
+lemma post_Union_acom: "\<forall> c' \<in> M. strip c' = c \<Longrightarrow> post (Union_acom c M) = post ` M"
+proof(induction c arbitrary: M)
+ case (Seq c1 c2)
+ have "post ` M = post ` sub\<^isub>2 ` M" using Seq.prems by (force simp: strip_eq_Seq)
+ moreover have "\<forall> c' \<in> sub\<^isub>2 ` M. strip c' = c2" using Seq.prems by (auto simp: strip_eq_Seq)
+ ultimately show ?case using Seq.IH(2)[of "sub\<^isub>2 ` M"] by simp
+qed simp_all
+
+
+lemma post_lfp: "post(lfp c f) = (\<Inter>{post C|C. strip C = c \<and> f C \<le> C})"
+by(auto simp add: lfp_def post_Union_acom)
+
+lemma big_step_post_step:
+ "\<lbrakk> (c, s) \<Rightarrow> t; strip C = c; s \<in> S; step S C \<le> C \<rbrakk> \<Longrightarrow> t \<in> post C"
+proof(induction arbitrary: C S rule: big_step_induct)
+ case Skip thus ?case by(auto simp: strip_eq_SKIP)
+next
+ case Assign thus ?case by(fastforce simp: strip_eq_Assign)
+next
+ case Seq thus ?case by(fastforce simp: strip_eq_Seq)
+next
+ case IfTrue thus ?case apply(auto simp: strip_eq_If)
+ by (metis (lifting) mem_Collect_eq set_mp)
+next
+ case IfFalse thus ?case apply(auto simp: strip_eq_If)
+ by (metis (lifting) mem_Collect_eq set_mp)
+next
+ case (WhileTrue b s1 c' s2 s3)
+ from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
+ by(auto simp: strip_eq_While)
+ from WhileTrue.prems(3) `C = _`
+ have "step P C' \<le> C'" "{s \<in> I. bval b s} \<le> P" "S \<le> I" "step (post C') C \<le> C" by auto
+ have "step {s \<in> I. bval b s} C' \<le> C'"
+ by (rule order_trans[OF mono2_step[OF order_refl `{s \<in> I. bval b s} \<le> P`] `step P C' \<le> C'`])
+ have "s1: {s:I. bval b s}" using `s1 \<in> S` `S \<subseteq> I` `bval b s1` by auto
+ note s2_in_post_C' = WhileTrue.IH(1)[OF `strip C' = c'` this `step {s \<in> I. bval b s} C' \<le> C'`]
+ from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' `step (post C') C \<le> C`]
+ show ?case .
+next
+ case (WhileFalse b s1 c') thus ?case by (force simp: strip_eq_While)
+qed
+
+lemma big_step_lfp: "\<lbrakk> (c,s) \<Rightarrow> t; s \<in> S \<rbrakk> \<Longrightarrow> t \<in> post(lfp c (step S))"
+by(auto simp add: post_lfp intro: big_step_post_step)
+
+lemma big_step_CS: "(c,s) \<Rightarrow> t \<Longrightarrow> t : post(CS c)"
+by(simp add: CS_def big_step_lfp)
+
end
--- a/src/HOL/IMP/Complete_Lattice.thy Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/IMP/Complete_Lattice.thy Fri Sep 21 11:47:16 2012 +0200
@@ -1,3 +1,5 @@
+header "Abstract Interpretation"
+
theory Complete_Lattice
imports Main
begin
--- a/src/HOL/Library/RBT_Impl.thy Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Fri Sep 21 11:47:16 2012 +0200
@@ -1197,6 +1197,8 @@
end
+subsection {* Code generator setup *}
+
lemmas [code] =
ord.rbt_less_prop
ord.rbt_greater_prop
@@ -1217,6 +1219,36 @@
ord.rbt_map_entry.simps
ord.rbt_bulkload_def
+text {* More efficient implementations for @{term entries} and @{term keys} *}
+
+definition gen_entries ::
+ "(('a \<times> 'b) \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
+where
+ "gen_entries kvts t = entries t @ concat (List.map (\<lambda>(kv, t). kv # entries t) kvts)"
+
+lemma gen_entries_simps [simp, code]:
+ "gen_entries [] Empty = []"
+ "gen_entries ((kv, t) # kvts) Empty = kv # gen_entries kvts t"
+ "gen_entries kvts (Branch c l k v r) = gen_entries (((k, v), r) # kvts) l"
+by(simp_all add: gen_entries_def)
+
+lemma entries_code [code]:
+ "entries = gen_entries []"
+by(simp add: gen_entries_def fun_eq_iff)
+
+definition gen_keys :: "('a \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a list"
+where "gen_keys kts t = RBT_Impl.keys t @ concat (List.map (\<lambda>(k, t). k # keys t) kts)"
+
+lemma gen_keys_simps [simp, code]:
+ "gen_keys [] Empty = []"
+ "gen_keys ((k, t) # kts) Empty = k # gen_keys kts t"
+ "gen_keys kts (Branch c l k v r) = gen_keys ((k, r) # kts) l"
+by(simp_all add: gen_keys_def)
+
+lemma keys_code [code]:
+ "keys = gen_keys []"
+by(simp add: gen_keys_def fun_eq_iff)
+
text {* Restore original type constraints for constants *}
setup {*
fold Sign.add_const_constraint
@@ -1240,6 +1272,6 @@
(@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
*}
-hide_const (open) R B Empty entries keys map fold
+hide_const (open) R B Empty entries keys map fold gen_keys gen_entries
end
--- a/src/HOL/ROOT Fri Sep 21 11:42:14 2012 +0200
+++ b/src/HOL/ROOT Fri Sep 21 11:47:16 2012 +0200
@@ -610,7 +610,7 @@
"document/root.tex"
"document/root.bib"
-session "HOL-Codatatype" in Codatatype = "HOL-Cardinals-Base" +
+session "HOL-Codatatype" in Codatatype = "HOL-Cardinals" +
description {* New (Co)datatype Package *}
options [document = false]
theories Codatatype