uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
authorhuffman
Wed Mar 03 07:36:31 2010 -0800 (2010-03-03)
changeset 355575da670d57118
parent 35556 730fdfbbd5f8
child 35558 bb088a6fafbc
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
src/HOLCF/Representable.thy
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/Representable.thy	Wed Mar 03 06:48:00 2010 -0800
     1.2 +++ b/src/HOLCF/Representable.thy	Wed Mar 03 07:36:31 2010 -0800
     1.3 @@ -189,21 +189,21 @@
     1.4  
     1.5  lemma deflation_chain_min:
     1.6    assumes chain: "chain d"
     1.7 -  assumes defl: "\<And>i. deflation (d i)"
     1.8 -  shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x"
     1.9 +  assumes defl: "\<And>n. deflation (d n)"
    1.10 +  shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
    1.11  proof (rule linorder_le_cases)
    1.12 -  assume "i \<le> j"
    1.13 -  with chain have "d i \<sqsubseteq> d j" by (rule chain_mono)
    1.14 -  then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x"
    1.15 +  assume "m \<le> n"
    1.16 +  with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
    1.17 +  then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
    1.18      by (rule deflation_below_comp1 [OF defl defl])
    1.19 -  moreover from `i \<le> j` have "min i j = i" by simp
    1.20 +  moreover from `m \<le> n` have "min m n = m" by simp
    1.21    ultimately show ?thesis by simp
    1.22  next
    1.23 -  assume "j \<le> i"
    1.24 -  with chain have "d j \<sqsubseteq> d i" by (rule chain_mono)
    1.25 -  then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x"
    1.26 +  assume "n \<le> m"
    1.27 +  with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
    1.28 +  then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
    1.29      by (rule deflation_below_comp2 [OF defl defl])
    1.30 -  moreover from `j \<le> i` have "min i j = j" by simp
    1.31 +  moreover from `n \<le> m` have "min m n = n" by simp
    1.32    ultimately show ?thesis by simp
    1.33  qed
    1.34  
     2.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Mar 03 06:48:00 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Mar 03 07:36:31 2010 -0800
     2.3 @@ -627,8 +627,8 @@
     2.4      (* prove lub of take equals ID *)
     2.5      fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
     2.6        let
     2.7 -        val i = Free ("i", natT);
     2.8 -        val goal = mk_eqs (mk_lub (lambda i (take_const $ i)), mk_ID lhsT);
     2.9 +        val n = Free ("n", natT);
    2.10 +        val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT);
    2.11          val tac =
    2.12              EVERY
    2.13              [rtac @{thm trans} 1, rtac map_ID_thm 2,
     3.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 06:48:00 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 07:36:31 2010 -0800
     3.3 @@ -230,10 +230,10 @@
     3.4            (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
     3.5      val take_rhss =
     3.6        let
     3.7 -        val i = Free ("i", HOLogic.natT);
     3.8 -        val rhs = mk_iterate (i, take_functional)
     3.9 +        val n = Free ("n", HOLogic.natT);
    3.10 +        val rhs = mk_iterate (n, take_functional);
    3.11        in
    3.12 -        map (Term.lambda i o snd) (mk_projs dom_binds rhs)
    3.13 +        map (lambda n o snd) (mk_projs dom_binds rhs)
    3.14        end;
    3.15  
    3.16      (* define take constants *)
    3.17 @@ -284,12 +284,12 @@
    3.18        fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
    3.19  
    3.20      (* prove take_Suc lemmas *)
    3.21 -    val i = Free ("i", natT);
    3.22 -    val take_is = map (fn t => t $ i) take_consts;
    3.23 +    val n = Free ("n", natT);
    3.24 +    val take_is = map (fn t => t $ n) take_consts;
    3.25      fun prove_take_Suc
    3.26            (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
    3.27        let
    3.28 -        val lhs = take_const $ (@{term Suc} $ i);
    3.29 +        val lhs = take_const $ (@{term Suc} $ n);
    3.30          val body = map_of_typ thy (newTs ~~ take_is) rhsT;
    3.31          val rhs = mk_cfcomp2 (rep_abs, body);
    3.32          val goal = mk_eqs (lhs, rhs);
    3.33 @@ -308,8 +308,8 @@
    3.34      val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
    3.35      val deflation_take_thm =
    3.36        let
    3.37 -        val i = Free ("i", natT);
    3.38 -        fun mk_goal take_const = mk_deflation (take_const $ i);
    3.39 +        val n = Free ("n", natT);
    3.40 +        fun mk_goal take_const = mk_deflation (take_const $ n);
    3.41          val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
    3.42          val adm_rules =
    3.43            @{thms adm_conj adm_subst [OF _ adm_deflation]
    3.44 @@ -344,7 +344,7 @@
    3.45      (* prove strictness of take functions *)
    3.46      fun prove_take_strict (take_const, dname) thy =
    3.47        let
    3.48 -        val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
    3.49 +        val goal = mk_trp (mk_strict (take_const $ Free ("n", natT)));
    3.50          val tac = rtac @{thm deflation_strict} 1
    3.51                    THEN resolve_tac deflation_take_thms 1;
    3.52          val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
    3.53 @@ -358,7 +358,8 @@
    3.54      fun prove_take_take ((chain_take, deflation_take), dname) thy =
    3.55        let
    3.56          val take_take_thm =
    3.57 -            @{thm deflation_chain_min} OF [chain_take, deflation_take];
    3.58 +            Drule.export_without_context
    3.59 +            (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
    3.60        in
    3.61          add_qualified_thm "take_take" (dname, take_take_thm) thy
    3.62        end;
    3.63 @@ -374,10 +375,10 @@
    3.64          val (finite_const, thy) =
    3.65            Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
    3.66          val x = Free ("x", lhsT);
    3.67 -        val i = Free ("i", natT);
    3.68 +        val n = Free ("n", natT);
    3.69          val finite_rhs =
    3.70            lambda x (HOLogic.exists_const natT $
    3.71 -            (lambda i (mk_eq (mk_capply (take_const $ i, x), x))));
    3.72 +            (lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
    3.73          val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
    3.74          val (finite_def_thm, thy) =
    3.75            thy
     4.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 06:48:00 2010 -0800
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 07:36:31 2010 -0800
     4.3 @@ -199,7 +199,7 @@
     4.4            [simp_tac (HOL_basic_ss addsimps rules) 1,
     4.5             asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
     4.6      in pg con_appls goal (K tacs) end;
     4.7 -  val take_apps = map (Drule.export_without_context o one_take_app) cons;
     4.8 +  val take_apps = map one_take_app cons;
     4.9  in
    4.10    val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
    4.11  end;
    4.12 @@ -438,13 +438,15 @@
    4.13    val take_lemmas =
    4.14      let
    4.15        fun take_lemma (ax_chain_take, ax_lub_take) =
    4.16 -        @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take];
    4.17 +        Drule.export_without_context
    4.18 +        (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
    4.19      in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
    4.20  
    4.21    val axs_reach =
    4.22      let
    4.23        fun reach (ax_chain_take, ax_lub_take) =
    4.24 -        @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take];
    4.25 +        Drule.export_without_context
    4.26 +        (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
    4.27      in map reach (axs_chain_take ~~ axs_lub_take) end;
    4.28  
    4.29  (* ----- theorems concerning finiteness and induction ----------------------- *)
     5.1 --- a/src/HOLCF/ex/Stream.thy	Wed Mar 03 06:48:00 2010 -0800
     5.2 +++ b/src/HOLCF/ex/Stream.thy	Wed Mar 03 07:36:31 2010 -0800
     5.3 @@ -290,12 +290,12 @@
     5.4  
     5.5  lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
     5.6  apply (simp add: stream.finite_def,auto)
     5.7 -apply (rule_tac x="Suc i" in exI)
     5.8 +apply (rule_tac x="Suc n" in exI)
     5.9  by (simp add: stream_take_lemma4)
    5.10  
    5.11  lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
    5.12  apply (simp add: stream.finite_def, auto)
    5.13 -apply (rule_tac x="i" in exI)
    5.14 +apply (rule_tac x="n" in exI)
    5.15  by (erule stream_take_lemma3,simp)
    5.16  
    5.17  lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"