introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
authorhuffman
Fri Mar 05 14:50:37 2010 -0800 (2010-03-05)
changeset 35597e4331b99b03f
parent 35596 49a02dab35ed
child 35598 78224a53cf73
child 35599 20670f5564e9
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
src/HOLCF/Domain.thy
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Domain.thy	Fri Mar 05 14:05:25 2010 -0800
     1.2 +++ b/src/HOLCF/Domain.thy	Fri Mar 05 14:50:37 2010 -0800
     1.3 @@ -214,6 +214,102 @@
     1.4    ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
     1.5  
     1.6  
     1.7 +subsection {* Take functions and finiteness *}
     1.8 +
     1.9 +lemma lub_ID_take_lemma:
    1.10 +  assumes "chain t" and "(\<Squnion>n. t n) = ID"
    1.11 +  assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
    1.12 +proof -
    1.13 +  have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
    1.14 +    using assms(3) by simp
    1.15 +  then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
    1.16 +    using assms(1) by (simp add: lub_distribs)
    1.17 +  then show "x = y"
    1.18 +    using assms(2) by simp
    1.19 +qed
    1.20 +
    1.21 +lemma lub_ID_reach:
    1.22 +  assumes "chain t" and "(\<Squnion>n. t n) = ID"
    1.23 +  shows "(\<Squnion>n. t n\<cdot>x) = x"
    1.24 +using assms by (simp add: lub_distribs)
    1.25 +
    1.26 +text {*
    1.27 +  Let a ``decisive'' function be a deflation that maps every input to
    1.28 +  either itself or bottom.  Then if a domain's take functions are all
    1.29 +  decisive, then all values in the domain are finite.
    1.30 +*}
    1.31 +
    1.32 +definition
    1.33 +  decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
    1.34 +where
    1.35 +  "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
    1.36 +
    1.37 +lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
    1.38 +  unfolding decisive_def by simp
    1.39 +
    1.40 +lemma decisive_cases:
    1.41 +  assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
    1.42 +using assms unfolding decisive_def by auto
    1.43 +
    1.44 +lemma decisive_bottom: "decisive \<bottom>"
    1.45 +  unfolding decisive_def by simp
    1.46 +
    1.47 +lemma decisive_ID: "decisive ID"
    1.48 +  unfolding decisive_def by simp
    1.49 +
    1.50 +lemma decisive_ssum_map:
    1.51 +  assumes f: "decisive f"
    1.52 +  assumes g: "decisive g"
    1.53 +  shows "decisive (ssum_map\<cdot>f\<cdot>g)"
    1.54 +apply (rule decisiveI, rename_tac s)
    1.55 +apply (case_tac s, simp_all)
    1.56 +apply (rule_tac x=x in decisive_cases [OF f], simp_all)
    1.57 +apply (rule_tac x=y in decisive_cases [OF g], simp_all)
    1.58 +done
    1.59 +
    1.60 +lemma decisive_sprod_map:
    1.61 +  assumes f: "decisive f"
    1.62 +  assumes g: "decisive g"
    1.63 +  shows "decisive (sprod_map\<cdot>f\<cdot>g)"
    1.64 +apply (rule decisiveI, rename_tac s)
    1.65 +apply (case_tac s, simp_all)
    1.66 +apply (rule_tac x=x in decisive_cases [OF f], simp_all)
    1.67 +apply (rule_tac x=y in decisive_cases [OF g], simp_all)
    1.68 +done
    1.69 +
    1.70 +lemma decisive_abs_rep:
    1.71 +  fixes abs rep
    1.72 +  assumes iso: "iso abs rep"
    1.73 +  assumes d: "decisive d"
    1.74 +  shows "decisive (abs oo d oo rep)"
    1.75 +apply (rule decisiveI)
    1.76 +apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
    1.77 +apply (simp add: iso.rep_iso [OF iso])
    1.78 +apply (simp add: iso.abs_strict [OF iso])
    1.79 +done
    1.80 +
    1.81 +lemma lub_ID_finite:
    1.82 +  assumes chain: "chain d"
    1.83 +  assumes lub: "(\<Squnion>n. d n) = ID"
    1.84 +  assumes decisive: "\<And>n. decisive (d n)"
    1.85 +  shows "\<exists>n. d n\<cdot>x = x"
    1.86 +proof -
    1.87 +  have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
    1.88 +  have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
    1.89 +  have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
    1.90 +    using decisive unfolding decisive_def by simp
    1.91 +  hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
    1.92 +    by auto
    1.93 +  hence "finite (range (\<lambda>n. d n\<cdot>x))"
    1.94 +    by (rule finite_subset, simp)
    1.95 +  with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
    1.96 +    by (rule finite_range_imp_finch)
    1.97 +  then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
    1.98 +    unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
    1.99 +  with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
   1.100 +qed
   1.101 +
   1.102 +
   1.103  subsection {* Installing the domain package *}
   1.104  
   1.105  lemmas con_strict_rules =
   1.106 @@ -253,23 +349,6 @@
   1.107    ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
   1.108    sprod_map_spair' sprod_map_strict u_map_up u_map_strict
   1.109  
   1.110 -lemma lub_ID_take_lemma:
   1.111 -  assumes "chain t" and "(\<Squnion>n. t n) = ID"
   1.112 -  assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
   1.113 -proof -
   1.114 -  have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
   1.115 -    using assms(3) by simp
   1.116 -  then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
   1.117 -    using assms(1) by (simp add: lub_distribs)
   1.118 -  then show "x = y"
   1.119 -    using assms(2) by simp
   1.120 -qed
   1.121 -
   1.122 -lemma lub_ID_reach:
   1.123 -  assumes "chain t" and "(\<Squnion>n. t n) = ID"
   1.124 -  shows "(\<Squnion>n. t n\<cdot>x) = x"
   1.125 -using assms by (simp add: lub_distribs)
   1.126 -
   1.127  use "Tools/cont_consts.ML"
   1.128  use "Tools/cont_proc.ML"
   1.129  use "Tools/Domain/domain_library.ML"
     2.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 14:05:25 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 14:50:37 2010 -0800
     2.3 @@ -216,8 +216,13 @@
     2.4      fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
     2.5      fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
     2.6    in
     2.7 +    val axs_rep_iso = map (ga "rep_iso") dnames;
     2.8 +    val axs_abs_iso = map (ga "abs_iso") dnames;
     2.9      val axs_chain_take = map (ga "chain_take") dnames;
    2.10 +    val lub_take_thms = map (ga "lub_take") dnames;
    2.11      val axs_finite_def = map (ga "finite_def") dnames;
    2.12 +    val take_0_thms = map (ga "take_0") dnames;
    2.13 +    val take_Suc_thms = map (ga "take_Suc") dnames;
    2.14      val cases = map (ga  "casedist" ) dnames;
    2.15      val con_rews  = maps (gts "con_rews" ) dnames;
    2.16    end;
    2.17 @@ -318,75 +323,41 @@
    2.18    (
    2.19      if is_finite
    2.20      then (* finite case *)
    2.21 -      let 
    2.22 -        fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
    2.23 -        fun dname_lemma dn =
    2.24 -          let
    2.25 -            val prem1 = mk_trp (defined (%:"x"));
    2.26 -            val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
    2.27 -            val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
    2.28 -            val concl = mk_trp (take_enough dn);
    2.29 -            val goal = prem1 ===> prem2 ===> concl;
    2.30 -            val tacs = [
    2.31 -              etac disjE 1,
    2.32 -              etac notE 1,
    2.33 -              resolve_tac take_lemmas 1,
    2.34 -              asm_simp_tac take_ss 1,
    2.35 -              atac 1];
    2.36 -          in pg [] goal (K tacs) end;
    2.37 -        val _ = trace " Proving finite_lemmas1a";
    2.38 -        val finite_lemmas1a = map dname_lemma dnames;
    2.39 - 
    2.40 -        val _ = trace " Proving finite_lemma1b";
    2.41 -        val finite_lemma1b =
    2.42 +      let
    2.43 +        val decisive_lemma =
    2.44            let
    2.45 -            fun mk_eqn n ((dn, args), _) =
    2.46 -              let
    2.47 -                val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
    2.48 -                val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
    2.49 -              in
    2.50 -                mk_constrainall
    2.51 -                  (x_name n, Type (dn,args), mk_disj (disj1, disj2))
    2.52 -              end;
    2.53 -            val goal =
    2.54 -              mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
    2.55 -            fun arg_tacs ctxt vn = [
    2.56 -              eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
    2.57 -              etac disjE 1,
    2.58 -              asm_simp_tac (HOL_ss addsimps con_rews) 1,
    2.59 -              asm_simp_tac take_ss 1];
    2.60 -            fun con_tacs ctxt (con, args) =
    2.61 -              asm_simp_tac take_ss 1 ::
    2.62 -              maps (arg_tacs ctxt) (nonlazy_rec args);
    2.63 -            fun foo_tacs ctxt n (cons, cases) =
    2.64 -              simp_tac take_ss 1 ::
    2.65 -              rtac allI 1 ::
    2.66 -              res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
    2.67 -              asm_simp_tac take_ss 1 ::
    2.68 -              maps (con_tacs ctxt) cons;
    2.69 -            fun tacs ctxt =
    2.70 -              rtac allI 1 ::
    2.71 -              InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
    2.72 -              simp_tac take_ss 1 ::
    2.73 -              TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
    2.74 -              flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
    2.75 -          in pg [] goal tacs end;
    2.76 -
    2.77 -        fun one_finite (dn, l1b) =
    2.78 +            val iso_locale_thms =
    2.79 +                map2 (fn x => fn y => @{thm iso.intro} OF [x, y])
    2.80 +                axs_abs_iso axs_rep_iso;
    2.81 +            val decisive_abs_rep_thms =
    2.82 +                map (fn x => @{thm decisive_abs_rep} OF [x])
    2.83 +                iso_locale_thms;
    2.84 +            val n = Free ("n", @{typ nat});
    2.85 +            fun mk_decisive t = %%: @{const_name decisive} $ t;
    2.86 +            fun f dn = mk_decisive (dc_take dn $ n);
    2.87 +            val goal = mk_trp (foldr1 mk_conj (map f dnames));
    2.88 +            val rules0 = @{thm decisive_bottom} :: take_0_thms;
    2.89 +            val rules1 =
    2.90 +                take_Suc_thms @ decisive_abs_rep_thms
    2.91 +                @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
    2.92 +            val tacs = [
    2.93 +                rtac @{thm nat.induct} 1,
    2.94 +                simp_tac (HOL_ss addsimps rules0) 1,
    2.95 +                asm_simp_tac (HOL_ss addsimps rules1) 1];
    2.96 +          in pg [] goal (K tacs) end;
    2.97 +        fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
    2.98 +        fun one_finite (dn, decisive_thm) =
    2.99            let
   2.100              val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
   2.101 -            fun tacs ctxt = [
   2.102 -                        (* FIXME! case_UU_tac *)
   2.103 -              case_UU_tac ctxt take_rews 1 "x",
   2.104 -              eresolve_tac finite_lemmas1a 1,
   2.105 -              step_tac HOL_cs 1,
   2.106 -              step_tac HOL_cs 1,
   2.107 -              cut_facts_tac [l1b] 1,
   2.108 -              fast_tac HOL_cs 1];
   2.109 -          in pg axs_finite_def goal tacs end;
   2.110 +            val tacs = [
   2.111 +                rtac @{thm lub_ID_finite} 1,
   2.112 +                resolve_tac axs_chain_take 1,
   2.113 +                resolve_tac lub_take_thms 1,
   2.114 +                rtac decisive_thm 1];
   2.115 +          in pg axs_finite_def goal (K tacs) end;
   2.116  
   2.117          val _ = trace " Proving finites";
   2.118 -        val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
   2.119 +        val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
   2.120          val _ = trace " Proving ind";
   2.121          val ind =
   2.122            let