optimize cardinal bounds involving natLeq (omega)
authorblanchet
Mon Mar 03 12:48:19 2014 +0100 (2014-03-03)
changeset 558513d40cf74726c
parent 55850 7f229b0212fe
child 55852 48ced935c0e5
optimize cardinal bounds involving natLeq (omega)
src/HOL/BNF_Cardinal_Arithmetic.thy
src/HOL/BNF_Comp.thy
src/HOL/BNF_LFP.thy
src/HOL/Cardinals/Cardinal_Arithmetic.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 03:13:45 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 12:48:19 2014 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4    "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
     1.5  unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
     1.6  
     1.7 -lemma Cinfinite_csum_strong:
     1.8 +lemma Cinfinite_csum_weak:
     1.9    "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
    1.10  by (erule Cinfinite_csum1)
    1.11  
    1.12 @@ -335,6 +335,9 @@
    1.13  lemma cprod_mono2: "p2 \<le>o r2 \<Longrightarrow> q *c p2 \<le>o q *c r2"
    1.14  by (simp only: cprod_def ordLeq_Times_mono2)
    1.15  
    1.16 +lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
    1.17 +by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
    1.18 +
    1.19  lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
    1.20  unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
    1.21  
    1.22 @@ -347,6 +350,15 @@
    1.23  lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
    1.24  by (blast intro: cinfinite_cprod2 Card_order_cprod)
    1.25  
    1.26 +lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
    1.27 +by (metis cprod_mono ordIso_iff_ordLeq)
    1.28 +
    1.29 +lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
    1.30 +by (metis cprod_mono1 ordIso_iff_ordLeq)
    1.31 +
    1.32 +lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
    1.33 +by (metis cprod_mono2 ordIso_iff_ordLeq)
    1.34 +
    1.35  lemma cprod_com: "p1 *c p2 =o p2 *c p1"
    1.36  by (simp only: cprod_def card_of_Times_commute)
    1.37  
    1.38 @@ -514,6 +526,9 @@
    1.39  unfolding cinfinite_def cprod_def
    1.40  by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+
    1.41  
    1.42 +lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
    1.43 +using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
    1.44 +
    1.45  lemma cexp_cprod_ordLeq:
    1.46    assumes r1: "Card_order r1" and r2: "Cinfinite r2"
    1.47    and r3: "Cnotzero r3" "r3 \<le>o r2"
     2.1 --- a/src/HOL/BNF_Comp.thy	Mon Mar 03 03:13:45 2014 +0100
     2.2 +++ b/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:19 2014 +0100
     2.3 @@ -128,6 +128,12 @@
     2.4  
     2.5  end
     2.6  
     2.7 +lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
     2.8 +by (metis csum_absorb2' ordIso_transitive ordLeq_refl)
     2.9 +
    2.10 +lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    2.11 +by (metis cprod_infinite ordIso_transitive)
    2.12 +
    2.13  ML_file "Tools/BNF/bnf_comp_tactics.ML"
    2.14  ML_file "Tools/BNF/bnf_comp.ML"
    2.15  
     3.1 --- a/src/HOL/BNF_LFP.thy	Mon Mar 03 03:13:45 2014 +0100
     3.2 +++ b/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:19 2014 +0100
     3.3 @@ -251,10 +251,10 @@
     3.4    unfolding vimage2p_def by auto
     3.5  
     3.6  lemma id_transfer: "fun_rel A A id id"
     3.7 -unfolding fun_rel_def by simp
     3.8 +  unfolding fun_rel_def by simp
     3.9  
    3.10  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
    3.11 -  by simp
    3.12 +  by (rule ssubst)
    3.13  
    3.14  ML_file "Tools/BNF/bnf_lfp_util.ML"
    3.15  ML_file "Tools/BNF/bnf_lfp_tactics.ML"
     4.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Mar 03 03:13:45 2014 +0100
     4.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Mar 03 12:48:19 2014 +0100
     4.3 @@ -66,18 +66,10 @@
     4.4    unfolding cprod_def cone_def Field_card_of
     4.5    by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])
     4.6  
     4.7 -lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
     4.8 -by (simp only: cprod_def ordIso_Times_cong2)
     4.9  
    4.10  lemma ordLeq_cprod1: "\<lbrakk>Card_order p1; Cnotzero p2\<rbrakk> \<Longrightarrow> p1 \<le>o p1 *c p2"
    4.11  unfolding cprod_def by (metis Card_order_Times1 czeroI)
    4.12  
    4.13 -lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
    4.14 -using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
    4.15 -
    4.16 -lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
    4.17 -  by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
    4.18 -
    4.19  
    4.20  subsection {* Exponentiation *}
    4.21  
     5.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 03:13:45 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:19 2014 +0100
     5.3 @@ -95,6 +95,10 @@
     5.4      val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
     5.5    in Envir.expand_term get end;
     5.6  
     5.7 +fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
     5.8 +  | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
     5.9 +  | is_sum_prod_natLeq t = (t = @{term natLeq});
    5.10 +
    5.11  fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
    5.12    let
    5.13      val olive = live_of_bnf outer;
    5.14 @@ -170,6 +174,20 @@
    5.15      (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
    5.16      val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
    5.17  
    5.18 +    val (bd', bd_ordIso_natLeq_thm_opt) =
    5.19 +      if is_sum_prod_natLeq bd then
    5.20 +        let
    5.21 +          val bd' = @{term natLeq};
    5.22 +          val bd_bd' = HOLogic.mk_prod (bd, bd');
    5.23 +          val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
    5.24 +          val goal = HOLogic.mk_Trueprop (HOLogic.mk_mem (bd_bd', ordIso));
    5.25 +        in
    5.26 +          (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
    5.27 +            |> Thm.close_derivation))
    5.28 +        end
    5.29 +      else
    5.30 +        (bd, NONE);
    5.31 +
    5.32      fun map_id0_tac _ =
    5.33        mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
    5.34          (map map_id0_of_bnf inners);
    5.35 @@ -220,7 +238,7 @@
    5.36              map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
    5.37          in
    5.38            map2 (fn set_alt => fn single_set_bds => fn ctxt =>
    5.39 -            mk_comp_set_bd_tac ctxt set_alt single_set_bds)
    5.40 +            mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
    5.41            set_alt_thms single_set_bd_thmss
    5.42          end;
    5.43  
    5.44 @@ -278,7 +296,7 @@
    5.45  
    5.46      val (bnf', lthy') =
    5.47        bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
    5.48 -        Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy;
    5.49 +        Binding.empty [] ((((((b, CCA), mapx), sets), bd'), wits), SOME rel) lthy;
    5.50    in
    5.51      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    5.52    end;
     6.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Mar 03 03:13:45 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Mar 03 12:48:19 2014 +0100
     6.3 @@ -15,7 +15,7 @@
     6.4    val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
     6.5    val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
     6.6    val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
     6.7 -  val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
     6.8 +  val mk_comp_set_bd_tac: Proof.context -> thm option -> thm -> thm list -> tactic
     6.9    val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
    6.10    val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
    6.11  
    6.12 @@ -31,6 +31,7 @@
    6.13    val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
    6.14    val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
    6.15    val mk_simple_wit_tac: thm list -> tactic
    6.16 +  val bd_ordIso_natLeq_tac: tactic
    6.17  end;
    6.18  
    6.19  structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
    6.20 @@ -45,7 +46,6 @@
    6.21  val trans_o_apply = @{thm trans[OF o_apply]};
    6.22  
    6.23  
    6.24 -
    6.25  (* Composition *)
    6.26  
    6.27  fun mk_comp_set_alt_tac ctxt collect_set_map =
    6.28 @@ -101,6 +101,7 @@
    6.29    end;
    6.30  
    6.31  fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
    6.32 +  rtac @{thm natLeq_card_order} 1 ORELSE
    6.33    let
    6.34      val (card_orders, last_card_order) = split_last Fbd_card_orders;
    6.35      fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm;
    6.36 @@ -111,14 +112,15 @@
    6.37    end;
    6.38  
    6.39  fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite =
    6.40 -  (rtac @{thm cinfinite_cprod} THEN'
    6.41 +  (rtac @{thm natLeq_cinfinite} ORELSE'
    6.42 +   rtac @{thm cinfinite_cprod} THEN'
    6.43     ((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN'
    6.44       ((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE'
    6.45        rtac Fbd_cinfinite)) ORELSE'
    6.46      rtac Fbd_cinfinite) THEN'
    6.47     rtac Gbd_cinfinite) 1;
    6.48  
    6.49 -fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds =
    6.50 +fun mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds =
    6.51    let
    6.52      val (bds, last_bd) = split_last Gset_Fset_bds;
    6.53      fun gen_before bd =
    6.54 @@ -127,6 +129,9 @@
    6.55        rtac bd;
    6.56      fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
    6.57    in
    6.58 +    (case bd_ordIso_natLeq_opt of
    6.59 +      SOME thm => rtac (thm RS rotate_prems 1 @{thm ordLeq_ordIso_trans}) 1
    6.60 +    | NONE => all_tac) THEN
    6.61      unfold_thms_tac ctxt [comp_set_alt] THEN
    6.62      rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
    6.63      unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
    6.64 @@ -168,7 +173,6 @@
    6.65      (etac FalseE ORELSE' atac))) 1);
    6.66  
    6.67  
    6.68 -
    6.69  (* Kill operation *)
    6.70  
    6.71  fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
    6.72 @@ -187,7 +191,6 @@
    6.73      REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
    6.74  
    6.75  
    6.76 -
    6.77  (* Lift operation *)
    6.78  
    6.79  val empty_natural_tac = rtac @{thm empty_natural} 1;
    6.80 @@ -206,7 +209,6 @@
    6.81      REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
    6.82  
    6.83  
    6.84 -
    6.85  (* Permute operation *)
    6.86  
    6.87  fun mk_permute_in_alt_tac src dest =
    6.88 @@ -214,6 +216,9 @@
    6.89    mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
    6.90      dest src) 1;
    6.91  
    6.92 +
    6.93 +(* Miscellaneous *)
    6.94 +
    6.95  fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
    6.96    EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
    6.97  
    6.98 @@ -222,4 +227,13 @@
    6.99  
   6.100  fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
   6.101  
   6.102 +val csum_thms =
   6.103 +  @{thms csum_cong1 csum_cong2 csum_cong  csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
   6.104 +val cprod_thms =
   6.105 +  @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
   6.106 +
   6.107 +val bd_ordIso_natLeq_tac =
   6.108 +  HEADGOAL (REPEAT_DETERM o resolve_tac
   6.109 +    (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
   6.110 +
   6.111  end;
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 03:13:45 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 12:48:19 2014 +0100
     7.3 @@ -32,6 +32,8 @@
     7.4  
     7.5    val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
     7.6  
     7.7 +  val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
     7.8 +
     7.9    val IITN: string
    7.10    val LevN: string
    7.11    val algN: string
    7.12 @@ -164,7 +166,8 @@
    7.13    val mk_sum_caseN: int -> int -> thm
    7.14    val mk_sum_caseN_balanced: int -> int -> thm
    7.15  
    7.16 -  val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
    7.17 +  val mk_sum_Cinfinite: thm list -> thm
    7.18 +  val mk_sum_card_order: thm list -> thm
    7.19  
    7.20    val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
    7.21      term list -> term list -> term list -> term list -> term list ->
    7.22 @@ -474,6 +477,12 @@
    7.23      Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
    7.24        right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
    7.25  
    7.26 +fun mk_sum_Cinfinite [thm] = thm
    7.27 +  | mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms];
    7.28 +
    7.29 +fun mk_sum_card_order [thm] = thm
    7.30 +  | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
    7.31 +
    7.32  fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
    7.33    let
    7.34      val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
     8.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 03 03:13:45 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 03 12:48:19 2014 +0100
     8.3 @@ -953,17 +953,8 @@
     8.4            val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
     8.5            val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
     8.6  
     8.7 -          fun mk_sum_Cinfinite [thm] = thm
     8.8 -            | mk_sum_Cinfinite (thm :: thms) =
     8.9 -              @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
    8.10 -
    8.11            val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
    8.12            val sum_Card_order = sum_Cinfinite RS conjunct2;
    8.13 -
    8.14 -          fun mk_sum_card_order [thm] = thm
    8.15 -            | mk_sum_card_order (thm :: thms) =
    8.16 -              @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
    8.17 -
    8.18            val sum_card_order = mk_sum_card_order bd_card_orders;
    8.19  
    8.20            val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 03 03:13:45 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 03 12:48:19 2014 +0100
     9.3 @@ -587,17 +587,8 @@
     9.4            val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
     9.5            val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
     9.6  
     9.7 -          fun mk_sum_Cinfinite [thm] = thm
     9.8 -            | mk_sum_Cinfinite (thm :: thms) =
     9.9 -              @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
    9.10 -
    9.11            val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
    9.12            val sum_Card_order = sum_Cinfinite RS conjunct2;
    9.13 -
    9.14 -          fun mk_sum_card_order [thm] = thm
    9.15 -            | mk_sum_card_order (thm :: thms) =
    9.16 -              @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
    9.17 -
    9.18            val sum_card_order = mk_sum_card_order bd_card_orders;
    9.19  
    9.20            val sbd_ordIso = @{thm ssubst_Pair_rhs} OF