--- a/src/HOL/BNF/BNF_Def.thy Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy Sat Jul 13 13:03:21 2013 +0200
@@ -185,6 +185,25 @@
lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
by metis
+lemma sum_case_o_inj:
+"sum_case f g \<circ> Inl = f"
+"sum_case f g \<circ> Inr = g"
+by auto
+
+lemma card_order_csum_cone_cexp_def:
+ "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
+ unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order)
+
+lemma If_the_inv_into_in_Func:
+ "\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
+ (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
+unfolding Func_def by (auto dest: the_inv_into_into)
+
+lemma If_the_inv_into_f_f:
+ "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
+ ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
+unfolding Func_def by (auto elim: the_inv_into_f_f)
+
ML_file "Tools/bnf_def_tactics.ML"
ML_file "Tools/bnf_def.ML"
--- a/src/HOL/BNF/BNF_FP_Basic.thy Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Sat Jul 13 13:03:21 2013 +0200
@@ -100,11 +100,6 @@
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
-lemma sum_case_o_inj:
-"sum_case f g \<circ> Inl = f"
-"sum_case f g \<circ> Inr = g"
-by auto
-
lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
by blast
--- a/src/HOL/BNF/BNF_LFP.thy Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy Sat Jul 13 13:03:21 2013 +0200
@@ -215,16 +215,6 @@
lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
by auto
-lemma If_the_inv_into_in_Func:
- "\<lbrakk>inj_on g C; g ` C \<subseteq> A; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
- (\<lambda>i. if i \<in> A then if i \<in> g ` C then the_inv_into C g i else x else undefined) \<in> Func A (B \<union> {x})"
-unfolding Func_def by (auto dest: the_inv_into_into)
-
-lemma If_the_inv_into_f_f:
- "\<lbrakk>inj_on g C; g ` C \<subseteq> A; i \<in> C\<rbrakk> \<Longrightarrow>
- ((\<lambda>i. if i \<in> A then if i \<in> g ` C then the_inv_into C g i else x else undefined) o g) i = id i"
-unfolding Func_def by (auto elim: the_inv_into_f_f)
-
(*helps resolution*)
lemma well_order_induct_imp:
"wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
--- a/src/HOL/BNF/Basic_BNFs.thy Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Basic_BNFs.thy Sat Jul 13 13:03:21 2013 +0200
@@ -35,34 +35,13 @@
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
-apply (rule ordLeq_transitive)
-apply (rule ordLeq_cexp1[of natLeq])
-apply (rule Cinfinite_Cnotzero)
-apply (rule conjI)
-apply (rule natLeq_cinfinite)
-apply (rule natLeq_Card_order)
-apply (rule card_of_Card_order)
-apply (rule cexp_mono1)
-apply (rule ordLeq_csum1)
-apply (rule card_of_Card_order)
-apply (rule natLeq_Card_order)
done
bnf DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
"op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
-apply (auto simp add: wpull_Grp_def Grp_def
+by (auto simp add: wpull_Grp_def Grp_def
card_order_csum natLeq_card_order card_of_card_order_on
cinfinite_csum natLeq_cinfinite)
-apply (rule ordLess_imp_ordLeq)
-apply (rule ordLess_ordLeq_trans)
-apply (rule ordLess_ctwo_cexp)
-apply (rule card_of_Card_order)
-apply (rule cexp_mono2'')
-apply (rule ordLeq_csum2)
-apply (rule card_of_Card_order)
-apply (rule ctwo_Cnotzero)
-apply (rule card_of_Card_order)
-done
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
"setl x = (case x of Inl z => {z} | _ => {})"
@@ -119,32 +98,6 @@
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: setr_def split: sum.split)
next
- fix A1 :: "'a set" and A2 :: "'b set"
- have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and>
- (case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R")
- proof safe
- fix x :: "'a + 'b"
- assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2"
- hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+
- thus "x \<in> A1 <+> A2" by blast
- qed (auto split: sum.split)
- show "|{x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}| \<le>o
- (( |A1| +c |A2| ) +c ctwo) ^c natLeq"
- apply (rule ordIso_ordLeq_trans)
- apply (rule card_of_ordIso_subst)
- apply (unfold sum_set_defs)
- apply (rule in_alt)
- apply (rule ordIso_ordLeq_trans)
- apply (rule Plus_csum)
- apply (rule ordLeq_transitive)
- apply (rule ordLeq_csum1)
- apply (rule Card_order_csum)
- apply (rule ordLeq_cexp1)
- apply (rule conjI)
- using Field_natLeq UNIV_not_empty czeroE apply fast
- apply (rule natLeq_Card_order)
- by (rule Card_order_csum)
-next
fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
hence
@@ -195,16 +148,6 @@
by (fastforce split: sum.splits)
qed (auto simp: sum_set_defs)
-lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq"
- apply (rule ordLeq_transitive)
- apply (rule ordLeq_cprod2)
- apply (rule ctwo_Cnotzero)
- apply (auto simp: Field_card_of intro: card_of_card_order_on)
- apply (rule cprod_mono2)
- apply (rule ordLess_imp_ordLeq)
- apply (unfold finite_iff_ordLess_natLeq[symmetric])
- by simp
-
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
"fsts x = {fst x}"
@@ -216,7 +159,7 @@
definition prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
"prod_rel \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
-bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
+bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. natLeq" [Pair] prod_rel
proof (unfold prod_set_defs)
show "map_pair id id = id" by (rule map_pair.id)
next
@@ -236,48 +179,17 @@
show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
by (rule ext, unfold o_apply) simp
next
- show "card_order (ctwo *c natLeq)"
- apply (rule card_order_cprod)
- apply (rule ctwo_card_order)
- by (rule natLeq_card_order)
+ show "card_order natLeq" by (rule natLeq_card_order)
next
- show "cinfinite (ctwo *c natLeq)"
- apply (rule cinfinite_cprod2)
- apply (rule ctwo_Cnotzero)
- apply (rule conjI[OF _ natLeq_Card_order])
- by (rule natLeq_cinfinite)
-next
- fix x
- show "|{fst x}| \<le>o ctwo *c natLeq"
- by (rule singleton_ordLeq_ctwo_natLeq)
+ show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix x
- show "|{snd x}| \<le>o ctwo *c natLeq"
- by (rule singleton_ordLeq_ctwo_natLeq)
+ show "|{fst x}| \<le>o natLeq"
+ by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
next
- fix A1 :: "'a set" and A2 :: "'b set"
- have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto
- show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o
- ( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)"
- apply (rule ordIso_ordLeq_trans)
- apply (rule card_of_ordIso_subst)
- apply (rule in_alt)
- apply (rule ordIso_ordLeq_trans)
- apply (rule Times_cprod)
- apply (rule ordLeq_transitive)
- apply (rule cprod_csum_cexp)
- apply (rule cexp_mono)
- apply (rule ordLeq_csum1)
- apply (rule Card_order_csum)
- apply (rule ordLeq_cprod1)
- apply (rule Card_order_ctwo)
- apply (rule Cinfinite_Cnotzero)
- apply (rule conjI[OF _ natLeq_Card_order])
- apply (rule natLeq_cinfinite)
- apply (rule notE)
- apply (rule ctwo_not_czero)
- apply assumption
- by (rule Card_order_ctwo)
+ fix x
+ show "|{snd x}| \<le>o natLeq"
+ by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
next
fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
@@ -360,22 +272,6 @@
also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
finally show "|range f| \<le>o natLeq +c ?U" .
next
- fix B :: "'a set"
- have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range)
- also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|"
- unfolding cexp_def Field_card_of by (rule card_of_refl)
- also have "|B| ^c |UNIV :: 'd set| \<le>o
- ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )"
- apply (rule cexp_mono)
- apply (rule ordLeq_csum1) apply (rule card_of_Card_order)
- apply (rule ordLeq_csum2) apply (rule card_of_Card_order)
- apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast
- apply (rule card_of_Card_order)
- done
- finally
- show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o
- ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" .
-next
fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
(op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
--- a/src/HOL/BNF/More_BNFs.thy Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Sat Jul 13 13:03:21 2013 +0200
@@ -47,24 +47,6 @@
show "|Option.set x| \<le>o natLeq"
by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
next
- fix A
- have unfold: "{x. Option.set x \<subseteq> A} = Some ` A \<union> {None}"
- by (auto simp add: option_rec_conv_option_case Option.set_def split: option.split_asm)
- show "|{x. Option.set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
- apply (rule ordIso_ordLeq_trans)
- apply (rule card_of_ordIso_subst[OF unfold])
- apply (rule ordLeq_transitive)
- apply (rule Un_csum)
- apply (rule ordLeq_transitive)
- apply (rule csum_mono)
- apply (rule card_of_image)
- apply (rule ordIso_ordLeq_trans)
- apply (rule single_cone)
- apply (rule cone_ordLeq_ctwo)
- apply (rule ordLeq_cexp1)
- apply (simp_all add: natLeq_cinfinite natLeq_Card_order cinfinite_not_czero Card_order_csum)
- done
-next
fix A B1 B2 f1 f2 p1 p2
assume wpull: "wpull A B1 B2 f1 f2 p1 p2"
show "wpull {x. Option.set x \<subseteq> A} {x. Option.set x \<subseteq> B1} {x. Option.set x \<subseteq> B2}
@@ -119,68 +101,6 @@
apply (metis Field_card_of czeroE)
by (rule card_of_Card_order)
-lemma list_in_bd: "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
-proof -
- fix A :: "'a set"
- show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
- proof (cases "A = {}")
- case False thus ?thesis
- apply -
- apply (rule ordLeq_transitive)
- apply (rule card_of_list_in)
- apply (rule ordLeq_transitive)
- apply (erule card_of_Pfunc_Pow_Func_option)
- apply (rule ordIso_ordLeq_trans)
- apply (rule Times_cprod)
- apply (rule cprod_cinfinite_bound)
- apply (rule ordIso_ordLeq_trans)
- apply (rule Pow_cexp_ctwo)
- apply (rule ordIso_ordLeq_trans)
- apply (rule cexp_cong2)
- apply (rule card_of_nat)
- apply (rule Card_order_ctwo)
- apply (rule card_of_Card_order)
- apply (rule cexp_mono1)
- apply (rule ordLeq_csum2)
- apply (rule Card_order_ctwo)
- apply (rule natLeq_Card_order)
- apply (rule ordIso_ordLeq_trans)
- apply (rule card_of_Func_option_Func)
- apply (rule ordIso_ordLeq_trans)
- apply (rule card_of_Func)
- apply (rule ordIso_ordLeq_trans)
- apply (rule cexp_cong2)
- apply (rule card_of_nat)
- apply (rule card_of_Card_order)
- apply (rule card_of_Card_order)
- apply (rule cexp_mono1)
- apply (rule ordLeq_csum1)
- apply (rule card_of_Card_order)
- apply (rule natLeq_Card_order)
- apply (rule card_of_Card_order)
- apply (rule card_of_Card_order)
- apply (rule Cinfinite_cexp)
- apply (rule ordLeq_csum2)
- apply (rule Card_order_ctwo)
- apply (rule conjI)
- apply (rule natLeq_cinfinite)
- by (rule natLeq_Card_order)
- next
- case True thus ?thesis
- apply -
- apply (rule ordIso_ordLeq_trans)
- apply (rule card_of_ordIso_subst)
- apply (erule list_in_empty)
- apply (rule ordIso_ordLeq_trans)
- apply (rule single_cone)
- apply (rule cone_ordLeq_cexp)
- apply (rule ordLeq_transitive)
- apply (rule cone_ordLeq_ctwo)
- apply (rule ordLeq_csum2)
- by (rule Card_order_ctwo)
- qed
-qed
-
lemma wpull_map:
assumes "wpull A B1 B2 f1 f2 p1 p2"
shows "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)"
@@ -226,9 +146,6 @@
apply (rule ordLess_imp_ordLeq)
apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on)
-next
- fix A :: "'a set"
- show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
qed (simp add: wpull_map)+
(* Finite sets *)
@@ -339,8 +256,6 @@
apply (rule natLeq_card_order)
apply (rule natLeq_cinfinite)
apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite_set)
- apply (rule ordLeq_transitive[OF surj_imp_ordLeq[of _ abs_fset] list_in_bd])
- apply (auto simp: fset_def intro!: image_eqI[of _ abs_fset]) []
apply (erule wpull_fmap)
apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_def fset_rel_aux)
apply transfer apply simp
@@ -380,30 +295,6 @@
apply (rule disjI1)
by (erule finite_Collect_subsets)
-lemma card_of_countable_sets:
-"|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
-(is "|?L| \<le>o _")
-proof(cases "finite A")
- let ?R = "Func (UNIV::nat set) (A <+> (UNIV::bool set))"
- case True hence "finite ?L" by simp
- moreover have "infinite ?R"
- apply(rule infinite_Func[of _ "Inr True" "Inr False"]) by auto
- ultimately show ?thesis unfolding cexp_def csum_def ctwo_def Field_natLeq Field_card_of
- apply(intro ordLess_imp_ordLeq) by (rule finite_ordLess_infinite2)
-next
- case False
- hence "|{X. X \<subseteq> A \<and> countable X}| =o |{X. X \<subseteq> A \<and> countable X} - {{}}|"
- by (intro card_of_infinite_diff_finite finite.emptyI finite.insertI ordIso_symmetric)
- (unfold finite_countable_subset)
- also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
- using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
- also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq"
- apply(rule cexp_mono1)
- apply(rule ordLeq_csum1, rule card_of_Card_order)
- by (rule natLeq_Card_order)
- finally show ?thesis .
-qed
-
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
@@ -469,22 +360,6 @@
next
fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_card_le_natLeq .
next
- fix A :: "'a set"
- have "|{Z. rcset Z \<subseteq> A}| \<le>o |acset ` {X. X \<subseteq> A \<and> countable X}|"
- apply(rule card_of_mono1) unfolding Pow_def image_def
- proof (rule Collect_mono, clarsimp)
- fix x
- assume "rcset x \<subseteq> A"
- hence "rcset x \<subseteq> A \<and> countable (rcset x) \<and> x = acset (rcset x)"
- using acset_rcset[of x] rcset[of x] by force
- thus "\<exists>y \<subseteq> A. countable y \<and> x = acset y" by blast
- qed
- also have "|acset ` {X. X \<subseteq> A \<and> countable X}| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
- using card_of_image .
- also have "|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
- using card_of_countable_sets .
- finally show "|{Z. rcset Z \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
-next
fix A B1 B2 f1 f2 p1 p2
assume wp: "wpull A B1 B2 f1 f2 p1 p2"
show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
@@ -1105,12 +980,6 @@
apply(rule ordLess_imp_ordLeq)
unfolding finite_iff_ordLess_natLeq[symmetric] using finite_set_of .
next
- fix A :: "'a set"
- have "|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_set_of .
- also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
- by (rule list_in_bd)
- finally show "|{M. set_of M \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
-next
fix A B1 B2 f1 f2 p1 p2
let ?map = "\<lambda> f. Abs_multiset \<circ> mmap f \<circ> count"
assume wp: "wpull A B1 B2 f1 f2 p1 p2"
--- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Sat Jul 13 13:03:21 2013 +0200
@@ -211,10 +211,6 @@
|> Thm.close_derivation
end;
- fun in_bd_tac _ =
- mk_comp_in_bd_tac in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer)
- (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
-
fun map_wpull_tac _ =
mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
@@ -235,7 +231,7 @@
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -323,9 +319,6 @@
Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
end;
- fun in_bd_tac _ =
- mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
- (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
fun rel_OO_Grp_tac _ =
@@ -345,7 +338,7 @@
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -425,13 +418,12 @@
Goal.prove_sorry lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
end;
- fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -500,14 +492,12 @@
|> Thm.close_derivation
end;
- fun in_bd_tac _ =
- mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -634,11 +624,6 @@
val set_bds =
map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
- val in_bd =
- @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
- @{thm cexp_cong2} OF [bd_ordIso, if live = 0 then
- @{thm Card_order_ctwo} else @{thm Card_order_csum},
- bd_Card_order_of_bnf bnf]];
fun mk_tac thm {context = ctxt, prems = _} =
(rtac (unfold_all thm) THEN'
@@ -646,7 +631,7 @@
val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
(mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
- (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
+ (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
(mk_tac (map_wpull_of_bnf bnf))
(mk_tac (rel_OO_Grp_of_bnf bnf));
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Sat Jul 13 13:03:21 2013 +0200
@@ -11,7 +11,6 @@
val mk_comp_bd_card_order_tac: thm list -> thm -> tactic
val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
- val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic
val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
@@ -23,17 +22,14 @@
val mk_kill_bd_card_order_tac: int -> thm -> tactic
val mk_kill_bd_cinfinite_tac: thm -> tactic
val kill_in_alt_tac: tactic
- val mk_kill_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic
val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
val mk_kill_set_bd_tac: thm -> thm -> tactic
val empty_natural_tac: tactic
val lift_in_alt_tac: tactic
- val mk_lift_in_bd_tac: int -> thm -> thm -> thm -> tactic
val mk_lift_set_bd_tac: thm -> tactic
val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
- val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
@@ -46,15 +42,10 @@
open BNF_Util
open BNF_Tactics
-val Card_order_csum = @{thm Card_order_csum};
-val Card_order_ctwo = @{thm Card_order_ctwo};
val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
-val card_of_Card_order = @{thm card_of_Card_order};
val csum_Cnotzero1 = @{thm csum_Cnotzero1};
val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
-val ordIso_transitive = @{thm ordIso_transitive};
-val ordLeq_csum2 = @{thm ordLeq_csum2};
val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
val trans_o_apply = @{thm trans[OF o_apply]};
@@ -167,47 +158,6 @@
atac ORELSE'
(rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1));
-fun mk_comp_in_bd_tac comp_in_alt Fin_bds Gin_bd Fbd_Cinfs Gbd_Card_order =
- let
- val (bds, last_bd) = split_last Fin_bds;
- val (Cinfs, _) = split_last Fbd_Cinfs;
- fun gen_before (bd, _) = rtac ctrans THEN' rtac @{thm csum_mono} THEN' rtac bd;
- fun gen_after (_, (bd_Cinf, next_bd_Cinf)) =
- TRY o (rtac @{thm csum_cexp} THEN'
- rtac bd_Cinf THEN'
- (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac next_bd_Cinf ORELSE'
- rtac next_bd_Cinf) THEN'
- ((rtac Card_order_csum THEN' rtac ordLeq_csum2) ORELSE'
- (rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl})) THEN'
- rtac Card_order_ctwo);
- in
- (rtac @{thm ordIso_ordLeq_trans} THEN'
- rtac @{thm card_of_ordIso_subst} THEN'
- rtac comp_in_alt THEN'
- rtac ctrans THEN'
- rtac Gin_bd THEN'
- rtac @{thm ordLeq_ordIso_trans} THEN'
- rtac @{thm cexp_mono1} THEN'
- rtac @{thm ordLeq_ordIso_trans} THEN'
- rtac @{thm csum_mono1} THEN'
- WRAP' gen_before gen_after (bds ~~ (Cinfs ~~ tl Fbd_Cinfs)) (rtac last_bd) THEN'
- rtac @{thm csum_absorb1} THEN'
- rtac @{thm Cinfinite_cexp} THEN'
- (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN'
- rtac Card_order_ctwo THEN'
- (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
- rtac (hd Fbd_Cinfs)) THEN'
- rtac @{thm ctwo_ordLeq_Cinfinite} THEN'
- rtac @{thm Cinfinite_cexp} THEN'
- (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN'
- rtac Card_order_ctwo THEN'
- (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
- rtac (hd Fbd_Cinfs)) THEN'
- rtac Gbd_Card_order THEN'
- rtac @{thm cexp_cprod} THEN'
- rtac @{thm Card_order_csum}) 1
- end;
-
val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
Union_image_insert Union_image_empty};
@@ -264,64 +214,6 @@
((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
-fun mk_kill_in_bd_tac n nontrivial_kill_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero =
- (rtac @{thm ordIso_ordLeq_trans} THEN'
- rtac @{thm card_of_ordIso_subst} THEN'
- rtac in_alt THEN'
- rtac ctrans THEN'
- rtac in_bd THEN'
- rtac @{thm ordIso_ordLeq_trans} THEN'
- rtac @{thm cexp_cong1}) 1 THEN
- (if nontrivial_kill_in then
- rtac ordIso_transitive 1 THEN
- REPEAT_DETERM_N (n - 1)
- ((rtac @{thm csum_cong1} THEN'
- rtac @{thm ordIso_symmetric} THEN'
- rtac @{thm csum_assoc} THEN'
- rtac ordIso_transitive) 1) THEN
- (rtac @{thm ordIso_refl} THEN'
- rtac Card_order_csum THEN'
- rtac ordIso_transitive THEN'
- rtac @{thm csum_assoc} THEN'
- rtac ordIso_transitive THEN'
- rtac @{thm csum_cong1} THEN'
- K (mk_flatten_assoc_tac
- (rtac @{thm ordIso_refl} THEN'
- FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
- ordIso_transitive @{thm csum_assoc} @{thm csum_cong}) THEN'
- rtac @{thm ordIso_refl} THEN'
- (rtac card_of_Card_order ORELSE' rtac Card_order_csum)) 1
- else all_tac) THEN
- (rtac @{thm csum_com} THEN'
- rtac bd_Card_order THEN'
- rtac @{thm ordLeq_ordIso_trans} THEN'
- rtac @{thm cexp_mono1} THEN'
- rtac ctrans THEN'
- rtac @{thm csum_mono2} THEN'
- rtac @{thm ordLeq_cprod1} THEN'
- (rtac card_of_Card_order ORELSE' rtac Card_order_csum) THEN'
- rtac bd_Cnotzero THEN'
- rtac @{thm csum_cexp'} THEN'
- rtac @{thm Cinfinite_cprod2} THEN'
- TRY o rtac csum_Cnotzero1 THEN'
- rtac Cnotzero_UNIV THEN'
- rtac bd_Cinfinite THEN'
- ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE'
- (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN'
- rtac Card_order_ctwo THEN'
- rtac bd_Card_order THEN'
- rtac @{thm cexp_cprod_ordLeq} THEN'
- resolve_tac @{thms Card_order_csum Card_order_ctwo} THEN'
- rtac @{thm Cinfinite_cprod2} THEN'
- TRY o rtac csum_Cnotzero1 THEN'
- rtac Cnotzero_UNIV THEN'
- rtac bd_Cinfinite THEN'
- rtac bd_Cnotzero THEN'
- rtac @{thm ordLeq_cprod2} THEN'
- TRY o rtac csum_Cnotzero1 THEN'
- rtac Cnotzero_UNIV THEN'
- rtac bd_Card_order) 1;
-
(* Lift operation *)
@@ -341,23 +233,6 @@
((rtac sym THEN' rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
-fun mk_lift_in_bd_tac n in_alt in_bd bd_Card_order =
- (rtac @{thm ordIso_ordLeq_trans} THEN'
- rtac @{thm card_of_ordIso_subst} THEN'
- rtac in_alt THEN'
- rtac ctrans THEN'
- rtac in_bd THEN'
- rtac @{thm cexp_mono1}) 1 THEN
- ((rtac @{thm csum_mono1} 1 THEN
- REPEAT_DETERM_N (n - 1)
- ((rtac ctrans THEN'
- rtac ordLeq_csum2 THEN'
- (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) THEN
- (rtac ordLeq_csum2 THEN'
- (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE
- (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN
- (rtac bd_Card_order) 1;
-
(* Permute operation *)
@@ -367,21 +242,6 @@
mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
dest src) 1;
-fun mk_permute_in_bd_tac src dest in_alt in_bd bd_Card_order =
- (rtac @{thm ordIso_ordLeq_trans} THEN'
- rtac @{thm card_of_ordIso_subst} THEN'
- rtac in_alt THEN'
- rtac @{thm ordLeq_ordIso_trans} THEN'
- rtac in_bd THEN'
- rtac @{thm cexp_cong1} THEN'
- rtac @{thm csum_cong1} THEN'
- mk_rotate_eq_tac
- (rtac @{thm ordIso_refl} THEN'
- FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
- ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
- src dest THEN'
- rtac bd_Card_order) 1;
-
fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
(rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Sat Jul 13 13:03:21 2013 +0200
@@ -80,7 +80,7 @@
val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
val wits_of_bnf: bnf -> nonemptiness_witness list
- val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
+ val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
datatype fact_policy = Dont_Note | Note_Some | Note_All
@@ -114,14 +114,13 @@
bd_card_order: thm,
bd_cinfinite: thm,
set_bd: thm list,
- in_bd: thm,
map_wpull: thm,
rel_OO_Grp: thm
};
-fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), rel) =
+fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
{map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
- bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel};
+ bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel};
fun dest_cons [] = raise List.Empty
| dest_cons (x :: xs) = (x, xs);
@@ -136,20 +135,19 @@
||>> dest_cons
||>> chop n
||>> dest_cons
- ||>> dest_cons
||> the_single
|> mk_axioms';
-fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
- [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
+fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel =
+ [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel];
-fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, in_bd,
+fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
map_wpull, rel_OO_Grp} =
- zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd in_bd map_wpull
+ zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
rel_OO_Grp;
fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
- in_bd, map_wpull, rel_OO_Grp} =
+ map_wpull, rel_OO_Grp} =
{map_id = f map_id,
map_comp = f map_comp,
map_cong0 = f map_cong0,
@@ -157,7 +155,6 @@
bd_card_order = f bd_card_order,
bd_cinfinite = f bd_cinfinite,
set_bd = map f set_bd,
- in_bd = f in_bd,
map_wpull = f map_wpull,
rel_OO_Grp = f rel_OO_Grp};
@@ -181,6 +178,7 @@
bd_Cinfinite: thm,
bd_Cnotzero: thm,
collect_set_map: thm lazy,
+ in_bd: thm lazy,
in_cong: thm lazy,
in_mono: thm lazy,
in_rel: thm lazy,
@@ -199,13 +197,14 @@
rel_OO: thm lazy
};
-fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_rel
+fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map' rel_cong rel_mono rel_mono_strong
rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
collect_set_map = collect_set_map,
+ in_bd = in_bd,
in_cong = in_cong,
in_mono = in_mono,
in_rel = in_rel,
@@ -228,6 +227,7 @@
bd_Cinfinite,
bd_Cnotzero,
collect_set_map,
+ in_bd,
in_cong,
in_mono,
in_rel,
@@ -248,6 +248,7 @@
bd_Cinfinite = f bd_Cinfinite,
bd_Cnotzero = f bd_Cnotzero,
collect_set_map = Lazy.map f collect_set_map,
+ in_bd = Lazy.map f in_bd,
in_cong = Lazy.map f in_cong,
in_mono = Lazy.map f in_mono,
in_rel = Lazy.map f in_rel,
@@ -355,7 +356,7 @@
val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf;
val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf;
val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
-val in_bd_of_bnf = #in_bd o #axioms o rep_bnf;
+val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf;
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
@@ -806,17 +807,6 @@
map mk_goal bnf_sets_As
end;
- val in_bd_goal =
- let
- val bd = mk_cexp
- (if live = 0 then ctwo
- else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)
- bnf_bd_As;
- in
- fold_rev Logic.all As
- (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd))
- end;
-
val map_wpull_goal =
let
val prems = map HOLogic.mk_Trueprop
@@ -843,7 +833,7 @@
val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal
- cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_OO_Grp_goal;
+ cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
fun mk_wit_goals (I, wit) =
let
@@ -940,6 +930,26 @@
val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map axioms);
+ fun mk_in_bd () =
+ let
+ val bd = mk_cexp
+ (if live = 0 then ctwo
+ else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)
+ (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV
+ (mk_bnf_T (replicate live (fst (dest_relT (fastype_of bnf_bd_As)))) CA))));
+ val in_bd_goal =
+ fold_rev Logic.all As
+ (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd));
+ in
+ Goal.prove_sorry lthy [] [] in_bd_goal
+ (mk_in_bd_tac live (Lazy.force map_comp') (Lazy.force map_id') (#map_cong0 axioms)
+ (map Lazy.force set_map') (#set_bd axioms) (#bd_card_order axioms)
+ bd_Card_order bd_Cinfinite bd_Cnotzero)
+ |> Thm.close_derivation
+ end;
+
+ val in_bd = Lazy.lazy mk_in_bd;
+
fun mk_map_wppull () =
let
val prems = if live = 0 then [] else
@@ -1122,8 +1132,8 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
- val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono
- in_rel map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map'
+ val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
+ in_mono in_rel map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map'
rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
@@ -1145,7 +1155,7 @@
(bd_CinfiniteN, [#bd_Cinfinite facts]),
(bd_CnotzeroN, [#bd_Cnotzero facts]),
(collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
- (in_bdN, [#in_bd axioms]),
+ (in_bdN, [Lazy.force (#in_bd facts)]),
(in_monoN, [Lazy.force (#in_mono facts)]),
(in_relN, [Lazy.force (#in_rel facts)]),
(map_compN, [#map_comp axioms]),
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Sat Jul 13 13:03:21 2013 +0200
@@ -27,6 +27,9 @@
{prems: thm list, context: Proof.context} -> tactic
val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+
+ val mk_in_bd_tac: int -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm -> thm ->
+ {prems: 'a, context: Proof.context} -> tactic
end;
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -35,6 +38,8 @@
open BNF_Util
open BNF_Tactics
+val ord_eq_le_trans = @{thm ord_eq_le_trans};
+
fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
fun mk_map_cong_tac ctxt cong0 =
@@ -63,7 +68,7 @@
REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
set_maps,
CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
@@ -87,7 +92,7 @@
hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac],
rtac CollectI,
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac])
set_maps,
rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
@@ -99,7 +104,7 @@
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
CONJ_WRAP' (fn thm =>
- EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
+ EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac])
set_maps])
@{thms fst_convol snd_convol} [map_id', refl])] 1
@@ -133,7 +138,7 @@
EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans,
rtac map_cong0, 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}),
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
end;
@@ -147,7 +152,7 @@
let
val n = length set_maps;
fun in_tac nthO_in = rtac CollectI THEN'
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
in
if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
@@ -203,5 +208,65 @@
EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
+fun mk_in_bd_tac live map_comp' map_id' map_cong0 set_map's set_bds
+ bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
+ if live = 0 then
+ rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
+ ordLeq_cexp2[OF ordLeq_refl[OF Card_order_ctwo] Card_order_csum]]} 1
+ else
+ let
+ val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
+ val inserts =
+ map (fn set_bd =>
+ iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
+ [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
+ set_bds;
+ in
+ EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm cprod_cinfinite_bound},
+ rtac (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac @{thm card_of_Card_order},
+ rtac @{thm ordLeq_csum2}, rtac @{thm Card_order_ctwo}, rtac @{thm Card_order_csum},
+ rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1},
+ if live = 1 then rtac @{thm ordIso_refl[OF Card_order_csum]}
+ else
+ REPEAT_DETERM_N (live - 2) o rtac @{thm ordIso_transitive[OF csum_cong2]} THEN'
+ REPEAT_DETERM_N (live - 1) o rtac @{thm csum_csum},
+ rtac bd_Card_order, rtac (@{thm cexp_mono2_Cnotzero} RS ctrans), rtac @{thm ordLeq_csum1},
+ rtac bd_Card_order, rtac @{thm Card_order_csum}, rtac bd_Cnotzero,
+ rtac @{thm csum_Cfinite_cexp_Cinfinite},
+ rtac (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}),
+ CONJ_WRAP_GEN' (rtac @{thm Cfinite_csum}) (K (rtac @{thm Cfinite_cone})) set_map's,
+ rtac bd'_Cinfinite, rtac @{thm card_of_Card_order},
+ rtac @{thm Card_order_cexp}, rtac @{thm Cinfinite_cexp}, rtac @{thm ordLeq_csum2},
+ rtac @{thm Card_order_ctwo}, rtac bd'_Cinfinite,
+ rtac (Drule.rotate_prems 1 (@{thm cprod_mono2} RSN (2, ctrans))),
+ REPEAT_DETERM_N (live - 1) o
+ (rtac (bd_Cinfinite RS @{thm cprod_cexp_csum_cexp_Cinfinite} RSN (2, ctrans)) THEN'
+ rtac @{thm ordLeq_ordIso_trans[OF cprod_mono2 ordIso_symmetric[OF cprod_cexp]]}),
+ rtac @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN
+ unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
+ unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
+ EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm surj_imp_ordLeq}, rtac subsetI,
+ Method.insert_tac inserts, REPEAT_DETERM o dtac meta_spec,
+ REPEAT_DETERM o eresolve_tac [exE, Tactic.make_elim conjunct1], etac CollectE,
+ if live = 1 then K all_tac
+ else REPEAT_DETERM_N (live - 2) o (etac conjE THEN' rotate_tac ~1) THEN' etac conjE,
+ rtac (Drule.rotate_prems 1 @{thm image_eqI}), rtac @{thm SigmaI}, rtac @{thm UNIV_I},
+ CONJ_WRAP_GEN' (rtac @{thm SigmaI})
+ (K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_map's,
+ rtac sym,
+ rtac (Drule.rotate_prems 1
+ ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
+ map_comp' RS sym, map_id']) RSN (2, trans))),
+ REPEAT_DETERM_N (2 * live) o atac,
+ REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans),
+ rtac refl,
+ rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
+ rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
+ map_comp' RS sym, map_id']),
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
+ CONJ_WRAP' (fn thm =>
+ rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
+ set_map's] 1
+ end;
end;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sat Jul 13 13:03:21 2013 +0200
@@ -153,8 +153,8 @@
val hrecTs = map fastype_of Zeros;
val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs;
- val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2),
- z's), As), As_copy), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
+ val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2),
+ z's), As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
(nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy
|> mk_Frees' "b" activeAs
@@ -162,7 +162,6 @@
||>> mk_Frees "b" activeAs
||>> mk_Frees "b" activeBs
||>> mk_Frees "A" ATs
- ||>> mk_Frees "A" ATs
||>> mk_Frees "B" BTs
||>> mk_Frees "B" BTs
||>> mk_Frees "B'" B'Ts
@@ -209,9 +208,6 @@
val bd_Card_order = hd bd_Card_orders;
val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
val bd_Cinfinite = hd bd_Cinfinites;
- val bd_Cnotzeros = map bd_Cnotzero_of_bnf bnfs;
- val bd_Cnotzero = hd bd_Cnotzeros;
- val in_bds = map in_bd_of_bnf bnfs;
val in_monos = map in_mono_of_bnf bnfs;
val map_comps = map map_comp_of_bnf bnfs;
val sym_map_comps = map (fn thm => thm RS sym) map_comps;
@@ -348,8 +344,6 @@
(K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
end;
- val coalg_set_thmss' = transpose coalg_set_thmss;
-
fun mk_tcoalg ATs BTs = mk_coalg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
val tcoalg_thm =
@@ -655,7 +649,6 @@
val set_incl_hset_thmss' = transpose set_incl_hset_thmss;
val set_hset_incl_hset_thmsss' = transpose (map transpose set_hset_incl_hset_thmsss);
- val set_hset_incl_hset_thmsss'' = map transpose set_hset_incl_hset_thmsss';
val set_hset_thmss = map (map (fn thm => thm RS @{thm set_mp})) set_incl_hset_thmss;
val set_hset_hset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp})))
set_hset_incl_hset_thmsss;
@@ -733,53 +726,6 @@
goals hset_defss' hset_rec_minimal_thms
end;
- val mor_hset_thmss =
- let
- val mor_hset_rec_thms =
- let
- fun mk_conjunct j T i f x B =
- HOLogic.mk_imp (HOLogic.mk_mem (x, B), HOLogic.mk_eq
- (mk_hset_rec s's nat i j T $ (f $ x), mk_hset_rec ss nat i j T $ x));
-
- fun mk_concl j T = list_all_free zs
- (Library.foldr1 HOLogic.mk_conj (map4 (mk_conjunct j T) ks fs zs Bs));
- val concls = map2 mk_concl ls passiveAs;
-
- val ctss =
- map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
-
- val goals = map (fn concl =>
- Logic.list_implies ([coalg_prem, mor_prem], HOLogic.mk_Trueprop concl)) concls;
- in
- map5 (fn j => fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (K (mk_mor_hset_rec_tac m n cts j hset_rec_0s hset_rec_Sucs
- morE_thms set_map'ss coalg_set_thmss)))
- |> Thm.close_derivation)
- ls goals ctss hset_rec_0ss' hset_rec_Sucss'
- end;
-
- val mor_hset_rec_thmss = map (fn thm => map (fn i =>
- mk_specN n thm RS mk_conjunctN n i RS mp) ks) mor_hset_rec_thms;
-
- fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
-
- fun mk_concl j T i f x =
- mk_Trueprop_eq (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x);
-
- val goalss = map2 (fn j => fn T => map4 (fn i => fn f => fn x => fn B =>
- fold_rev Logic.all (x :: As @ Bs @ ss @ B's @ s's @ fs)
- (Logic.list_implies ([coalg_prem, mor_prem,
- mk_prem x B], mk_concl j T i f x))) ks fs zs Bs) ls passiveAs;
- in
- map3 (map3 (fn goal => fn hset_def => fn mor_hset_rec =>
- Goal.prove_sorry lthy [] [] goal
- (K (mk_mor_hset_tac hset_def mor_hset_rec))
- |> Thm.close_derivation))
- goalss hset_defss' mor_hset_rec_thmss
- end;
-
val timer = time (timer "Hereditary sets");
(* bisimulation *)
@@ -1009,10 +955,9 @@
(* bounds *)
val (lthy, sbd, sbdT,
- sbd_card_order, sbd_Cinfinite, sbd_Cnotzero, sbd_Card_order, set_sbdss, in_sbds) =
+ sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss) =
if n = 1
- then (lthy, sum_bd, sum_bdT,
- bd_card_order, bd_Cinfinite, bd_Cnotzero, bd_Card_order, set_bdss, in_bds)
+ then (lthy, sum_bd, sum_bdT, bd_card_order, bd_Cinfinite, bd_Card_order, set_bdss)
else
let
val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
@@ -1062,31 +1007,16 @@
val sbd_card_order = fold_thms lthy [sbd_def]
(@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]);
val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
- val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
val sbd_Card_order = sbd_Cinfinite RS conjunct2;
fun mk_set_sbd i bd_Card_order bds =
map (fn thm => @{thm ordLeq_ordIso_trans} OF
[bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
-
- fun mk_in_sbd i Co Cnz bd =
- Cnz RS ((@{thm ordLeq_ordIso_trans} OF
- [(Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})), sbd_ordIso]) RS
- (bd RS @{thm ordLeq_transitive[OF _
- cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
- val in_sbds = map4 mk_in_sbd ks bd_Card_orders bd_Cnotzeros in_bds;
in
- (lthy, sbd, sbdT,
- sbd_card_order, sbd_Cinfinite, sbd_Cnotzero, sbd_Card_order, set_sbdss, in_sbds)
+ (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss)
end;
- fun mk_sbd_sbd 1 = sbd_Card_order RS @{thm ordIso_refl}
- | mk_sbd_sbd n = @{thm csum_absorb1} OF
- [sbd_Cinfinite, mk_sbd_sbd (n - 1) RS @{thm ordIso_imp_ordLeq}];
-
- val sbd_sbd_thm = mk_sbd_sbd n;
-
val sbdTs = replicate n sbdT;
val sum_sbd = Library.foldr1 (uncurry mk_csum) (replicate n sbd);
val sum_sbdT = mk_sumTN sbdTs;
@@ -1103,7 +1033,6 @@
val treeFTs = mk_FTs treeTs;
val tree_maps = map4 mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs;
val final_maps = map4 mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs;
- val tree_setss = mk_setss treeTs;
val isNode_setss = mk_setss (passiveAs @ replicate n sbdT);
val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []];
@@ -1269,9 +1198,7 @@
fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
val carTAs = map (mk_carT As) ks;
- val carTAs_copy = map (mk_carT As_copy) ks;
val strTAs = map2 mk_strT treeFTs ks;
- val hset_strTss = map (fn i => map2 (mk_hset strTAs i) ls passiveAs) ks;
val coalgT_thm =
Goal.prove_sorry lthy [] []
@@ -1279,122 +1206,6 @@
(mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_map'ss)
|> Thm.close_derivation;
- val card_of_carT_thms =
- let
- val lhs = mk_card_of
- (HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
- (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)), isTree))));
- val rhs = mk_cexp
- (if m = 0 then ctwo else
- (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo))
- (mk_cexp sbd sbd);
- val card_of_carT =
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs)))
- (K (mk_card_of_carT_tac lthy m isNode_defs sbd_sbd_thm
- sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds))
- |> Thm.close_derivation
- in
- map (fn def => @{thm ordLeq_transitive[OF
- card_of_mono1[OF ord_eq_le_trans[OF _ Collect_restrict']]]} OF [def, card_of_carT])
- carT_defs
- end;
-
- val carT_set_thmss =
- let
- val Kl_lab = HOLogic.mk_prod (Kl, lab);
- fun mk_goal carT strT set k i =
- fold_rev Logic.all (sumx :: Kl :: lab :: k :: kl :: As)
- (Logic.list_implies (map HOLogic.mk_Trueprop
- [HOLogic.mk_mem (Kl_lab, carT), HOLogic.mk_mem (mk_Cons sumx kl, Kl),
- HOLogic.mk_eq (sumx, mk_InN sbdTs k i)],
- HOLogic.mk_Trueprop (HOLogic.mk_mem
- (HOLogic.mk_prod (mk_Shift Kl sumx, mk_shift lab sumx),
- set $ (strT $ Kl_lab)))));
-
- val goalss = map3 (fn carT => fn strT => fn sets =>
- map3 (mk_goal carT strT) (drop m sets) kks ks) carTAs strTAs tree_setss;
- in
- map6 (fn i => fn goals => fn carT_def => fn strT_def => fn isNode_def => fn set_maps =>
- map2 (fn goal => fn set_map =>
- Goal.prove_sorry lthy [] [] goal
- (mk_carT_set_tac n i carT_def strT_def isNode_def set_map)
- |> Thm.close_derivation)
- goals (drop m set_maps))
- ks goalss carT_defs strT_defs isNode_defs set_map'ss
- end;
-
- val carT_set_thmss' = transpose carT_set_thmss;
-
- val isNode_hset_thmss =
- let
- val Kl_lab = HOLogic.mk_prod (Kl, lab);
- fun mk_Kl_lab carT = HOLogic.mk_mem (Kl_lab, carT);
-
- val strT_hset_thmsss =
- let
- val strT_hset_thms =
- let
- fun mk_lab_kl i x = HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i);
-
- fun mk_inner_conjunct j T i x set i' carT =
- HOLogic.mk_imp (HOLogic.mk_conj (mk_Kl_lab carT, mk_lab_kl i x),
- mk_leq (set $ x) (mk_hset strTAs i' j T $ Kl_lab));
-
- fun mk_conjunct j T i x set =
- Library.foldr1 HOLogic.mk_conj (map2 (mk_inner_conjunct j T i x set) ks carTAs);
-
- fun mk_concl j T = list_all_free (Kl :: lab :: xs @ As)
- (HOLogic.mk_imp (HOLogic.mk_mem (kl, Kl),
- Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T)
- ks xs (map (fn xs => nth xs (j - 1)) isNode_setss))));
- val concls = map2 mk_concl ls passiveAs;
-
- val cTs = [SOME (certifyT lthy sum_sbdT)];
- val arg_cong_cTs = map (SOME o certifyT lthy) treeFTs;
- val ctss =
- map (fn phi => map (SOME o certify lthy) [Term.absfree kl' phi, kl]) concls;
-
- val goals = map HOLogic.mk_Trueprop concls;
- in
- map5 (fn j => fn goal => fn cts => fn set_incl_hsets => fn set_hset_incl_hsetss =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (K (mk_strT_hset_tac lthy n m j arg_cong_cTs cTs cts
- carT_defs strT_defs isNode_defs
- set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss'
- coalgT_thm set_map'ss)))
- |> Thm.close_derivation)
- ls goals ctss set_incl_hset_thmss' set_hset_incl_hset_thmsss''
- end;
-
- val strT_hset'_thms = map (fn thm => mk_specN (2 + n + m) thm RS mp) strT_hset_thms;
- in
- map (fn thm => map (fn i => map (fn i' =>
- thm RS mk_conjunctN n i RS mk_conjunctN n i' RS mp) ks) ks) strT_hset'_thms
- end;
-
- val carT_prems = map (fn carT =>
- HOLogic.mk_Trueprop (HOLogic.mk_mem (Kl_lab, carT))) carTAs_copy;
- val prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, Kl));
- val in_prems = map (fn hsets =>
- HOLogic.mk_Trueprop (HOLogic.mk_mem (Kl_lab, mk_in As hsets treeT))) hset_strTss;
- val isNode_premss = replicate n (map (HOLogic.mk_Trueprop o mk_isNode As_copy kl) ks);
- val conclss = replicate n (map (HOLogic.mk_Trueprop o mk_isNode As kl) ks);
- in
- map5 (fn carT_prem => fn isNode_prems => fn in_prem => fn concls => fn strT_hset_thmss =>
- map4 (fn isNode_prem => fn concl => fn isNode_def => fn strT_hset_thms =>
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Kl :: lab :: kl :: As @ As_copy)
- (Logic.list_implies ([carT_prem, prem, isNode_prem, in_prem], concl)))
- (mk_isNode_hset_tac n isNode_def strT_hset_thms)
- |> Thm.close_derivation)
- isNode_prems concls isNode_defs
- (if m = 0 then replicate n [] else transpose strT_hset_thmss))
- carT_prems isNode_premss in_prems conclss
- (if m = 0 then replicate n [] else transpose (map transpose strT_hset_thmsss))
- end;
-
val timer = time (timer "Tree coalgebra");
fun mk_to_sbd s x i i' =
@@ -1831,7 +1642,6 @@
val Reps = map #Rep T_loc_infos;
val Rep_injects = map #Rep_inject T_loc_infos;
- val Rep_inverses = map #Rep_inverse T_loc_infos;
val Abs_inverses = map #Abs_inverse T_loc_infos;
val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
@@ -2689,23 +2499,14 @@
val set_bd_tacss =
map2 (map2 (K oo mk_set_bd_tac sbd_Cinfinite)) hset_defss (transpose col_bd_thmss);
- val in_bd_tacs = map7 (fn i => fn isNode_hsets => fn carT_def =>
- fn card_of_carT => fn mor_image => fn Rep_inverse => fn mor_hsets =>
- (fn {context = ctxt, prems = _} =>
- mk_in_bd_tac ctxt (nth isNode_hsets (i - 1)) isNode_hsets carT_def
- card_of_carT mor_image Rep_inverse mor_hsets
- mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm))
- ks isNode_hset_thmss carT_defs card_of_carT_thms
- mor_image'_thms Rep_inverses (transpose mor_hset_thmss);
-
val map_wpull_tacs =
map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_OO_Grp_tacs;
+ val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
let
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sat Jul 13 13:03:21 2013 +0200
@@ -20,10 +20,6 @@
val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
thm list list -> tactic
- val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
- {prems: 'a, context: Proof.context} -> tactic
- val mk_card_of_carT_tac: Proof.context -> int -> thm list -> thm -> thm -> thm -> thm -> thm ->
- thm list -> tactic
val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
@@ -57,10 +53,7 @@
val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
- val mk_in_bd_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm -> thm -> thm list ->
- thm -> thm -> thm -> thm -> tactic
val mk_incl_lsbis_tac: int -> int -> thm -> tactic
- val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_length_Lev'_tac: thm -> tactic
val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
@@ -83,7 +76,6 @@
val mk_mor_elim_tac: thm -> tactic
val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
thm list -> thm list list -> thm list list -> tactic
- val mk_mor_hset_tac: thm -> thm -> tactic
val mk_mor_incl_tac: thm -> thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
val mk_mor_sum_case_tac: 'a list -> thm -> tactic
@@ -122,9 +114,6 @@
val mk_set_map_tac: thm -> thm -> tactic
val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
thm list -> thm list -> thm list list -> thm list list -> tactic
- val mk_strT_hset_tac: Proof.context -> int -> int -> int -> ctyp option list ->
- ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
- thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic
val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
val mk_unique_mor_tac: thm list -> thm -> tactic
val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
@@ -262,10 +251,6 @@
(rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
(rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
-fun mk_mor_hset_tac hset_def mor_hset_rec =
- EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
- atac, atac, rtac (hset_def RS sym)] 1
-
fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss =
let
val n = length rel_OO_Grps;
@@ -457,157 +442,6 @@
CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
end;
-fun mk_card_of_carT_tac ctxt m isNode_defs sbd_sbd
- sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
- let
- val n = length isNode_defs;
- in
- EVERY' [rtac (Thm.permute_prems 0 1 ctrans),
- rtac @{thm card_of_Sigma_ordLeq_Cinfinite}, rtac @{thm Cinfinite_cexp},
- if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
- rtac @{thm Card_order_ctwo}, rtac @{thm Cinfinite_cexp},
- rtac @{thm ctwo_ordLeq_Cinfinite}, rtac sbd_Cinfinite, rtac sbd_Cinfinite,
- rtac ctrans, rtac @{thm card_of_diff},
- rtac ordIso_ordLeq_trans, rtac @{thm card_of_Field_ordIso},
- rtac @{thm Card_order_cpow}, rtac ordIso_ordLeq_trans,
- rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1},
- if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
- rtac @{thm Card_order_ctwo}, rtac @{thm Card_order_clists},
- rtac @{thm cexp_mono2_Cnotzero}, rtac ordIso_ordLeq_trans,
- rtac @{thm clists_Cinfinite},
- if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}),
- rtac ordIso_ordLeq_trans, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},
- rtac sbd_Cinfinite,
- if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
- rtac @{thm Cnotzero_clists},
- rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp},
- rtac ctrans, rtac @{thm cexp_mono},
- rtac @{thm ordLeq_ordIso_trans},
- CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1
- (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]}
- RSN (3, @{thm Un_Cinfinite_bound}))))
- (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds),
- rtac @{thm cexp_cong1}, rtac @{thm csum_cong1},
- REPEAT_DETERM_N m o rtac @{thm csum_cong2},
- CONJ_WRAP_GEN' (rtac @{thm csum_cong})
- (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds,
- rtac sbd_Card_order,
- rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound},
- rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite,
- rtac FalseE, etac @{thm cpow_clists_czero}, atac,
- rtac @{thm card_of_Card_order},
- rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod},
- rtac @{thm Card_order_csum},
- rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2},
- rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd,
- rtac @{thm cprod_infinite}, rtac sbd_Cinfinite,
- rtac @{thm Card_order_csum}, rtac @{thm Card_order_cprod},
- rtac ctrans, rtac @{thm cexp_mono1},
- rtac ordIso_ordLeq_trans, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
- rtac @{thm ordIso_transitive},
- REPEAT_DETERM_N m o rtac @{thm csum_cong2},
- rtac sbd_sbd,
- BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN'
- FIRST' [rtac @{thm card_of_Card_order},
- rtac @{thm Card_order_csum}, rtac sbd_Card_order])
- @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
- (1 upto m + 1) (m + 1 :: (1 upto m)),
- if m = 0 then K all_tac else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_assoc}],
- rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite,
- if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
- if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
- rtac @{thm Card_order_ctwo}, rtac sbd_Card_order,
- rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod_ordLeq},
- if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
- rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order,
- rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp},
- rtac sbd_Cinfinite,
- if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
- rtac sbd_Cnotzero,
- rtac @{thm card_of_mono1}, rtac subsetI,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac ctxt,
- rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
- rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
- rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
- hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Func_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 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,
- rtac subset_UNIV, rtac equalityD2, rtac @{thm Field_card_order},
- rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),
- atac] 1
- end;
-
-fun mk_carT_set_tac n i carT_def strT_def isNode_def set_map {context = ctxt, prems = _}=
- EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- dtac Pair_eqD,
- etac conjE, hyp_subst_tac ctxt,
- 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),
- etac (arg_cong RS trans),
- fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,
- rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
- etac @{thm prefCl_Succ}, atac] 1;
-
-fun mk_strT_hset_tac ctxt n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
- set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
- let
- val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
- val ks = 1 upto n;
- fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_map)))) =
- CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'
- (if i = i'
- then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
- rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
- rtac (Thm.permute_prems 0 1 (set_map RS box_equals)),
- rtac (trans OF [@{thm image_id} RS fun_cong, id_apply]),
- 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_eqD, etac conjE,
- hyp_subst_tac ctxt, 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));
- fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) =
- dtac (mk_conjunctN n i) THEN'
- CONJ_WRAP' (fn (coalg_set, (carT_set, set_hset_incl_hset)) =>
- EVERY' [rtac impI, etac conjE, etac impE, rtac conjI,
- rtac (coalgT RS coalg_set RS set_mp), atac, etac carT_set, atac, atac,
- etac (@{thm shift_def} RS fun_cong RS trans), etac subset_trans,
- rtac set_hset_incl_hset, etac carT_set, atac, atac])
- (coalg_sets ~~ (carT_sets ~~ set_hset_incl_hsets));
- in
- EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
- REPEAT_DETERM o rtac allI, rtac impI,
- CONJ_WRAP' base_tac
- (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_maps)))),
- REPEAT_DETERM o rtac allI, rtac impI,
- REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI},
- CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN'
- CONJ_WRAP_GEN' (K all_tac) step_tac
- (ks ~~ (drop m coalg_setss ~~ (carT_setss ~~ set_hset_incl_hsetss)))) ks] 1
- end;
-
-fun mk_isNode_hset_tac n isNode_def strT_hsets {context = ctxt, prems = _} =
- let
- val m = length strT_hsets;
- in
- if m = 0 then atac 1
- else (unfold_thms_tac ctxt [isNode_def] THEN
- EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
- rtac exI, rtac conjI, atac,
- CONJ_WRAP' (fn (thm, i) => if i > m then atac
- else EVERY' [rtac (thm RS subset_trans), atac, rtac conjI, atac, atac, atac])
- (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
- end;
-
fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
let
val n = length Lev_0s;
@@ -1325,40 +1159,6 @@
@{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
@{thm infinite_ordLeq_cexp}, sbd_Cinfinite]) 1;
-fun mk_in_bd_tac ctxt isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
- mor_Rep coalgT mor_T_final tcoalg =
- let
- val n = length isNode_hsets;
- val in_hin_tac = rtac CollectI THEN'
- CONJ_WRAP' (fn mor_hset => EVERY' (map etac
- [mor_hset OF [coalgT, mor_T_final] RS sym RS ord_eq_le_trans,
- arg_cong RS sym RS ord_eq_le_trans,
- mor_hset OF [tcoalg, mor_Rep, UNIV_I] RS ord_eq_le_trans])) mor_hsets;
- in
- EVERY' [rtac (Thm.permute_prems 0 1 @{thm ordLeq_transitive}), rtac ctrans,
- rtac @{thm card_of_image}, rtac ordIso_ordLeq_trans,
- rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans,
- rtac @{thm card_of_image}, rtac card_of_carT,
- rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
- rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac set_mp, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE,
- rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
- rtac @{thm proj_image}, rtac @{thm image_eqI}, atac,
- ftac (carT_def RS equalityD1 RS set_mp),
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
- rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
- rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
- rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
- CONJ_WRAP_GEN' (etac disjE) (fn (i, isNode_hset) =>
- EVERY' [rtac (mk_disjIN n i), rtac isNode_hset, atac, atac, atac, in_hin_tac])
- (1 upto n ~~ isNode_hsets),
- CONJ_WRAP' (fn isNode_hset =>
- EVERY' [rtac ballI, rtac isNode_hset, atac, ftac CollectD, etac @{thm SuccD},
- etac bspec, atac, in_hin_tac])
- isNode_hsets,
- atac, rtac isNode_hset, atac, atac, atac, in_hin_tac] 1
- end;
-
fun mk_bd_card_order_tac sbd_card_order =
EVERY' (map rtac [@{thm card_order_cexp}, sbd_card_order, sbd_card_order]) 1;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sat Jul 13 13:03:21 2013 +0200
@@ -98,7 +98,12 @@
fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
(map (replicate live) (replicate n Ts)) bnfs;
val setssAs = mk_setss allAs;
- val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
+ val bd0s = map3 mk_bd_of_bnf Dss Ass bnfs;
+ val bds =
+ map3 (fn bd0 => fn Ds => fn bnf => mk_csum bd0
+ (mk_card_of (HOLogic.mk_UNIV
+ (mk_T_of_bnf Ds (replicate live (fst (dest_relT (fastype_of bd0)))) bnf))))
+ bd0s Dss bnfs;
val witss = map wits_of_bnf bnfs;
val (((((((((((((((((((zs, zs'), As), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
@@ -131,12 +136,23 @@
val fsts = map fst_const prodBsAs;
(* thms *)
- val bd_card_orders = map bd_card_order_of_bnf bnfs;
- val bd_Card_orders = map bd_Card_order_of_bnf bnfs;
- val bd_Card_order = hd bd_Card_orders;
- val bd_Cinfinite = bd_Cinfinite_of_bnf (hd bnfs);
- val bd_Cnotzeros = map bd_Cnotzero_of_bnf bnfs;
+ val bd0_card_orders = map bd_card_order_of_bnf bnfs;
+ val bd0_Card_orders = map bd_Card_order_of_bnf bnfs;
+ val bd0_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
+ val set_bd0ss = map set_bd_of_bnf bnfs;
+
+ val bd_card_orders =
+ map (fn thm => @{thm card_order_csum} OF [thm, @{thm card_of_card_order_on}]) bd0_card_orders;
+ val bd_Card_order = @{thm Card_order_csum};
+ val bd_Card_orders = replicate n bd_Card_order;
+ val bd_Cinfinites = map (fn thm => thm RS @{thm Cinfinite_csum1}) bd0_Cinfinites;
+ val bd_Cnotzeros = map (fn thm => thm RS @{thm Cinfinite_Cnotzero}) bd_Cinfinites;
+ val bd_Cinfinite = hd bd_Cinfinites;
val bd_Cnotzero = hd bd_Cnotzeros;
+ val set_bdss =
+ map2 (fn set_bd0s => fn bd0_Card_order =>
+ map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s)
+ set_bd0ss bd0_Card_orders;
val in_bds = map in_bd_of_bnf bnfs;
val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
val map_comp's = map map_comp'_of_bnf bnfs;
@@ -144,7 +160,6 @@
val map_ids = map map_id_of_bnf bnfs;
val map_id's = map map_id'_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
- val set_bdss = map set_bd_of_bnf bnfs;
val set_map'ss = map set_map'_of_bnf bnfs;
val timer = time (timer "Extracted terms & thms");
@@ -1617,33 +1632,6 @@
split_conj_thm thm
end;
- val in_incl_min_alg_thms =
- let
- fun mk_prem z sets =
- HOLogic.mk_mem (z, mk_in As sets (fastype_of z));
-
- fun mk_incl z sets i =
- HOLogic.mk_imp (mk_prem z sets, HOLogic.mk_mem (z, mk_min_alg As ctors i));
-
- fun mk_cphi z sets i =
- certify lthy (Term.absfree (dest_Free z) (mk_incl z sets i));
-
- val cphis = map3 mk_cphi Izs setss_by_bnf ks;
-
- val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
-
- val goal =
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map3 mk_incl Izs setss_by_bnf ks));
-
- val thm = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (mk_incl_min_alg_tac (rtac induct) Fset_set_thmsss alg_set_thms alg_min_alg_thm))
- |> Thm.close_derivation;
- in
- split_conj_thm thm
- end;
-
val Xsetss = map (map (Term.subst_atomic_types (passiveAs ~~ passiveXs))) setss_by_bnf;
val map_wpull_thms =
@@ -1697,14 +1685,12 @@
val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1));
val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss);
- val in_bd_tacs = map2 (K oo mk_in_bd_tac sum_Card_order suc_bd_Cnotzero)
- in_incl_min_alg_thms card_of_min_alg_thms;
val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
- val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_OO_Grp_tacs;
+ val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+ bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
val ctor_witss =
let
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Jul 11 11:16:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sat Jul 13 13:03:21 2013 +0200
@@ -27,9 +27,6 @@
thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
- val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
- val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
- {prems: 'a, context: Proof.context} -> tactic
val mk_init_ex_mor_tac: thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
{prems: 'a, context: Proof.context} -> tactic
val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
@@ -666,22 +663,6 @@
(induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
end;
-fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} =
- let
- fun use_asm thm = etac (thm RS subset_trans);
-
- fun useIH set_sets = EVERY' [rtac subsetI, rtac mp, Goal.assume_rule_tac ctxt,
- rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [etac (thm RS subset_trans), atac]) set_sets];
-
- fun mk_incl alg_set set_setss =
- EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac (alg_min_alg RS alg_set),
- EVERY' (map use_asm (map hd set_setss)),
- EVERY' (map useIH (transpose (map tl set_setss)))];
- in
- (induct_tac THEN' EVERY' (map2 mk_incl alg_sets set_setsss)) 1
- end;
-
fun mk_lfp_map_wpull_tac ctxt m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
let
val n = length wpulls;
@@ -751,12 +732,6 @@
fun mk_set_map_tac set_nat =
EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
-fun mk_in_bd_tac sum_Card_order sucbd_Cnotzero incl card_of_min_alg =
- EVERY' [rtac ctrans, rtac @{thm card_of_mono1}, rtac subsetI, etac rev_mp,
- rtac incl, rtac ctrans, rtac card_of_min_alg, rtac @{thm cexp_mono2_Cnotzero},
- rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm Card_order_csum},
- rtac sucbd_Cnotzero] 1;
-
fun mk_bd_card_order_tac bd_card_orders =
(rtac @{thm card_order_cpow} THEN'
CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders) 1;