--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Cardinals/Cardinals.thy Wed Sep 19 12:11:09 2012 +0200
@@ -0,0 +1,15 @@
+(* Title: HOL/Cardinals/Cardinals.thy
+ Author: Andrei Popescu, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2012
+
+Theory of ordinals and cardinals.
+*)
+
+header {* Theory of Ordinals and Cardinals *}
+
+theory Cardinals
+imports Cardinal_Order_Relation Cardinal_Arithmetic
+begin
+
+end
--- a/src/HOL/Codatatype/BNF_FP.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy Wed Sep 19 12:11:09 2012 +0200
@@ -104,19 +104,20 @@
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
-lemma UN_compreh_bex:
-"\<Union>{y. \<exists>x \<in> A. y = {}} = {}"
-"\<Union>{y. \<exists>x \<in> A. y = {f x}} = {y. \<exists>x \<in> A. y = f x}"
-by blast+
+lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
+by blast
-lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C"
-apply (rule exI)
-apply (rule conjI)
- apply (rule bexI)
- apply (rule refl)
- apply assumption
-apply assumption
-done
+lemma prod_set_simps:
+"fsts (x, y) = {x}"
+"snds (x, y) = {y}"
+unfolding fsts_def snds_def by simp+
+
+lemma sum_set_simps:
+"sum_setl (Inl x) = {x}"
+"sum_setl (Inr x) = {}"
+"sum_setr (Inl x) = {}"
+"sum_setr (Inr x) = {x}"
+unfolding sum_setl_def sum_setr_def by simp+
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_sugar_tactics.ML"
--- a/src/HOL/Codatatype/Basic_BNFs.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy Wed Sep 19 12:11:09 2012 +0200
@@ -24,7 +24,7 @@
lemma natLeq_cinfinite: "cinfinite natLeq"
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
-bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
+bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
apply auto
apply (rule natLeq_card_order)
apply (rule natLeq_cinfinite)
@@ -52,7 +52,7 @@
lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>"
unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto
-bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
+bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
apply (auto simp add: wpull_id)
apply (rule card_order_csum)
apply (rule natLeq_card_order)
@@ -86,8 +86,8 @@
structure Basic_BNFs : BASIC_BNFS =
struct
-val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
-val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
+val ID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.ID");
+val DEADID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.DEADID");
val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
val ID_rel_def = rel_def RS sym;
@@ -104,7 +104,7 @@
lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def]
-bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
+bnf_def sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
proof -
show "sum_map id id = id" by (rule sum_map.id)
next
@@ -240,7 +240,7 @@
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
-bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
+bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
proof (unfold prod_set_defs)
show "map_pair id id = id" by (rule map_pair.id)
next
@@ -320,7 +320,6 @@
lemma prod_pred[simp]:
"prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> (\<phi> a1 a2 \<and> \<psi> b1 b2))"
unfolding prod_set_defs prod_pred_def prod_rel_def Gr_def relcomp_unfold converse_unfold by auto
-(* TODO: pred characterization for each basic BNF *)
(* Categorical version of pullback: *)
lemma wpull_cat:
@@ -358,7 +357,7 @@
ultimately show ?thesis using card_of_ordLeq by fast
qed
-bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
+bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
["%c x::'b::type. c::'a::type"]
proof
fix f show "id \<circ> f = id f" by simp
--- a/src/HOL/Codatatype/Countable_Set.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Countable_Set.thy Wed Sep 19 12:11:09 2012 +0200
@@ -8,7 +8,7 @@
header {* (At Most) Countable Sets *}
theory Countable_Set
-imports "../Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/Countable"
+imports "../Cardinals/Cardinals" "~~/src/HOL/Library/Countable"
begin
@@ -273,6 +273,45 @@
shows "countable {a \<in> A. \<phi> a}"
by (metis Collect_conj_eq Int_absorb Int_commute Int_def assms contable_IntR)
+lemma countable_Plus[simp]:
+assumes A: "countable A" and B: "countable B"
+shows "countable (A <+> B)"
+proof-
+ let ?U = "UNIV::nat set"
+ have "|A| \<le>o |?U|" and "|B| \<le>o |?U|" using A B
+ using card_of_nat[THEN ordIso_symmetric] ordLeq_ordIso_trans
+ unfolding countable_def by blast+
+ hence "|A <+> B| \<le>o |?U|" by (intro card_of_Plus_ordLeq_infinite) auto
+ thus ?thesis using card_of_nat unfolding countable_def by(rule ordLeq_ordIso_trans)
+qed
+
+lemma countable_Times[simp]:
+assumes A: "countable A" and B: "countable B"
+shows "countable (A \<times> B)"
+proof-
+ let ?U = "UNIV::nat set"
+ have "|A| \<le>o |?U|" and "|B| \<le>o |?U|" using A B
+ using card_of_nat[THEN ordIso_symmetric] ordLeq_ordIso_trans
+ unfolding countable_def by blast+
+ hence "|A \<times> B| \<le>o |?U|" by (intro card_of_Times_ordLeq_infinite) auto
+ thus ?thesis using card_of_nat unfolding countable_def by(rule ordLeq_ordIso_trans)
+qed
+
+lemma ordLeq_countable:
+assumes "|A| \<le>o |B|" and "countable B"
+shows "countable A"
+using assms unfolding countable_def by(rule ordLeq_transitive)
+
+lemma ordLess_countable:
+assumes A: "|A| <o |B|" and B: "countable B"
+shows "countable A"
+by (rule ordLeq_countable[OF ordLess_imp_ordLeq[OF A] B])
+
+lemma countable_def2: "countable A \<longleftrightarrow> |A| \<le>o |UNIV :: nat set|"
+unfolding countable_def using card_of_nat[THEN ordIso_symmetric]
+by (metis (lifting) Field_card_of Field_natLeq card_of_mono2 card_of_nat
+ countable_def ordIso_imp_ordLeq ordLeq_countable)
+
subsection{* The type of countable sets *}
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Wed Sep 19 12:11:09 2012 +0200
@@ -145,8 +145,8 @@
and s8 = S8 nat
*)
-data ('a, 'b) bar = BAR "'b \<Rightarrow> 'a"
-data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
+data ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
+data ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
data 'a dead_foo = A
data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
--- a/src/HOL/Codatatype/More_BNFs.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/More_BNFs.thy Wed Sep 19 12:11:09 2012 +0200
@@ -22,7 +22,7 @@
lemma option_rec_conv_option_case: "option_rec = option_case"
by (simp add: fun_eq_iff split: option.split)
-bnf_def option = Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
+bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
proof -
show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
next
@@ -190,7 +190,7 @@
qed
qed
-bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
+bnf_def map [set] "\<lambda>_::'a list. natLeq" ["[]"]
proof -
show "map id = id" by (rule List.map.id)
next
@@ -355,7 +355,7 @@
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
-bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
+bnf_def map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
proof -
show "map_fset id = id"
unfolding map_fset_def2 map_id o_id afset_rfset_id ..
@@ -432,8 +432,8 @@
qed auto
lemma fset_pred[simp]: "fset_pred R a b \<longleftrightarrow>
- ((\<forall>t \<in> fset a. (\<exists>u \<in> fset b. R t u)) \<and>
- (\<forall>t \<in> fset b. (\<exists>u \<in> fset a. R u t)))" (is "?L = ?R")
+ ((\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
+ (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t))" (is "?L = ?R")
proof
assume ?L thus ?R unfolding fset_rel_def fset_pred_def
Gr_def relcomp_unfold converse_unfold
@@ -511,7 +511,7 @@
finally show ?thesis .
qed
-bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
+bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
proof -
show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
next
@@ -575,9 +575,75 @@
qed
qed (unfold cEmp_def, auto)
+lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
+apply (rule f_the_inv_into_f)
+unfolding inj_on_def rcset_inj using rcset_surj by auto
+
+lemma Collect_Int_Times:
+"{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
+by auto
+
+lemma cset_pred[simp]: "cset_pred R a b \<longleftrightarrow>
+ ((\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
+ (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t))" (is "?L = ?R")
+proof
+ assume ?L thus ?R unfolding cset_rel_def cset_pred_def
+ Gr_def relcomp_unfold converse_unfold
+ apply (simp add: subset_eq Ball_def)
+ apply (rule conjI)
+ apply (clarsimp, metis (lifting, no_types) cset.set_natural' image_iff surjective_pairing)
+ apply (clarsimp)
+ by (metis Domain.intros Range.simps cset.set_natural' fst_eq_Domain snd_eq_Range)
+next
+ assume ?R
+ def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
+ (is "the_inv rcset ?R'")
+ have "countable ?R'" by auto
+ hence *: "rcset R' = ?R'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset)
+ show ?L unfolding cset_rel_def cset_pred_def Gr_def relcomp_unfold converse_unfold
+ proof (intro CollectI prod_caseI exI conjI)
+ have "rcset a = fst ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?A")
+ using conjunct1[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times)
+ hence "a = acset ?A" by (metis acset_rcset)
+ thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto
+ have "rcset b = snd ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?B")
+ using conjunct2[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times)
+ hence "b = acset ?B" by (metis acset_rcset)
+ thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto
+ qed (auto simp add: *)
+qed
+
(* Multisets *)
+(* The cardinal of a mutiset: this, and the following basic lemmas about it,
+should eventually go into Multiset.thy *)
+definition "mcard M \<equiv> setsum (count M) {a. count M a > 0}"
+
+lemma mcard_emp[simp]: "mcard {#} = 0"
+unfolding mcard_def by auto
+
+lemma mcard_emp_iff[simp]: "mcard M = 0 \<longleftrightarrow> M = {#}"
+unfolding mcard_def apply safe
+ apply simp_all
+ by (metis multi_count_eq zero_multiset.rep_eq)
+
+lemma mcard_singl[simp]: "mcard {#a#} = Suc 0"
+unfolding mcard_def by auto
+
+lemma mcard_Plus[simp]: "mcard (M + N) = mcard M + mcard N"
+proof-
+ have "setsum (count M) {a. 0 < count M a + count N a} =
+ setsum (count M) {a. a \<in># M}"
+ apply(rule setsum_mono_zero_cong_right) by auto
+ moreover
+ have "setsum (count N) {a. 0 < count M a + count N a} =
+ setsum (count N) {a. a \<in># N}"
+ apply(rule setsum_mono_zero_cong_right) by auto
+ ultimately show ?thesis
+ unfolding mcard_def count_union[THEN ext] comm_monoid_add_class.setsum.F_fun_f by simp
+qed
+
lemma setsum_gt_0_iff:
fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
@@ -797,7 +863,7 @@
\<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
\<longrightarrow> b1 = b1' \<and> b2 = b2'"
-lemma matrix_count_finite:
+lemma matrix_setsum_finite:
assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
and ss: "setsum N1 B1 = setsum N2 B2"
shows "\<exists> M :: 'a \<Rightarrow> nat.
@@ -1001,8 +1067,8 @@
hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = N1 b1) \<and>
(\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = N2 b2)"
unfolding sset_def
- using matrix_count_finite[OF set1_NE[OF c] fin_set1[OF c]
- set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
+ using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c]
+ set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
}
then obtain Ms where
ss1: "\<And> c b1. \<lbrakk>c \<in> supp P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
@@ -1131,11 +1197,11 @@
qed
qed
-definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
-"mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
+definition multiset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
+"multiset_map h = Abs_multiset \<circ> mmap h \<circ> count"
-bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
-unfolding mset_map_def
+bnf_def multiset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
+unfolding multiset_map_def
proof -
show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
next
@@ -1191,4 +1257,227 @@
qed
qed (unfold set_of_empty, auto)
+inductive multiset_pred' where
+Zero: "multiset_pred' R {#} {#}"
+|
+Plus: "\<lbrakk>R a b; multiset_pred' R M N\<rbrakk> \<Longrightarrow> multiset_pred' R (M + {#a#}) (N + {#b#})"
+
+lemma multiset_map_Zero_iff[simp]: "multiset_map f M = {#} \<longleftrightarrow> M = {#}"
+by (metis image_is_empty multiset.set_natural' set_of_eq_empty_iff)
+
+lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp
+
+lemma multiset_pred_Zero: "multiset_pred R {#} {#}"
+unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto
+
+declare multiset.count[simp]
+declare mmap[simp]
+declare Abs_multiset_inverse[simp]
+declare multiset.count_inverse[simp]
+declare union_preserves_multiset[simp]
+
+lemma mmap_Plus[simp]:
+assumes "K \<in> multiset" and "L \<in> multiset"
+shows "mmap f (\<lambda>a. K a + L a) a = mmap f K a + mmap f L a"
+proof-
+ have "{aa. f aa = a \<and> (0 < K aa \<or> 0 < L aa)} \<subseteq>
+ {aa. 0 < K aa} \<union> {aa. 0 < L aa}" (is "?C \<subseteq> ?A \<union> ?B") by auto
+ moreover have "finite (?A \<union> ?B)" apply(rule finite_UnI)
+ using assms unfolding multiset_def by auto
+ ultimately have C: "finite ?C" using finite_subset by blast
+ have "setsum K {aa. f aa = a \<and> 0 < K aa} = setsum K {aa. f aa = a \<and> 0 < K aa + L aa}"
+ apply(rule setsum_mono_zero_cong_left) using C by auto
+ moreover
+ have "setsum L {aa. f aa = a \<and> 0 < L aa} = setsum L {aa. f aa = a \<and> 0 < K aa + L aa}"
+ apply(rule setsum_mono_zero_cong_left) using C by auto
+ ultimately show ?thesis
+ unfolding mmap_def unfolding comm_monoid_add_class.setsum.F_fun_f by auto
+qed
+
+lemma multiset_map_Plus[simp]:
+"multiset_map f (M1 + M2) = multiset_map f M1 + multiset_map f M2"
+unfolding multiset_map_def
+apply(subst multiset.count_inject[symmetric])
+unfolding plus_multiset.rep_eq comp_def by auto
+
+lemma multiset_map_singl[simp]: "multiset_map f {#a#} = {#f a#}"
+proof-
+ have 0: "\<And> b. card {aa. a = aa \<and> (a = aa \<longrightarrow> f aa = b)} =
+ (if b = f a then 1 else 0)" by auto
+ thus ?thesis
+ unfolding multiset_map_def comp_def mmap_def[abs_def] map_fun_def
+ by (simp, simp add: single_def)
+qed
+
+lemma multiset_pred_Plus:
+assumes ab: "R a b" and MN: "multiset_pred R M N"
+shows "multiset_pred R (M + {#a#}) (N + {#b#})"
+proof-
+ {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
+ hence "\<exists>ya. multiset_map fst y + {#a#} = multiset_map fst ya \<and>
+ multiset_map snd y + {#b#} = multiset_map snd ya \<and>
+ set_of ya \<subseteq> {(x, y). R x y}"
+ apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
+ }
+ thus ?thesis
+ using assms
+ unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by force
+qed
+
+lemma multiset_pred'_imp_multiset_pred:
+"multiset_pred' R M N \<Longrightarrow> multiset_pred R M N"
+apply(induct rule: multiset_pred'.induct)
+using multiset_pred_Zero multiset_pred_Plus by auto
+
+lemma mcard_multiset_map[simp]: "mcard (multiset_map f M) = mcard M"
+proof-
+ def A \<equiv> "\<lambda> b. {a. f a = b \<and> a \<in># M}"
+ let ?B = "{b. 0 < setsum (count M) (A b)}"
+ have "{b. \<exists>a. f a = b \<and> a \<in># M} \<subseteq> f ` {a. a \<in># M}" by auto
+ moreover have "finite (f ` {a. a \<in># M})" apply(rule finite_imageI)
+ using finite_Collect_mem .
+ ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
+ have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
+ by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54)
+ setsum_gt_0_iff setsum_infinite)
+ have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
+ apply safe
+ apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
+ by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff)
+ hence AB: "A ` ?B = {A b | b. \<exists> a \<in> A b. count M a > 0}" by auto
+
+ have "setsum (\<lambda> x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B"
+ unfolding comp_def ..
+ also have "... = (\<Sum>x\<in> A ` ?B. setsum (count M) x)"
+ unfolding comm_monoid_add_class.setsum_reindex[OF i, symmetric] ..
+ also have "... = setsum (count M) (\<Union>x\<in>A ` {b. 0 < setsum (count M) (A b)}. x)"
+ (is "_ = setsum (count M) ?J")
+ apply(rule comm_monoid_add_class.setsum_UN_disjoint[symmetric])
+ using 0 fin unfolding A_def by (auto intro!: finite_imageI)
+ also have "?J = {a. a \<in># M}" unfolding AB unfolding A_def by auto
+ finally have "setsum (\<lambda> x. setsum (count M) (A x)) ?B =
+ setsum (count M) {a. a \<in># M}" .
+ thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def)
+qed
+
+lemma multiset_pred_mcard:
+assumes "multiset_pred R M N"
+shows "mcard M = mcard N"
+using assms unfolding multiset_pred_def multiset_rel_def relcomp_unfold Gr_def by auto
+
+lemma multiset_induct2[case_names empty addL addR]:
+assumes empty: "P {#} {#}"
+and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
+and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
+shows "P M N"
+apply(induct N rule: multiset_induct)
+ apply(induct M rule: multiset_induct, rule empty, erule addL)
+ apply(induct M rule: multiset_induct, erule addR, erule addR)
+done
+
+lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
+assumes c: "mcard M = mcard N"
+and empty: "P {#} {#}"
+and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
+shows "P M N"
+using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
+ case (less M) show ?case
+ proof(cases "M = {#}")
+ case True hence "N = {#}" using less.prems by auto
+ thus ?thesis using True empty by auto
+ next
+ case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
+ have "N \<noteq> {#}" using False less.prems by auto
+ then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
+ have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
+ thus ?thesis using M N less.hyps add by auto
+ qed
+qed
+
+lemma msed_map_invL:
+assumes "multiset_map f (M + {#a#}) = N"
+shows "\<exists> N1. N = N1 + {#f a#} \<and> multiset_map f M = N1"
+proof-
+ have "f a \<in># N"
+ using assms multiset.set_natural'[of f "M + {#a#}"] by auto
+ then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
+ have "multiset_map f M = N1" using assms unfolding N by simp
+ thus ?thesis using N by blast
+qed
+
+lemma msed_map_invR:
+assumes "multiset_map f M = N + {#b#}"
+shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> multiset_map f M1 = N"
+proof-
+ obtain a where a: "a \<in># M" and fa: "f a = b"
+ using multiset.set_natural'[of f M] unfolding assms
+ by (metis image_iff mem_set_of_iff union_single_eq_member)
+ then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
+ have "multiset_map f M1 = N" using assms unfolding M fa[symmetric] by simp
+ thus ?thesis using M fa by blast
+qed
+
+lemma msed_pred_invL:
+assumes "multiset_pred R (M + {#a#}) N"
+shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> multiset_pred R M N1"
+proof-
+ obtain K where KM: "multiset_map fst K = M + {#a#}"
+ and KN: "multiset_map snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
+ using assms
+ unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto
+ obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
+ and K1M: "multiset_map fst K1 = M" using msed_map_invR[OF KM] by auto
+ obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "multiset_map snd K1 = N1"
+ using msed_map_invL[OF KN[unfolded K]] by auto
+ have Rab: "R a (snd ab)" using sK a unfolding K by auto
+ have "multiset_pred R M N1" using sK K1M K1N1
+ unfolding K multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto
+ thus ?thesis using N Rab by auto
+qed
+
+lemma msed_pred_invR:
+assumes "multiset_pred R M (N + {#b#})"
+shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> multiset_pred R M1 N"
+proof-
+ obtain K where KN: "multiset_map snd K = N + {#b#}"
+ and KM: "multiset_map fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
+ using assms
+ unfolding multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto
+ obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
+ and K1N: "multiset_map snd K1 = N" using msed_map_invR[OF KN] by auto
+ obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "multiset_map fst K1 = M1"
+ using msed_map_invL[OF KM[unfolded K]] by auto
+ have Rab: "R (fst ab) b" using sK b unfolding K by auto
+ have "multiset_pred R M1 N" using sK K1N K1M1
+ unfolding K multiset_pred_def multiset_rel_def Gr_def relcomp_unfold by auto
+ thus ?thesis using M Rab by auto
+qed
+
+lemma multiset_pred_imp_multiset_pred':
+assumes "multiset_pred R M N"
+shows "multiset_pred' R M N"
+using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
+ case (less M)
+ have c: "mcard M = mcard N" using multiset_pred_mcard[OF less.prems] .
+ show ?case
+ proof(cases "M = {#}")
+ case True hence "N = {#}" using c by simp
+ thus ?thesis using True multiset_pred'.Zero by auto
+ next
+ case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
+ obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "multiset_pred R M1 N1"
+ using msed_pred_invL[OF less.prems[unfolded M]] by auto
+ have "multiset_pred' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
+ thus ?thesis using multiset_pred'.Plus[of R a b, OF R] unfolding M N by simp
+ qed
+qed
+
+lemma multiset_pred_multiset_pred':
+"multiset_pred R M N = multiset_pred' R M N"
+using multiset_pred_imp_multiset_pred' multiset_pred'_imp_multiset_pred by auto
+
+(* The main end product for multiset_pred: inductive characterization *)
+theorems multiset_pred_induct[case_names empty add, induct pred: multiset_pred] =
+ multiset_pred'.induct[unfolded multiset_pred_multiset_pred'[symmetric]]
+
end
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Wed Sep 19 12:11:09 2012 +0200
@@ -15,7 +15,7 @@
val rel_unfolds_of: unfold_thms -> thm list
val pred_unfolds_of: unfold_thms -> thm list
- val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) ->
+ val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
(BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
val default_comp_sort: (string * sort) list list -> (string * sort) list
@@ -68,10 +68,10 @@
val bdTN = "bdT";
-fun mk_killN n = "kill" ^ string_of_int n ^ "_";
-fun mk_liftN n = "lift" ^ string_of_int n ^ "_";
+fun mk_killN n = "_kill" ^ string_of_int n;
+fun mk_liftN n = "_lift" ^ string_of_int n;
fun mk_permuteN src dest =
- "permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest) ^ "_";
+ "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
val no_thm = refl;
val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
@@ -286,7 +286,7 @@
fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
let
- val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
+ val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
val live = live_of_bnf bnf;
val dead = dead_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
@@ -385,7 +385,7 @@
fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
let
- val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
+ val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
val live = live_of_bnf bnf;
val dead = dead_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
@@ -474,7 +474,7 @@
fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
let
- val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf);
+ val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
val live = live_of_bnf bnf;
val dead = dead_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
@@ -590,15 +590,9 @@
fun default_comp_sort Ass =
Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
-fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) =
+fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) =
let
- val name = Binding.name_of b;
- fun qualify i bind =
- let val namei = if i > 0 then name ^ string_of_int i else name;
- in
- if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
- else qualify' (Binding.prefix_name namei bind)
- end;
+ val b = name_of_bnf outer;
val Ass = map (map Term.dest_TFree) tfreess;
val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
@@ -609,7 +603,8 @@
val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
val As = map TFree As;
in
- apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy'))
+ apfst (rpair (Ds, As))
+ (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy'))
end;
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
@@ -682,7 +677,9 @@
fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
- val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads)
+ val policy = user_policy Derive_All_Facts;
+
+ val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
@@ -707,11 +704,11 @@
((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
end;
-fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
+fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
(SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
- | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
- | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
+ | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
+ | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
let
val tfrees = Term.add_tfreesT T [];
val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
@@ -734,13 +731,10 @@
in ((bnf, deads_lives), (unfold', lthy)) end
else
let
- val name = Binding.name_of b;
- fun qualify i bind =
- let val namei = if i > 0 then name ^ string_of_int i else name;
- in
- if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
- else qualify' (Binding.prefix_name namei bind)
- end;
+ val name = Long_Name.base_name C;
+ fun qualify i =
+ let val namei = name ^ nonzero_string_of_int i;
+ in qualify' o Binding.qualify true namei end;
val odead = dead_of_bnf bnf;
val olive = live_of_bnf bnf;
val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
@@ -749,11 +743,10 @@
val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
val ((inners, (Dss, Ass)), (unfold', lthy')) =
apfst (apsnd split_list o split_list)
- (fold_map2 (fn i =>
- bnf_of_typ Smart_Inline (Binding.name (name ^ string_of_int i)) (qualify i) sort)
+ (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
(if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy));
in
- compose_bnf const_policy (qualify 0) b sort bnf inners oDs Dss Ass (unfold', lthy')
+ compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy')
end)
end;
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Wed Sep 19 12:11:09 2012 +0200
@@ -12,6 +12,8 @@
type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
val bnf_of: Proof.context -> string -> BNF option
+ val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
+
val name_of_bnf: BNF -> binding
val T_of_bnf: BNF -> typ
val live_of_bnf: BNF -> int
@@ -80,7 +82,7 @@
datatype fact_policy =
Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
val bnf_note_all: bool Config.T
- val user_policy: Proof.context -> fact_policy
+ val user_policy: fact_policy -> Proof.context -> fact_policy
val print_bnfs: Proof.context -> unit
val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
@@ -461,9 +463,6 @@
(* Names *)
-fun nonzero_string_of_int 0 = ""
- | nonzero_string_of_int n = string_of_int n;
-
val mapN = "map";
val setN = "set";
fun mk_setN i = setN ^ nonzero_string_of_int i;
@@ -506,8 +505,8 @@
val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
-fun user_policy ctxt =
- if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else Derive_All_Facts_Note_Most;
+fun user_policy policy ctxt =
+ if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else policy;
val smart_max_inline_size = 25; (*FUDGE*)
@@ -543,6 +542,18 @@
| _ => error "Bad bound constant");
val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
+ fun err T =
+ error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
+ " as unnamed BNF");
+
+ val (b, key) =
+ if Binding.eq_name (b, Binding.empty) then
+ (case bd_rhsT of
+ Type (C, Ts) => if forall (is_some o try dest_TFree) Ts
+ then (Binding.qualified_name C, C) else err bd_rhsT
+ | T => err T)
+ else (b, Local_Theory.full_name no_defs_lthy b);
+
val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
val set_binds_defs =
let
@@ -627,12 +638,6 @@
| SOME Ds => map (Morphism.typ phi) Ds);
val dead = length deads;
- (*FIXME: check DUP here, not in after_qed*)
- val key =
- (case (CA, Binding.eq_name (qualify b, b)) of
- (Type (C, _), true) => C
- | _ => Name_Space.full_name Name_Space.default_naming b);
-
(*TODO: further checks of type of bnf_map*)
(*TODO: check types of bnf_sets*)
(*TODO: check type of bnf_bd*)
@@ -1155,18 +1160,20 @@
[(thms, [])]));
in
Local_Theory.notes notes #> snd
- #> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
end
else
I))
end;
in
- (goals, wit_goalss, after_qed, lthy', one_step_defs)
+ (key, goals, wit_goalss, after_qed, lthy', one_step_defs)
end;
+fun register_bnf key (bnf, lthy) =
+ (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy);
+
fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
- (fn (goals, wit_goalss, after_qed, lthy, defs) =>
+ (fn (_, goals, wit_goalss, after_qed, lthy, defs) =>
let
val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac;
val wit_goals = wit_goalss |> map Logic.mk_conjunction_balanced;
@@ -1182,11 +1189,11 @@
|> (fn thms => after_qed (map single thms @ wit_thms) lthy)
end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
-val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
+val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
Proof.unfolding ([[(defs, [])]])
- (Proof.theorem NONE (snd oo after_qed)
+ (Proof.theorem NONE (snd o register_bnf key oo after_qed)
(map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
- prepare_def Do_Inline user_policy I Syntax.read_term NONE;
+ prepare_def Do_Inline (user_policy Derive_All_Facts_Note_Most) I Syntax.read_term NONE;
fun print_bnfs ctxt =
let
@@ -1219,7 +1226,7 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
- (((Parse.binding --| @{keyword "="}) -- Parse.term --
+ ((parse_opt_binding_colon -- Parse.term --
(@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
(@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd);
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 19 12:11:09 2012 +0200
@@ -34,9 +34,8 @@
val simp_attrs = @{attributes [simp]};
-fun split_list10 xs =
- (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
- map #9 xs, map #10 xs);
+fun split_list8 xs =
+ (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
fun resort_tfree S (TFree (s, _)) = TFree (s, S);
@@ -406,7 +405,7 @@
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
- fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) =
+ fun define_iter_rec (wrap_res, no_defs_lthy) =
let
val fpT_to_C = fpT --> C;
@@ -438,10 +437,10 @@
val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
- ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy)
+ ((wrap_res, ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
end;
- fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) =
+ fun define_coiter_corec (wrap_res, no_defs_lthy) =
let
val B_to_fpT = C --> fpT;
@@ -478,8 +477,7 @@
val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
- ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def),
- lthy)
+ ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
end;
fun wrap lthy =
@@ -499,11 +497,13 @@
val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
fun mk_map live Ts Us t =
- let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
+ let
+ val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last
+ in
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
- fun build_map build_arg (T as Type (s, Ts)) (U as Type (_, Us)) =
+ fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
let
val bnf = the (bnf_of lthy s);
val live = live_of_bnf bnf;
@@ -512,9 +512,13 @@
val args = map build_arg TUs;
in Term.list_comb (mapx, args) end;
- fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _,
+ 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_predT fpTs)
@@ -588,30 +592,22 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry (op $)) phis vs)));
- fun mk_raw_prem_prems_indices pprems =
- let
- fun has_index kk (_, (kk', _)) = kk' = kk;
- val buckets = Library.partition_list has_index 1 nn pprems;
- val pps = map length buckets;
- in
- map (fn pprem as (xysets, (kk, _)) =>
- ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1),
- (length xysets, kk))) pprems
- end;
-
- val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
+ val kksss = map (map (map (fst o snd) o #2)) raw_premss;
val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
val induct_thm =
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_induct_tac ctxt ns mss ppjjqqkksss (flat ctr_defss) fld_induct'
+ mk_induct_tac ctxt ns mss kksss (flat ctr_defss) fld_induct'
nested_set_natural's pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
in
`(conj_dests nn) induct_thm
end;
+ (* TODO: Generate nicer names in case of clashes *)
+ val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
+
val (iter_thmss, rec_thmss) =
let
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
@@ -660,26 +656,39 @@
goal_recss 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 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));
+
val common_notes =
- (if nn > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
+ (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, [])]));
val notes =
- [(inductN, map single induct_thms, []), (* FIXME: attribs *)
- (itersN, iter_thmss, simp_attrs),
- (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)]
+ [(inductN, map single induct_thms,
+ fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
+ (itersN, iter_thmss, K simp_attrs),
+ (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
+ (simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
- map2 (fn b => fn thms =>
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
- [(thms, [])])) fp_bs thmss);
+ map3 (fn b => fn Type (T_name, _) => fn thms =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
+ [(thms, [])])) fp_bs fpTs thmss);
in
lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
- fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
- discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
+ 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 (vs', _) =
lthy
|> Variable.variant_fixes (map Binding.name_of fp_bs);
@@ -768,9 +777,9 @@
end;
val sel_coiter_thmsss =
- map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_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 selsss sel_thmsss;
+ map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss0 sel_thmsss;
val common_notes =
(if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
@@ -794,7 +803,7 @@
end;
fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
- fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10
+ fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8
val lthy' = lthy
|> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
@@ -814,12 +823,9 @@
val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
-val parse_binding_colon = Parse.binding --| @{keyword ":"};
-val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding;
-
val parse_ctr_arg =
@{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
- (Parse.typ >> pair no_binding);
+ (Parse.typ >> pair Binding.empty);
val parse_defaults =
@{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Wed Sep 19 12:11:09 2012 +0200
@@ -13,9 +13,8 @@
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
- val mk_induct_tac: Proof.context -> int list -> int list list ->
- ((int * int) * (int * int)) list list list -> thm list -> thm -> thm list -> thm list list ->
- tactic
+ val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list ->
+ thm -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> tactic
val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
end;
@@ -88,53 +87,40 @@
Local_Defs.unfold_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
-(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
-
-fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
- | mk_induct_prem_prem_endgame_tac ctxt qq =
- REPEAT_DETERM_N qq o
- (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
- etac @{thm induct_set_step}) THEN'
- atac ORELSE' SELECT_GOAL (auto_tac ctxt);
+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'
+ (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
val induct_prem_prem_thms =
- @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
- Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv
- snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps};
+ @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
+ Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
+ mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
-(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
- delay them. *)
-val induct_prem_prem_thms_delayed =
- @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
-
-fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
- EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
- [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
+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 (Local_Defs.unfold_tac ctxt
(pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
- SELECT_GOAL (Local_Defs.unfold_tac ctxt
- (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
- rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
- SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1;
+ solve_prem_prem_tac]) (rev kks)) 1;
-fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
- let val r = length ppjjqqkks in
+fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
+ let val r = length kks in
EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
EVERY [REPEAT_DETERM_N r
(rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1,
- mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs]
+ mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs]
end;
-fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss =
+fun mk_induct_tac ctxt ns mss kkss ctr_defs fld_induct' set_natural's pre_set_defss =
let
val nn = length ns;
val n = Integer.sum ns;
in
Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
- pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
+ pre_set_defss mss (unflat mss (1 upto n)) kkss)
end;
end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 19 12:11:09 2012 +0200
@@ -62,6 +62,7 @@
val sel_corecsN: string
val set_inclN: string
val set_set_inclN: string
+ val simpsN: string
val strTN: string
val str_initN: string
val sum_bdN: string
@@ -164,6 +165,7 @@
val coiterN = coN ^ iterN
val coitersN = coiterN ^ "s"
val uniqueN = "_unique"
+val simpsN = "simps"
val fldN = "fld"
val unfN = "unf"
val fld_iterN = fldN ^ "_" ^ iterN
@@ -173,7 +175,7 @@
val fld_iter_uniqueN = fld_iterN ^ uniqueN
val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s"
-val map_simpsN = mapN ^ "_simps"
+val map_simpsN = mapN ^ "_" ^ simpsN
val map_uniqueN = mapN ^ uniqueN
val min_algN = "min_alg"
val morN = "mor"
@@ -187,7 +189,7 @@
val LevN = "Lev"
val rvN = "recover"
val behN = "beh"
-fun mk_set_simpsN i = mk_setN i ^ "_simps"
+fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN
fun mk_set_minimalN i = mk_setN i ^ "_minimal"
fun mk_set_inductN i = mk_setN i ^ "_induct"
@@ -375,12 +377,9 @@
fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
let
val name = mk_common_name bs;
- fun qualify i bind =
- let val namei = if i > 0 then name ^ string_of_int i else name;
- in
- if member (op =) (#2 (Binding.dest bind)) (namei, true) then bind
- else Binding.prefix_name namei bind
- end;
+ fun qualify i =
+ let val namei = name ^ nonzero_string_of_int i;
+ in Binding.qualify true namei end;
val Ass = map (map dest_TFree) livess;
val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
@@ -415,8 +414,9 @@
val timer = time (Timer.startRealTimer ());
val (lhss, rhss) = split_list eqs;
val sort = fp_sort lhss (SOME resBs);
+ fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
- (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.prefix_name rawN b) I sort) bs rhss
+ (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
(empty_unfold, lthy));
in
mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
@@ -427,9 +427,10 @@
val timer = time (Timer.startRealTimer ());
val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
val sort = fp_sort lhss NONE;
+ fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
(fold_map2 (fn b => fn rawT =>
- (bnf_of_typ Smart_Inline (Binding.prefix_name rawN b) I sort (Syntax.read_typ lthy rawT)))
+ (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
bs raw_bnfs (empty_unfold, lthy));
in
snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 19 12:11:09 2012 +0200
@@ -2854,10 +2854,13 @@
val wit_tac = mk_wit_tac n unf_fld_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
+ val policy = user_policy Derive_All_Facts_Note_Most;
+
val (Jbnfs, lthy) =
- fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) =>
- bnf_def Dont_Inline user_policy I tacs (wit_tac thms) (SOME deads)
- ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
+ fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy =>
+ bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads)
+ ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+ |> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
val fold_maps = Local_Defs.fold lthy (map (fn bnf =>
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 19 12:11:09 2012 +0200
@@ -1700,10 +1700,13 @@
fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
+ val policy = user_policy Derive_All_Facts_Note_Most;
+
val (Ibnfs, lthy) =
- fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits =>
- bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
- ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
+ fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy =>
+ bnf_def Dont_Inline policy I tacs wit_tac (SOME deads)
+ ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+ |> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
val fold_maps = Local_Defs.fold lthy (map (fn bnf =>
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Wed Sep 19 12:11:09 2012 +0200
@@ -58,6 +58,7 @@
(term list * (string * typ) list) * Proof.context
val mk_Freess': string -> typ list list -> Proof.context ->
(term list list * (string * typ) list list) * Proof.context
+ val nonzero_string_of_int: int -> string
val strip_typeN: int -> typ -> typ list * typ
@@ -127,6 +128,9 @@
val certifyT: Proof.context -> typ -> ctyp
val certify: Proof.context -> term -> cterm
+ val parse_binding_colon: Token.T list -> binding * Token.T list
+ val parse_opt_binding_colon: Token.T list -> binding * Token.T list
+
val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
(binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
@@ -249,6 +253,9 @@
fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
+val parse_binding_colon = Parse.binding --| @{keyword ":"};
+val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
+
(*TODO: is this really different from Typedef.add_typedef_global?*)
fun typedef def opt_name typ set opt_morphs tac lthy =
let
@@ -286,6 +293,9 @@
(** Fresh variables **)
+fun nonzero_string_of_int 0 = ""
+ | nonzero_string_of_int n = string_of_int n;
+
val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 19 12:11:09 2012 +0200
@@ -7,13 +7,13 @@
signature BNF_WRAP =
sig
- val no_binding: binding
val mk_half_pairss: 'a list -> ('a * 'a) list list
val mk_ctr: 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 list) * local_theory
+ (term list list * thm list * thm list * thm list * thm list * thm list list) * local_theory
val parse_wrap_options: bool parser
val parse_bound_term: (binding * string) parser
end;
@@ -45,7 +45,6 @@
val split_asmN = "split_asm";
val weak_case_cong_thmsN = "weak_case_cong";
-val no_binding = @{binding ""};
val std_binding = @{binding _};
val induct_simp_attrs = @{attributes [induct_simp]};
@@ -71,14 +70,14 @@
Term.subst_atomic_types (Ts0 ~~ Ts) ctr
end;
-fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
-
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 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
@@ -111,10 +110,11 @@
val ms = map length ctr_Tss;
- val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings;
+ val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
fun can_really_rely_on_disc k =
- not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0;
+ not (Binding.eq_name (nth raw_disc_bindings' (k - 1), Binding.empty)) orelse
+ nth ms (k - 1) = 0;
fun can_rely_on_disc k =
can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
fun can_omit_disc_binding k m =
@@ -127,7 +127,7 @@
raw_disc_bindings'
|> map4 (fn k => fn m => fn ctr => fn disc =>
Option.map (Binding.qualify false (Binding.name_of data_b))
- (if Binding.eq_name (disc, no_binding) then
+ (if Binding.eq_name (disc, Binding.empty) then
if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
else if Binding.eq_name (disc, std_binding) then
SOME (std_disc_binding ctr)
@@ -143,10 +143,10 @@
pad_list [] n raw_sel_bindingss
|> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
Binding.qualify false (Binding.name_of data_b)
- (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then
+ (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
std_sel_binding m l ctr
else
- sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms;
+ sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
fun mk_case Ts T =
let
@@ -177,8 +177,8 @@
val xfs = map2 (curry Term.list_comb) fs xss;
val xgs = map2 (curry Term.list_comb) gs xss;
- val eta_fs = map2 eta_expand_case_arg xss xfs;
- val eta_gs = map2 eta_expand_case_arg xss xgs;
+ val eta_fs = map2 eta_expand_arg xss xfs;
+ val eta_gs = map2 eta_expand_arg xss xgs;
val fcase = Term.list_comb (casex, eta_fs);
val gcase = Term.list_comb (casex, eta_gs);
@@ -327,6 +327,8 @@
val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
(hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
+ 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)]
@@ -558,8 +560,8 @@
(split_thm, split_asm_thm)
end;
+ val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
- val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
val notes =
[(case_congN, [case_cong_thm], []),
@@ -571,7 +573,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]),
- (injectN, flat inject_thmss, iff_attrs @ induct_simp_attrs),
+ (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
(nchotomyN, [nchotomy_thm], []),
(selsN, all_sel_thms, simp_attrs),
(splitN, [split_thm], []),
@@ -586,7 +588,8 @@
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
in
- ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
+ ((selss, inject_thms, distinct_thms, case_thms, discI_thms, sel_thmss),
+ lthy |> Local_Theory.notes (notes' @ notes) |> snd)
end;
in
(goalss, after_qed, lthy')
--- a/src/HOL/IMP/Abs_Int1.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Sep 19 12:11:09 2012 +0200
@@ -233,7 +233,12 @@
assumes h: "m x \<le> h"
begin
-definition "m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
+definition m_st :: "'av st \<Rightarrow> nat" ("m\<^isub>s\<^isub>t") where
+"m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
+
+lemma m_st_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
+by(simp add: L_st_def m_st_def)
+ (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
lemma m_st1: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st S1 \<ge> m_st S2"
proof(auto simp add: le_st_def m_st_def)
@@ -254,15 +259,11 @@
qed
-definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" where
+definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
"m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_st S)"
-definition m_c :: "'av st option acom \<Rightarrow> nat" where
-"m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
-
-lemma m_st_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
-by(simp add: L_st_def m_st_def)
- (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
+lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)"
+by(auto simp add: m_o_def m_st_h split: option.split dest!:m_st_h)
lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
o1 \<sqsubseteq> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
@@ -286,6 +287,25 @@
case 3 thus ?case by simp
qed
+
+definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
+"m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
+
+lemma m_c_h: assumes "C \<in> L(vars(strip C))"
+shows "m_c C \<le> size(annos C) * (h * card(vars(strip C)) + 1)"
+proof-
+ let ?X = "vars(strip C)" let ?n = "card ?X" let ?a = "size(annos C)"
+ { fix i assume "i < ?a"
+ hence "annos C ! i \<in> L ?X" using assms by(simp add: L_acom_def)
+ note m_o_h[OF this finite_cvars]
+ } note 1 = this
+ have "m_c C = (\<Sum>i<?a. m_o ?n (annos C ! i))" by(simp add: m_c_def)
+ also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
+ apply(rule setsum_mono) using 1 by simp
+ also have "\<dots> = ?a * (h * ?n + 1)" by simp
+ finally show ?thesis .
+qed
+
lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow>
C1 \<sqsubset> C2 \<Longrightarrow> m_c C1 > m_c C2"
proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] L_acom_def)
--- a/src/HOL/IMP/Abs_Int1_const.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Sep 19 12:11:09 2012 +0200
@@ -133,7 +133,7 @@
interpretation Abs_Int_measure
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-and m = m_const and h = "2"
+and m = m_const and h = "1"
proof
case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
next
--- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Sep 19 12:11:09 2012 +0200
@@ -155,7 +155,7 @@
interpretation Abs_Int_measure
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-and m = m_parity and h = "2"
+and m = m_parity and h = "1"
proof
case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
next
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Sep 19 12:11:09 2012 +0200
@@ -337,9 +337,9 @@
fun count x = (length oo filter o equal) x
-fun cpu_time description e =
- let val ({cpu, ...}, result) = Timing.timing e ()
- in (result, (description, Time.toMilliseconds cpu)) end
+fun elapsed_time description e =
+ let val ({elapsed, ...}, result) = Timing.timing e ()
+ in (result, (description, Time.toMilliseconds elapsed)) end
(*
fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
@@ -352,13 +352,13 @@
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
val _ = Output.urgent_message ("Invoking " ^ mtd_name)
- val (res, timing) = (*cpu_time "total time"
- (fn () => *)case try (invoke_mtd thy) t of
- SOME (res, timing) => (res, timing)
+ val (res, timing) = elapsed_time "total time"
+ (fn () => case try (invoke_mtd thy) t of
+ SOME (res, timing) => res
| NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
- (Error, []))
+ Error))
val _ = Output.urgent_message (" Done")
- in (res, timing) end
+ in (res, [timing]) end
(* theory -> term list -> mtd -> subentry *)
@@ -445,7 +445,7 @@
"size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
fun string_of_mtd_result (mtd_name, (outcome, timing)) =
mtd_name ^ ": " ^ string_of_outcome outcome
- (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
+ ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
(*^ "\n" ^ string_of_reports reports*)
in
"mutant of " ^ thm_name ^ ":\n"
--- a/src/HOL/ROOT Wed Sep 19 12:10:40 2012 +0200
+++ b/src/HOL/ROOT Wed Sep 19 12:11:09 2012 +0200
@@ -604,7 +604,7 @@
session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
description {* Ordinals and Cardinals, Full Theories *}
- theories Cardinal_Order_Relation
+ theories Cardinals
files
"document/intro.tex"
"document/root.tex"