--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 12:48:19 2014 +0100
@@ -199,7 +199,7 @@
"Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
-lemma Cinfinite_csum_strong:
+lemma Cinfinite_csum_weak:
"\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
by (erule Cinfinite_csum1)
@@ -335,6 +335,9 @@
lemma cprod_mono2: "p2 \<le>o r2 \<Longrightarrow> q *c p2 \<le>o q *c r2"
by (simp only: cprod_def ordLeq_Times_mono2)
+lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
+by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
+
lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
@@ -347,6 +350,15 @@
lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
by (blast intro: cinfinite_cprod2 Card_order_cprod)
+lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
+by (metis cprod_mono ordIso_iff_ordLeq)
+
+lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
+by (metis cprod_mono1 ordIso_iff_ordLeq)
+
+lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
+by (metis cprod_mono2 ordIso_iff_ordLeq)
+
lemma cprod_com: "p1 *c p2 =o p2 *c p1"
by (simp only: cprod_def card_of_Times_commute)
@@ -514,6 +526,9 @@
unfolding cinfinite_def cprod_def
by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+
+lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
+using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
+
lemma cexp_cprod_ordLeq:
assumes r1: "Card_order r1" and r2: "Cinfinite r2"
and r3: "Cnotzero r3" "r3 \<le>o r2"
--- a/src/HOL/BNF_Comp.thy Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:19 2014 +0100
@@ -128,6 +128,12 @@
end
+lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
+by (metis csum_absorb2' ordIso_transitive ordLeq_refl)
+
+lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
+by (metis cprod_infinite ordIso_transitive)
+
ML_file "Tools/BNF/bnf_comp_tactics.ML"
ML_file "Tools/BNF/bnf_comp.ML"
--- a/src/HOL/BNF_LFP.thy Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:19 2014 +0100
@@ -251,10 +251,10 @@
unfolding vimage2p_def by auto
lemma id_transfer: "fun_rel A A id id"
-unfolding fun_rel_def by simp
+ unfolding fun_rel_def by simp
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
- by simp
+ by (rule ssubst)
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Mar 03 12:48:19 2014 +0100
@@ -66,18 +66,10 @@
unfolding cprod_def cone_def Field_card_of
by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])
-lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
-by (simp only: cprod_def ordIso_Times_cong2)
lemma ordLeq_cprod1: "\<lbrakk>Card_order p1; Cnotzero p2\<rbrakk> \<Longrightarrow> p1 \<le>o p1 *c p2"
unfolding cprod_def by (metis Card_order_Times1 czeroI)
-lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
-using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
-
-lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
- by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
-
subsection {* Exponentiation *}
--- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 12:48:19 2014 +0100
@@ -95,6 +95,10 @@
val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
in Envir.expand_term get end;
+fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
+ | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
+ | is_sum_prod_natLeq t = (t = @{term natLeq});
+
fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
let
val olive = live_of_bnf outer;
@@ -170,6 +174,20 @@
(*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
+ val (bd', bd_ordIso_natLeq_thm_opt) =
+ if is_sum_prod_natLeq bd then
+ let
+ val bd' = @{term natLeq};
+ val bd_bd' = HOLogic.mk_prod (bd, bd');
+ val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
+ val goal = HOLogic.mk_Trueprop (HOLogic.mk_mem (bd_bd', ordIso));
+ in
+ (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
+ |> Thm.close_derivation))
+ end
+ else
+ (bd, NONE);
+
fun map_id0_tac _ =
mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
(map map_id0_of_bnf inners);
@@ -220,7 +238,7 @@
map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
in
map2 (fn set_alt => fn single_set_bds => fn ctxt =>
- mk_comp_set_bd_tac ctxt set_alt single_set_bds)
+ mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
set_alt_thms single_set_bd_thmss
end;
@@ -278,7 +296,7 @@
val (bnf', lthy') =
bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
- Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy;
+ Binding.empty [] ((((((b, CCA), mapx), sets), bd'), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Mar 03 12:48:19 2014 +0100
@@ -15,7 +15,7 @@
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
- val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_comp_set_bd_tac: Proof.context -> thm option -> thm -> thm list -> tactic
val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
@@ -31,6 +31,7 @@
val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
val mk_simple_wit_tac: thm list -> tactic
+ val bd_ordIso_natLeq_tac: tactic
end;
structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
@@ -45,7 +46,6 @@
val trans_o_apply = @{thm trans[OF o_apply]};
-
(* Composition *)
fun mk_comp_set_alt_tac ctxt collect_set_map =
@@ -101,6 +101,7 @@
end;
fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
+ rtac @{thm natLeq_card_order} 1 ORELSE
let
val (card_orders, last_card_order) = split_last Fbd_card_orders;
fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm;
@@ -111,14 +112,15 @@
end;
fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite =
- (rtac @{thm cinfinite_cprod} THEN'
+ (rtac @{thm natLeq_cinfinite} ORELSE'
+ rtac @{thm cinfinite_cprod} THEN'
((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN'
((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE'
rtac Fbd_cinfinite)) ORELSE'
rtac Fbd_cinfinite) THEN'
rtac Gbd_cinfinite) 1;
-fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds =
+fun mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds =
let
val (bds, last_bd) = split_last Gset_Fset_bds;
fun gen_before bd =
@@ -127,6 +129,9 @@
rtac bd;
fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
in
+ (case bd_ordIso_natLeq_opt of
+ SOME thm => rtac (thm RS rotate_prems 1 @{thm ordLeq_ordIso_trans}) 1
+ | NONE => all_tac) THEN
unfold_thms_tac ctxt [comp_set_alt] THEN
rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
@@ -168,7 +173,6 @@
(etac FalseE ORELSE' atac))) 1);
-
(* Kill operation *)
fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
@@ -187,7 +191,6 @@
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
-
(* Lift operation *)
val empty_natural_tac = rtac @{thm empty_natural} 1;
@@ -206,7 +209,6 @@
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
-
(* Permute operation *)
fun mk_permute_in_alt_tac src dest =
@@ -214,6 +216,9 @@
mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
dest src) 1;
+
+(* Miscellaneous *)
+
fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
@@ -222,4 +227,13 @@
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
+val csum_thms =
+ @{thms csum_cong1 csum_cong2 csum_cong csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
+val cprod_thms =
+ @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
+
+val bd_ordIso_natLeq_tac =
+ HEADGOAL (REPEAT_DETERM o resolve_tac
+ (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
+
end;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:19 2014 +0100
@@ -32,6 +32,8 @@
val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
+ val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
+
val IITN: string
val LevN: string
val algN: string
@@ -164,7 +166,8 @@
val mk_sum_caseN: int -> int -> thm
val mk_sum_caseN_balanced: int -> int -> thm
- val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
+ val mk_sum_Cinfinite: thm list -> thm
+ val mk_sum_card_order: thm list -> thm
val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
term list -> term list -> term list -> term list -> term list ->
@@ -474,6 +477,12 @@
Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
+fun mk_sum_Cinfinite [thm] = thm
+ | mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms];
+
+fun mk_sum_card_order [thm] = thm
+ | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
+
fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
let
val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 12:48:19 2014 +0100
@@ -953,17 +953,8 @@
val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
- fun mk_sum_Cinfinite [thm] = thm
- | mk_sum_Cinfinite (thm :: thms) =
- @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
-
val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
val sum_Card_order = sum_Cinfinite RS conjunct2;
-
- fun mk_sum_card_order [thm] = thm
- | mk_sum_card_order (thm :: thms) =
- @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
-
val sum_card_order = mk_sum_card_order bd_card_orders;
val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 12:48:19 2014 +0100
@@ -587,17 +587,8 @@
val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
- fun mk_sum_Cinfinite [thm] = thm
- | mk_sum_Cinfinite (thm :: thms) =
- @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
-
val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
val sum_Card_order = sum_Cinfinite RS conjunct2;
-
- fun mk_sum_card_order [thm] = thm
- | mk_sum_card_order (thm :: thms) =
- @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
-
val sum_card_order = mk_sum_card_order bd_card_orders;
val sbd_ordIso = @{thm ssubst_Pair_rhs} OF