# HG changeset patch
# User huffman
# Date 1268008771 28800
# Node ID f478d5a9d23833e61bbb4cc9c61475e6c7802c58
# Parent  a17bc4cec23ad6a5a8137f979c3bb87f41bd703a
generate separate qualified theorem name for each type's reach and take_lemma

diff -r a17bc4cec23a -r f478d5a9d238 src/HOLCF/FOCUS/Buffer.thy
--- a/src/HOLCF/FOCUS/Buffer.thy	Sun Mar 07 16:12:01 2010 -0800
+++ b/src/HOLCF/FOCUS/Buffer.thy	Sun Mar 07 16:39:31 2010 -0800
@@ -284,7 +284,7 @@
 done
 
 lemma BufAC_Asm_cong: "\<lbrakk>f \<in> BufEq; ff \<in> BufEq; s \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> f\<cdot>s = ff\<cdot>s"
-apply (rule stream.take_lemmas)
+apply (rule stream.take_lemma)
 apply (erule (2) BufAC_Asm_cong_lemma)
 done
 
diff -r a17bc4cec23a -r f478d5a9d238 src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Mar 07 16:12:01 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Mar 07 16:39:31 2010 -0800
@@ -467,7 +467,7 @@
   LastActExtsch A schA & LastActExtsch B schB   
   --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
 apply (intro strip)
-apply (rule seq.take_lemmas)
+apply (rule seq.take_lemma)
 apply (rule mp)
 prefer 2 apply assumption
 back back back back
@@ -687,7 +687,7 @@
   LastActExtsch A schA & LastActExtsch B schB   
   --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
 apply (intro strip)
-apply (rule seq.take_lemmas)
+apply (rule seq.take_lemma)
 apply (rule mp)
 prefer 2 apply assumption
 back back back back
diff -r a17bc4cec23a -r f478d5a9d238 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Mar 07 16:12:01 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Mar 07 16:39:31 2010 -0800
@@ -850,7 +850,7 @@
 
 lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
 apply (rule iffI)
-apply (rule seq.take_lemmas)
+apply (rule seq.take_lemma)
 apply auto
 done
 
@@ -936,7 +936,7 @@
                ==> A x --> (f x)=(g x)"
 apply (case_tac "Forall Q x")
 apply (auto dest!: divide_Seq3)
-apply (rule seq.take_lemmas)
+apply (rule seq.take_lemma)
 apply auto
 done
 
@@ -957,7 +957,7 @@
                               = seq_take (Suc n)$(g (s1 @@ y>>s2)) |]
                ==> A x --> (f x)=(g x)"
 apply (rule impI)
-apply (rule seq.take_lemmas)
+apply (rule seq.take_lemma)
 apply (rule mp)
 prefer 2 apply assumption
 apply (rule_tac x="x" in spec)
@@ -978,7 +978,7 @@
                               = seq_take n$(g (s1 @@ y>>s2)) |]
                ==> A x --> (f x)=(g x)"
 apply (rule impI)
-apply (rule seq.take_lemmas)
+apply (rule seq.take_lemma)
 apply (rule mp)
 prefer 2 apply assumption
 apply (rule_tac x="x" in spec)
@@ -1000,7 +1000,7 @@
                          = seq_take (Suc n)$(g (y>>s)) |]
                ==> A x --> (f x)=(g x)"
 apply (rule impI)
-apply (rule seq.take_lemmas)
+apply (rule seq.take_lemma)
 apply (rule mp)
 prefer 2 apply assumption
 apply (rule_tac x="x" in spec)
diff -r a17bc4cec23a -r f478d5a9d238 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Mar 07 16:12:01 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Mar 07 16:39:31 2010 -0800
@@ -633,20 +633,26 @@
   fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
   val axs_chain_take = map (ga "chain_take") dnames;
   val axs_lub_take   = map (ga "lub_take"  ) dnames;
-in
-  val _ = trace " Proving take_lemmas...";
-  val take_lemmas =
+  fun take_thms ((ax_chain_take, ax_lub_take), dname) thy =
     let
-      fun take_lemma (ax_chain_take, ax_lub_take) =
+      val dnam = Long_Name.base_name dname;
+      val take_lemma =
           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) =
+      val reach =
           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;
+      val thy =
+          thy |> Sign.add_path dnam
+              |> snd o PureThy.add_thms [
+                 ((Binding.name "take_lemma", take_lemma), []),
+                 ((Binding.name "reach"     , reach     ), [])]
+              |> Sign.parent_path;
+    in ((take_lemma, reach), thy) end;
+in
+  val ((take_lemmas, axs_reach), thy) =
+      fold_map take_thms (axs_chain_take ~~ axs_lub_take ~~ dnames) thy
+      |>> ListPair.unzip;
 end;
 
 val take_rews =
@@ -661,10 +667,7 @@
     if is_indirect then thy else
     prove_coinduction (comp_dnam, eqs) take_lemmas thy;
 
-in thy |> Sign.add_path comp_dnam
-       |> snd o PureThy.add_thmss [
-           ((Binding.name "take_lemmas", take_lemmas ), []),
-           ((Binding.name "reach"      , axs_reach   ), [])]
-       |> Sign.parent_path |> pair take_rews
+in
+  (take_rews, thy)
 end; (* let *)
 end; (* struct *)
diff -r a17bc4cec23a -r f478d5a9d238 src/HOLCF/ex/Dagstuhl.thy
--- a/src/HOLCF/ex/Dagstuhl.thy	Sun Mar 07 16:12:01 2010 -0800
+++ b/src/HOLCF/ex/Dagstuhl.thy	Sun Mar 07 16:39:31 2010 -0800
@@ -52,7 +52,7 @@
   done
 
 lemma wir_moel: "YS = YYS"
-  apply (rule stream.take_lemmas)
+  apply (rule stream.take_lemma)
   apply (induct_tac n)
   apply (simp (no_asm))
   apply (subst YS_def2)
diff -r a17bc4cec23a -r f478d5a9d238 src/HOLCF/ex/Domain_ex.thy
--- a/src/HOLCF/ex/Domain_ex.thy	Sun Mar 07 16:12:01 2010 -0800
+++ b/src/HOLCF/ex/Domain_ex.thy	Sun Mar 07 16:39:31 2010 -0800
@@ -166,7 +166,7 @@
 thm tree.chain_take
 thm tree.take_take
 thm tree.deflation_take
-thm tree.take_lemmas
+thm tree.take_lemma
 thm tree.lub_take
 thm tree.reach
 thm tree.finite_ind
diff -r a17bc4cec23a -r f478d5a9d238 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Sun Mar 07 16:12:01 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy	Sun Mar 07 16:39:31 2010 -0800
@@ -845,7 +845,7 @@
 by blast+
 
 lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2"
-by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast)
+by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast)
 
 (* ----------------------------------------------------------------------- *)
    subsection "finiteness"
@@ -912,7 +912,7 @@
    apply (simp+,rule slen_take_lemma3 [of _ s1 s2])
   apply (simp+,rule_tac x="UU" in exI)
 apply (insert slen_take_lemma3 [of _ s1 s2])
-by (rule stream.take_lemmas,simp)
+by (rule stream.take_lemma,simp)
 
 (* ----------------------------------------------------------------------- *)
    subsection "continuity"