# 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: "\f \ BufEq; ff \ BufEq; s \ BufAC_Asm\ \ f\s = ff\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"