# HG changeset patch
# User huffman
# Date 1267630591 28800
# Node ID 5da670d57118ee1ee45962f4fb0d55e8ea106f33
# Parent  730fdfbbd5f81d59c0566fb3891eba9ee0b49920
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate

diff -r 730fdfbbd5f8 -r 5da670d57118 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Wed Mar 03 06:48:00 2010 -0800
+++ b/src/HOLCF/Representable.thy	Wed Mar 03 07:36:31 2010 -0800
@@ -189,21 +189,21 @@
 
 lemma deflation_chain_min:
   assumes chain: "chain d"
-  assumes defl: "\<And>i. deflation (d i)"
-  shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x"
+  assumes defl: "\<And>n. deflation (d n)"
+  shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
 proof (rule linorder_le_cases)
-  assume "i \<le> j"
-  with chain have "d i \<sqsubseteq> d j" by (rule chain_mono)
-  then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x"
+  assume "m \<le> n"
+  with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
+  then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
     by (rule deflation_below_comp1 [OF defl defl])
-  moreover from `i \<le> j` have "min i j = i" by simp
+  moreover from `m \<le> n` have "min m n = m" by simp
   ultimately show ?thesis by simp
 next
-  assume "j \<le> i"
-  with chain have "d j \<sqsubseteq> d i" by (rule chain_mono)
-  then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x"
+  assume "n \<le> m"
+  with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
+  then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
     by (rule deflation_below_comp2 [OF defl defl])
-  moreover from `j \<le> i` have "min i j = j" by simp
+  moreover from `n \<le> m` have "min m n = n" by simp
   ultimately show ?thesis by simp
 qed
 
diff -r 730fdfbbd5f8 -r 5da670d57118 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Mar 03 06:48:00 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Mar 03 07:36:31 2010 -0800
@@ -627,8 +627,8 @@
     (* prove lub of take equals ID *)
     fun prove_lub_take (((bind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
       let
-        val i = Free ("i", natT);
-        val goal = mk_eqs (mk_lub (lambda i (take_const $ i)), mk_ID lhsT);
+        val n = Free ("n", natT);
+        val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT);
         val tac =
             EVERY
             [rtac @{thm trans} 1, rtac map_ID_thm 2,
diff -r 730fdfbbd5f8 -r 5da670d57118 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 06:48:00 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 07:36:31 2010 -0800
@@ -230,10 +230,10 @@
           (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
     val take_rhss =
       let
-        val i = Free ("i", HOLogic.natT);
-        val rhs = mk_iterate (i, take_functional)
+        val n = Free ("n", HOLogic.natT);
+        val rhs = mk_iterate (n, take_functional);
       in
-        map (Term.lambda i o snd) (mk_projs dom_binds rhs)
+        map (lambda n o snd) (mk_projs dom_binds rhs)
       end;
 
     (* define take constants *)
@@ -284,12 +284,12 @@
       fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
 
     (* prove take_Suc lemmas *)
-    val i = Free ("i", natT);
-    val take_is = map (fn t => t $ i) take_consts;
+    val n = Free ("n", natT);
+    val take_is = map (fn t => t $ n) take_consts;
     fun prove_take_Suc
           (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
       let
-        val lhs = take_const $ (@{term Suc} $ i);
+        val lhs = take_const $ (@{term Suc} $ n);
         val body = map_of_typ thy (newTs ~~ take_is) rhsT;
         val rhs = mk_cfcomp2 (rep_abs, body);
         val goal = mk_eqs (lhs, rhs);
@@ -308,8 +308,8 @@
     val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
     val deflation_take_thm =
       let
-        val i = Free ("i", natT);
-        fun mk_goal take_const = mk_deflation (take_const $ i);
+        val n = Free ("n", natT);
+        fun mk_goal take_const = mk_deflation (take_const $ n);
         val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
         val adm_rules =
           @{thms adm_conj adm_subst [OF _ adm_deflation]
@@ -344,7 +344,7 @@
     (* prove strictness of take functions *)
     fun prove_take_strict (take_const, dname) thy =
       let
-        val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
+        val goal = mk_trp (mk_strict (take_const $ Free ("n", natT)));
         val tac = rtac @{thm deflation_strict} 1
                   THEN resolve_tac deflation_take_thms 1;
         val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
@@ -358,7 +358,8 @@
     fun prove_take_take ((chain_take, deflation_take), dname) thy =
       let
         val take_take_thm =
-            @{thm deflation_chain_min} OF [chain_take, deflation_take];
+            Drule.export_without_context
+            (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
       in
         add_qualified_thm "take_take" (dname, take_take_thm) thy
       end;
@@ -374,10 +375,10 @@
         val (finite_const, thy) =
           Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
         val x = Free ("x", lhsT);
-        val i = Free ("i", natT);
+        val n = Free ("n", natT);
         val finite_rhs =
           lambda x (HOLogic.exists_const natT $
-            (lambda i (mk_eq (mk_capply (take_const $ i, x), x))));
+            (lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
         val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
         val (finite_def_thm, thy) =
           thy
diff -r 730fdfbbd5f8 -r 5da670d57118 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 06:48:00 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 07:36:31 2010 -0800
@@ -199,7 +199,7 @@
           [simp_tac (HOL_basic_ss addsimps rules) 1,
            asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
     in pg con_appls goal (K tacs) end;
-  val take_apps = map (Drule.export_without_context o one_take_app) cons;
+  val take_apps = map one_take_app cons;
 in
   val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
 end;
@@ -438,13 +438,15 @@
   val take_lemmas =
     let
       fun take_lemma (ax_chain_take, ax_lub_take) =
-        @{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take];
+        Drule.export_without_context
+        (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
     in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
 
   val axs_reach =
     let
       fun reach (ax_chain_take, ax_lub_take) =
-        @{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take];
+        Drule.export_without_context
+        (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
     in map reach (axs_chain_take ~~ axs_lub_take) end;
 
 (* ----- theorems concerning finiteness and induction ----------------------- *)
diff -r 730fdfbbd5f8 -r 5da670d57118 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Wed Mar 03 06:48:00 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy	Wed Mar 03 07:36:31 2010 -0800
@@ -290,12 +290,12 @@
 
 lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
 apply (simp add: stream.finite_def,auto)
-apply (rule_tac x="Suc i" in exI)
+apply (rule_tac x="Suc n" in exI)
 by (simp add: stream_take_lemma4)
 
 lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
 apply (simp add: stream.finite_def, auto)
-apply (rule_tac x="i" in exI)
+apply (rule_tac x="n" in exI)
 by (erule stream_take_lemma3,simp)
 
 lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"