generate separate qualified theorem name for each type's reach and take_lemma
authorhuffman
Sun Mar 07 16:39:31 2010 -0800 (2010-03-07)
changeset 35642f478d5a9d238
parent 35641 a17bc4cec23a
child 35643 965c24dd6856
generate separate qualified theorem name for each type's reach and take_lemma
src/HOLCF/FOCUS/Buffer.thy
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/ex/Dagstuhl.thy
src/HOLCF/ex/Domain_ex.thy
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/FOCUS/Buffer.thy	Sun Mar 07 16:12:01 2010 -0800
     1.2 +++ b/src/HOLCF/FOCUS/Buffer.thy	Sun Mar 07 16:39:31 2010 -0800
     1.3 @@ -284,7 +284,7 @@
     1.4  done
     1.5  
     1.6  lemma BufAC_Asm_cong: "\<lbrakk>f \<in> BufEq; ff \<in> BufEq; s \<in> BufAC_Asm\<rbrakk> \<Longrightarrow> f\<cdot>s = ff\<cdot>s"
     1.7 -apply (rule stream.take_lemmas)
     1.8 +apply (rule stream.take_lemma)
     1.9  apply (erule (2) BufAC_Asm_cong_lemma)
    1.10  done
    1.11  
     2.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Mar 07 16:12:01 2010 -0800
     2.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Mar 07 16:39:31 2010 -0800
     2.3 @@ -467,7 +467,7 @@
     2.4    LastActExtsch A schA & LastActExtsch B schB   
     2.5    --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
     2.6  apply (intro strip)
     2.7 -apply (rule seq.take_lemmas)
     2.8 +apply (rule seq.take_lemma)
     2.9  apply (rule mp)
    2.10  prefer 2 apply assumption
    2.11  back back back back
    2.12 @@ -687,7 +687,7 @@
    2.13    LastActExtsch A schA & LastActExtsch B schB   
    2.14    --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
    2.15  apply (intro strip)
    2.16 -apply (rule seq.take_lemmas)
    2.17 +apply (rule seq.take_lemma)
    2.18  apply (rule mp)
    2.19  prefer 2 apply assumption
    2.20  back back back back
     3.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Mar 07 16:12:01 2010 -0800
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Mar 07 16:39:31 2010 -0800
     3.3 @@ -850,7 +850,7 @@
     3.4  
     3.5  lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
     3.6  apply (rule iffI)
     3.7 -apply (rule seq.take_lemmas)
     3.8 +apply (rule seq.take_lemma)
     3.9  apply auto
    3.10  done
    3.11  
    3.12 @@ -936,7 +936,7 @@
    3.13                 ==> A x --> (f x)=(g x)"
    3.14  apply (case_tac "Forall Q x")
    3.15  apply (auto dest!: divide_Seq3)
    3.16 -apply (rule seq.take_lemmas)
    3.17 +apply (rule seq.take_lemma)
    3.18  apply auto
    3.19  done
    3.20  
    3.21 @@ -957,7 +957,7 @@
    3.22                                = seq_take (Suc n)$(g (s1 @@ y>>s2)) |]
    3.23                 ==> A x --> (f x)=(g x)"
    3.24  apply (rule impI)
    3.25 -apply (rule seq.take_lemmas)
    3.26 +apply (rule seq.take_lemma)
    3.27  apply (rule mp)
    3.28  prefer 2 apply assumption
    3.29  apply (rule_tac x="x" in spec)
    3.30 @@ -978,7 +978,7 @@
    3.31                                = seq_take n$(g (s1 @@ y>>s2)) |]
    3.32                 ==> A x --> (f x)=(g x)"
    3.33  apply (rule impI)
    3.34 -apply (rule seq.take_lemmas)
    3.35 +apply (rule seq.take_lemma)
    3.36  apply (rule mp)
    3.37  prefer 2 apply assumption
    3.38  apply (rule_tac x="x" in spec)
    3.39 @@ -1000,7 +1000,7 @@
    3.40                           = seq_take (Suc n)$(g (y>>s)) |]
    3.41                 ==> A x --> (f x)=(g x)"
    3.42  apply (rule impI)
    3.43 -apply (rule seq.take_lemmas)
    3.44 +apply (rule seq.take_lemma)
    3.45  apply (rule mp)
    3.46  prefer 2 apply assumption
    3.47  apply (rule_tac x="x" in spec)
     4.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Mar 07 16:12:01 2010 -0800
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Mar 07 16:39:31 2010 -0800
     4.3 @@ -633,20 +633,26 @@
     4.4    fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
     4.5    val axs_chain_take = map (ga "chain_take") dnames;
     4.6    val axs_lub_take   = map (ga "lub_take"  ) dnames;
     4.7 -in
     4.8 -  val _ = trace " Proving take_lemmas...";
     4.9 -  val take_lemmas =
    4.10 +  fun take_thms ((ax_chain_take, ax_lub_take), dname) thy =
    4.11      let
    4.12 -      fun take_lemma (ax_chain_take, ax_lub_take) =
    4.13 +      val dnam = Long_Name.base_name dname;
    4.14 +      val take_lemma =
    4.15            Drule.export_without_context
    4.16              (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
    4.17 -    in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
    4.18 -  val axs_reach =
    4.19 -    let
    4.20 -      fun reach (ax_chain_take, ax_lub_take) =
    4.21 +      val reach =
    4.22            Drule.export_without_context
    4.23              (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
    4.24 -    in map reach (axs_chain_take ~~ axs_lub_take) end;
    4.25 +      val thy =
    4.26 +          thy |> Sign.add_path dnam
    4.27 +              |> snd o PureThy.add_thms [
    4.28 +                 ((Binding.name "take_lemma", take_lemma), []),
    4.29 +                 ((Binding.name "reach"     , reach     ), [])]
    4.30 +              |> Sign.parent_path;
    4.31 +    in ((take_lemma, reach), thy) end;
    4.32 +in
    4.33 +  val ((take_lemmas, axs_reach), thy) =
    4.34 +      fold_map take_thms (axs_chain_take ~~ axs_lub_take ~~ dnames) thy
    4.35 +      |>> ListPair.unzip;
    4.36  end;
    4.37  
    4.38  val take_rews =
    4.39 @@ -661,10 +667,7 @@
    4.40      if is_indirect then thy else
    4.41      prove_coinduction (comp_dnam, eqs) take_lemmas thy;
    4.42  
    4.43 -in thy |> Sign.add_path comp_dnam
    4.44 -       |> snd o PureThy.add_thmss [
    4.45 -           ((Binding.name "take_lemmas", take_lemmas ), []),
    4.46 -           ((Binding.name "reach"      , axs_reach   ), [])]
    4.47 -       |> Sign.parent_path |> pair take_rews
    4.48 +in
    4.49 +  (take_rews, thy)
    4.50  end; (* let *)
    4.51  end; (* struct *)
     5.1 --- a/src/HOLCF/ex/Dagstuhl.thy	Sun Mar 07 16:12:01 2010 -0800
     5.2 +++ b/src/HOLCF/ex/Dagstuhl.thy	Sun Mar 07 16:39:31 2010 -0800
     5.3 @@ -52,7 +52,7 @@
     5.4    done
     5.5  
     5.6  lemma wir_moel: "YS = YYS"
     5.7 -  apply (rule stream.take_lemmas)
     5.8 +  apply (rule stream.take_lemma)
     5.9    apply (induct_tac n)
    5.10    apply (simp (no_asm))
    5.11    apply (subst YS_def2)
     6.1 --- a/src/HOLCF/ex/Domain_ex.thy	Sun Mar 07 16:12:01 2010 -0800
     6.2 +++ b/src/HOLCF/ex/Domain_ex.thy	Sun Mar 07 16:39:31 2010 -0800
     6.3 @@ -166,7 +166,7 @@
     6.4  thm tree.chain_take
     6.5  thm tree.take_take
     6.6  thm tree.deflation_take
     6.7 -thm tree.take_lemmas
     6.8 +thm tree.take_lemma
     6.9  thm tree.lub_take
    6.10  thm tree.reach
    6.11  thm tree.finite_ind
     7.1 --- a/src/HOLCF/ex/Stream.thy	Sun Mar 07 16:12:01 2010 -0800
     7.2 +++ b/src/HOLCF/ex/Stream.thy	Sun Mar 07 16:39:31 2010 -0800
     7.3 @@ -845,7 +845,7 @@
     7.4  by blast+
     7.5  
     7.6  lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2"
     7.7 -by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast)
     7.8 +by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast)
     7.9  
    7.10  (* ----------------------------------------------------------------------- *)
    7.11     subsection "finiteness"
    7.12 @@ -912,7 +912,7 @@
    7.13     apply (simp+,rule slen_take_lemma3 [of _ s1 s2])
    7.14    apply (simp+,rule_tac x="UU" in exI)
    7.15  apply (insert slen_take_lemma3 [of _ s1 s2])
    7.16 -by (rule stream.take_lemmas,simp)
    7.17 +by (rule stream.take_lemma,simp)
    7.18  
    7.19  (* ----------------------------------------------------------------------- *)
    7.20     subsection "continuity"