--- a/src/HOLCF/FOCUS/Fstream.thy Mon Mar 30 12:07:59 2009 -0700
+++ b/src/HOLCF/FOCUS/Fstream.thy Mon Mar 30 13:55:05 2009 -0700
@@ -87,9 +87,6 @@
apply (cut_tac fscons_not_empty)
apply (fast dest: eq_UU_iff [THEN iffD2])
apply (simp add: fscons_def2)
-apply (drule stream_flat_prefix)
-apply (rule Def_not_UU)
-apply (fast)
done
lemma fstream_prefix' [simp]:
--- a/src/HOLCF/FOCUS/Fstreams.thy Mon Mar 30 12:07:59 2009 -0700
+++ b/src/HOLCF/FOCUS/Fstreams.thy Mon Mar 30 13:55:05 2009 -0700
@@ -173,13 +173,12 @@
lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt & s << tt"
apply (simp add: fsingleton_def2)
apply (insert stream_prefix [of "Def a" s t], auto)
-by (auto simp add: stream.inverts)
+done
lemma fstreams_prefix': "x << <a> ooo z = (x = <> | (EX y. x = <a> ooo y & y << z))"
apply (auto, case_tac "x=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (simp add: fsingleton_def2, auto)
-apply (auto simp add: stream.inverts)
apply (drule ax_flat, simp)
by (erule sconc_mono)
@@ -197,8 +196,7 @@
by auto
lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
-apply (simp add: fsingleton_def2)
-by (auto simp add: stream.inverts)
+by (simp add: fsingleton_def2)
lemma fsmap_UU[simp]: "fsmap f$UU = UU"
by (simp add: fsmap_def)
@@ -220,7 +218,6 @@
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (case_tac "y=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (auto simp add: stream.inverts)
apply (simp add: flat_less_iff)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
@@ -344,7 +341,3 @@
by (erule ch2ch_monofun, simp)
end
-
-
-
-
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 30 12:07:59 2009 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 30 13:55:05 2009 -0700
@@ -322,7 +322,6 @@
lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
apply (simp add: Consq_def2)
-apply (simp add: seq.inverts)
done
lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
@@ -661,7 +660,7 @@
(Forall (%x. ~P x) ys & Finite ys)"
apply (rule_tac x="ys" in Seq_induct)
(* adm *)
-apply (simp add: seq.compacts Forall_def sforall_def)
+apply (simp add: Forall_def sforall_def)
(* base cases *)
apply simp
apply simp
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Mon Mar 30 12:07:59 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Mon Mar 30 13:55:05 2009 -0700
@@ -607,23 +607,23 @@
in
thy
|> Sign.add_path (Long_Name.base_name dname)
- |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
- ("iso_rews" , iso_rews ),
- ("exhaust" , [exhaust] ),
- ("casedist" , [casedist]),
- ("when_rews", when_rews ),
- ("compacts", con_compacts),
- ("con_rews", con_rews),
- ("sel_rews", sel_rews),
- ("dis_rews", dis_rews),
- ("pat_rews", pat_rews),
- ("dist_les", dist_les),
- ("dist_eqs", dist_eqs),
- ("inverts" , inverts ),
- ("injects" , injects ),
- ("copy_rews", copy_rews)])))
- |> (snd o PureThy.add_thmss
- [((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])])
+ |> (snd o PureThy.add_thmss [
+ ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
+ ((Binding.name "exhaust" , [exhaust] ), []),
+ ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]),
+ ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
+ ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
+ ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
+ ((Binding.name "sel_rews", sel_rews), [Simplifier.simp_add]),
+ ((Binding.name "dis_rews", dis_rews), [Simplifier.simp_add]),
+ ((Binding.name "pat_rews", pat_rews), [Simplifier.simp_add]),
+ ((Binding.name "dist_les", dist_les), [Simplifier.simp_add]),
+ ((Binding.name "dist_eqs", dist_eqs), [Simplifier.simp_add]),
+ ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
+ ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
+ ((Binding.name "copy_rews", copy_rews), [Simplifier.simp_add]),
+ ((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])
+ ])
|> Sign.parent_path
|> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
pat_rews @ dist_les @ dist_eqs @ copy_rews)
--- a/src/HOLCF/ex/Stream.thy Mon Mar 30 12:07:59 2009 -0700
+++ b/src/HOLCF/ex/Stream.thy Mon Mar 30 13:55:05 2009 -0700
@@ -81,15 +81,13 @@
lemma stream_prefix:
"[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"
-apply (insert stream.exhaust [of t], auto)
-by (auto simp add: stream.inverts)
+by (insert stream.exhaust [of t], auto)
lemma stream_prefix':
"b ~= UU ==> x << b && z =
(x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"
apply (case_tac "x=UU",auto)
-apply (drule stream_exhaust_eq [THEN iffD1],auto)
-by (auto simp add: stream.inverts)
+by (drule stream_exhaust_eq [THEN iffD1],auto)
(*
@@ -100,7 +98,6 @@
lemma stream_flat_prefix:
"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
apply (case_tac "y=UU",auto)
-apply (auto simp add: stream.inverts)
by (drule ax_flat,simp)
@@ -280,17 +277,17 @@
section "coinduction"
lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"
-apply (simp add: stream.bisim_def,clarsimp)
-apply (case_tac "x=UU",clarsimp)
-apply (erule_tac x="UU" in allE,simp)
-apply (case_tac "x'=UU",simp)
-apply (drule stream_exhaust_eq [THEN iffD1],auto)+
-apply (case_tac "x'=UU",auto)
-apply (erule_tac x="a && y" in allE)
-apply (erule_tac x="UU" in allE)+
-apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
-apply (erule_tac x="a && y" in allE)
-apply (erule_tac x="aa && ya" in allE)
+ apply (simp add: stream.bisim_def,clarsimp)
+ apply (case_tac "x=UU",clarsimp)
+ apply (erule_tac x="UU" in allE,simp)
+ apply (case_tac "x'=UU",simp)
+ apply (drule stream_exhaust_eq [THEN iffD1],auto)+
+ apply (case_tac "x'=UU",auto)
+ apply (erule_tac x="a && y" in allE)
+ apply (erule_tac x="UU" in allE)+
+ apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
+ apply (erule_tac x="a && y" in allE)
+ apply (erule_tac x="aa && ya" in allE) back
by auto
@@ -327,7 +324,6 @@
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
-apply (auto simp add: stream.inverts)
apply (erule_tac x="y" in allE, simp)
by (rule stream_finite_lemma1, simp)
@@ -374,8 +370,6 @@
lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & Fin n < #y)"
apply (auto, case_tac "x=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (rule_tac x="a" in exI)
-apply (rule_tac x="y" in exI, simp)
apply (case_tac "#y") apply simp_all
apply (case_tac "#y") apply simp_all
done
@@ -387,15 +381,11 @@
by (simp add: slen_def)
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
-apply (rule stream.casedist [of x], auto)
-apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
-apply (simp add: zero_inat_def)
-apply (subgoal_tac "s=y & aa=a", simp)
-apply (simp_all add: not_less iSuc_Fin)
-apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
-apply (case_tac "aa=UU", auto)
-apply (erule_tac x="a" in allE, simp)
-apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (rule stream.casedist [of x], auto)
+ apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
+ apply (simp add: zero_inat_def)
+ apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
done
lemma slen_take_lemma4 [rule_format]:
@@ -463,8 +453,7 @@
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (erule_tac x="y" in allE, auto)
-by (auto simp add: stream.inverts)
+done
lemma slen_mono: "s << t ==> #s <= #t"
apply (case_tac "stream_finite t")
@@ -493,7 +482,6 @@
apply (case_tac "y=UU", clarsimp)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
apply (erule_tac x="ya" in allE, simp)
-apply (auto simp add: stream.inverts)
by (drule ax_flat, simp)
lemma slen_strict_mono_lemma:
@@ -501,7 +489,6 @@
apply (erule stream_finite_ind, auto)
apply (case_tac "sa=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
-apply (simp add: stream.inverts, clarsimp)
by (drule ax_flat, simp)
lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
@@ -653,7 +640,7 @@
apply (simp add: i_th_def i_rt_Suc_back)
apply (rule stream.casedist [of "i_rt n s1"],simp)
apply (rule stream.casedist [of "i_rt n s2"],auto)
-by (intro monofun_cfun, auto)
+done
lemma i_th_stream_take_Suc [rule_format]:
"ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"