--- a/src/HOLCF/Cfun.thy Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/Cfun.thy Sun Mar 07 17:33:01 2010 -0800
@@ -126,9 +126,12 @@
lemma Rep_CFun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
by (simp add: Rep_CFun_strict)
+lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
+by (simp add: inst_fun_pcpo [symmetric] Abs_CFun_strict)
+
text {* for compatibility with old HOLCF-Version *}
lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
-by (simp add: inst_fun_pcpo [symmetric] Abs_CFun_strict)
+by simp
subsection {* Basic properties of continuous functions *}
--- a/src/HOLCF/FOCUS/Buffer.thy Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/FOCUS/Buffer.thy Sun Mar 07 17:33:01 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
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Sun Mar 07 17:33:01 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
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sun Mar 07 17:33:01 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)
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Mar 07 17:33:01 2010 -0800
@@ -478,6 +478,7 @@
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
val bottom_rules =
@{thms fst_strict snd_strict isodefl_bottom simp_thms};
+ val REP_simps = map (fn th => th RS sym) (RepData.get thy);
val isodefl_rules =
@{thms conjI isodefl_ID_REP}
@ isodefl_abs_rep_thms
@@ -493,6 +494,7 @@
simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
simp_tac beta_ss 1,
simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
+ simp_tac (HOL_basic_ss addsimps REP_simps) 1,
REPEAT (etac @{thm conjE} 1),
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
end;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 17:33:01 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 *)
--- a/src/HOLCF/ex/Dagstuhl.thy Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/ex/Dagstuhl.thy Sun Mar 07 17:33:01 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)
--- a/src/HOLCF/ex/Domain_ex.thy Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/ex/Domain_ex.thy Sun Mar 07 17:33:01 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
--- a/src/HOLCF/ex/Stream.thy Sun Mar 07 22:36:36 2010 +0100
+++ b/src/HOLCF/ex/Stream.thy Sun Mar 07 17:33:01 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"