# HG changeset patch
# User haftmann
# Date 1213104663 -7200
# Node ID c19be97e4553fdd29144fb5ee52d2265c328f523
# Parent  194aa674c2a168a63e2a899c367afb0f253e91a2
adjusted some proofs involving inats

diff -r 194aa674c2a1 -r c19be97e4553 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Tue Jun 10 15:31:02 2008 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Tue Jun 10 15:31:03 2008 +0200
@@ -60,7 +60,8 @@
 by (simp add: fsingleton_def2)
 
 lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
-apply (case_tac "#s", auto)
+apply (cases "#s")
+apply (auto simp add: iSuc_Fin)
 apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
 by (simp add: sconc_def)
 
diff -r 194aa674c2a1 -r c19be97e4553 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Tue Jun 10 15:31:02 2008 +0200
+++ b/src/HOLCF/ex/Stream.thy	Tue Jun 10 15:31:03 2008 +0200
@@ -350,14 +350,13 @@
 section "slen"
 
 lemma slen_empty [simp]: "#\<bottom> = 0"
-apply (simp add: slen_def stream.finite_def)
-by (simp add: inat_defs Least_equality)
+by (simp add: slen_def stream.finite_def zero_inat_def Least_equality)
 
 lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
 apply (case_tac "stream_finite (x && xs)")
 apply (simp add: slen_def, auto)
-apply (simp add: stream.finite_def, auto)
-apply (rule Least_Suc2,auto)
+apply (simp add: stream.finite_def, auto simp add: iSuc_Fin)
+apply (rule Least_Suc2, auto)
 (*apply (drule sym)*)
 (*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
 apply (erule stream_finite_lemma2, simp)
@@ -376,7 +375,9 @@
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="y" in exI, simp)
-by (simp add: inat_defs split:inat_splits)+
+apply (case_tac "#y") apply simp_all
+apply (case_tac "#y") apply simp_all
+done
 
 lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y &  a ~= \<bottom> &  #y = n)"
 by (rule stream.casedist [of x], auto)
@@ -387,18 +388,20 @@
 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: inat_defs split:inat_splits)
-apply (subgoal_tac "s=y & aa=a",simp)
-apply (simp add: inat_defs split:inat_splits)
-apply (case_tac "aa=UU",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)
-by (simp add: inat_defs split:inat_splits)
+apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+done
 
 lemma slen_take_lemma4 [rule_format]:
   "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n"
-apply (induct_tac n,auto simp add: Fin_0)
-apply (case_tac "s=UU",simp)
-by (drule stream_exhaust_eq [THEN iffD1], auto)
+apply (induct n, auto simp add: Fin_0)
+apply (case_tac "s=UU", simp)
+by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_Fin)
 
 (*
 lemma stream_take_idempotent [simp]:
@@ -426,11 +429,12 @@
 apply (case_tac "x=UU", simp)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
 apply (erule_tac x="y" in allE, auto)
-apply (simp add: inat_defs split:inat_splits)
+apply (simp_all add: not_less iSuc_Fin)
+apply (case_tac "#y") apply simp_all
 apply (case_tac "x=UU", simp)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
 apply (erule_tac x="y" in allE, simp)
-by (simp add: inat_defs split:inat_splits)
+apply (case_tac "#y") by simp_all
 
 lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
 by (simp add: linorder_not_less [symmetric] slen_take_eq)
@@ -472,19 +476,18 @@
 by (insert iterate_Suc2 [of n F x], auto)
 
 lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)"
-apply (induct_tac i, auto)
-apply (case_tac "x=UU", auto)
-apply (simp add: inat_defs)
+apply (induct i, auto)
+apply (case_tac "x=UU", auto simp add: zero_inat_def)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (erule_tac x="y" in allE, auto)
-apply (simp add: inat_defs split:inat_splits)
+apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
 by (simp add: iterate_lemma)
 
 lemma slen_take_lemma3 [rule_format]:
   "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
 apply (induct_tac n, auto)
 apply (case_tac "x=UU", auto)
-apply (simp add: inat_defs)
+apply (simp add: zero_inat_def)
 apply (simp add: Suc_ile_eq)
 apply (case_tac "y=UU", clarsimp)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
@@ -501,9 +504,7 @@
 by (drule ax_flat, simp)
 
 lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
-apply (intro ilessI1, auto)
-apply (simp add: slen_mono)
-by (drule slen_strict_mono_lemma, auto)
+by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma)
 
 lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==>
                      stream_take n$s ~= stream_take (Suc n)$s"
@@ -511,8 +512,7 @@
 apply (subgoal_tac "stream_take n$s ~=s")
  apply (insert slen_take_lemma4 [of n s],auto)
 apply (rule stream.casedist [of s],simp)
-apply (simp add: inat_defs split:inat_splits)
-by (simp add: slen_take_lemma4)
+by (simp add: slen_take_lemma4 iSuc_Fin)
 
 (* ----------------------------------------------------------------------- *)
 (* theorems about smap                                                     *)
@@ -601,9 +601,12 @@
  apply (subgoal_tac "#(i_rt n s)=0")
   apply (case_tac "stream_take n$s = s",simp+)
   apply (insert slen_take_eq [rule_format,of n s],simp)
-  apply (simp add: inat_defs split:inat_splits)
- apply (simp add: slen_take_eq )
-by (simp, insert i_rt_take_lemma1 [of n s],simp)
+  apply (cases "#s") apply (simp_all add: zero_inat_def)
+  apply (simp add: slen_take_eq)
+  apply (cases "#s")
+  using i_rt_take_lemma1 [of n s]
+  apply (simp_all add: zero_inat_def)
+  done
 
 lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
 by (simp add: i_rt_slen slen_take_lemma1)
@@ -616,21 +619,22 @@
 lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl &
                             #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j
                                               --> Fin (j + t) = #x"
-apply (induct_tac n,auto)
- apply (simp add: inat_defs)
+apply (induct n, auto)
+ apply (simp add: zero_inat_def)
 apply (case_tac "x=UU",auto)
- apply (simp add: inat_defs)
+ apply (simp add: zero_inat_def)
 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
 apply (subgoal_tac "EX k. Fin k = #y",clarify)
  apply (erule_tac x="k" in allE)
  apply (erule_tac x="y" in allE,auto)
  apply (erule_tac x="THE p. Suc p = t" in allE,auto)
-   apply (simp add: inat_defs split:inat_splits)
-  apply (simp add: inat_defs split:inat_splits)
+   apply (simp add: iSuc_def split: inat.splits)
+  apply (simp add: iSuc_def split: inat.splits)
   apply (simp only: the_equality)
- apply (simp add: inat_defs split:inat_splits)
+ apply (simp add: iSuc_def split: inat.splits)
  apply force
-by (simp add: inat_defs split:inat_splits)
+apply (simp add: iSuc_def split: inat.splits)
+done
 
 lemma take_i_rt_len:
 "[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==>
@@ -721,13 +725,13 @@
 (* ----------------------------------------------------------------------- *)
 
 lemma UU_sconc [simp]: " UU ooo s = s "
-by (simp add: sconc_def inat_defs)
+by (simp add: sconc_def zero_inat_def)
 
 lemma scons_neq_UU: "a~=UU ==> a && s ~=UU"
 by auto
 
 lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
-apply (simp add: sconc_def inat_defs split:inat_splits,auto)
+apply (simp add: sconc_def zero_inat_def iSuc_def split: inat.splits, auto)
 apply (rule someI2_ex,auto)
  apply (rule_tac x="x && y" in exI,auto)
 apply (simp add: i_rt_Suc_forw)
@@ -740,12 +744,12 @@
  apply (rule stream_finite_ind [of x],auto)
   apply (simp add: stream.finite_def)
   apply (drule slen_take_lemma1,blast)
- apply (simp add: inat_defs split:inat_splits)+
+ apply (simp_all add: zero_inat_def iSuc_def split: inat.splits)
 apply (erule_tac x="y" in allE,auto)
 by (rule_tac x="a && w" in exI,auto)
 
 lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"
-apply (simp add: sconc_def inat_defs split:inat_splits, arith?,auto)
+apply (simp add: sconc_def split: inat.splits, arith?,auto)
 apply (rule someI2_ex,auto)
 by (drule ex_sconc,simp)
 
@@ -755,7 +759,7 @@
 
 lemma sconc_UU [simp]:"s ooo UU = s"
 apply (case_tac "#s")
- apply (simp add: sconc_def inat_defs)
+ apply (simp add: sconc_def)
  apply (rule someI2_ex)
   apply (rule_tac x="s" in exI)
   apply auto
@@ -763,25 +767,24 @@
   apply (simp add: i_rt_lemma_slen)
  apply (drule slen_take_lemma1,auto)
  apply (simp add: i_rt_slen)
-by (simp add: sconc_def inat_defs)
+by (simp add: sconc_def)
 
 lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x"
 apply (simp add: sconc_def)
-apply (simp add: inat_defs split:inat_splits,auto)
-apply (rule someI2_ex,auto)
+apply (cases "#x")
+apply auto
+apply (rule someI2_ex, auto)
 by (drule ex_sconc,simp)
 
 lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
-apply (case_tac "#x",auto)
- apply (simp add: sconc_def)
+apply (cases "#x",auto)
+ apply (simp add: sconc_def iSuc_Fin)
  apply (rule someI2_ex)
-  apply (drule ex_sconc,simp)
- apply (rule someI2_ex,auto)
+  apply (drule ex_sconc, simp)
+ apply (rule someI2_ex, auto)
   apply (simp add: i_rt_Suc_forw)
-  apply (rule_tac x="a && x" in exI,auto)
+  apply (rule_tac x="a && x" in exI, auto)
  apply (case_tac "xa=UU",auto)
-(*apply (drule_tac s="stream_take nat$x" in scons_neq_UU)
-  apply (simp add: i_rt_Suc_forw)*)
  apply (drule stream_exhaust_eq [THEN iffD1],auto)
  apply (drule streams_prefix_lemma1,simp+)
 by (simp add: sconc_def)
@@ -839,7 +842,7 @@
 apply (case_tac "x=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (erule_tac x="ya" in allE)
-by (simp add: inat_defs split:inat_splits)
+apply (case_tac "#ya") by simp_all
 
 
 
@@ -913,7 +916,9 @@
 
 lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k"
 apply (insert slen_mono [of "x" "x ooo y"])
-by (simp add: inat_defs split: inat_splits)
+apply (cases "#x") apply simp_all
+apply (cases "#(x ooo y)") apply simp_all
+done
 
 (* ----------------------------------------------------------------------- *)
    subsection "finite slen"
@@ -986,7 +991,7 @@
 (* ----------------------------------------------------------------------- *)
 
 lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s"
-by (simp add: constr_sconc_def inat_defs)
+by (simp add: constr_sconc_def zero_inat_def)
 
 lemma "x ooo y = constr_sconc x y"
 apply (case_tac "#x")
@@ -994,7 +999,7 @@
   defer 1
   apply (simp add: constr_sconc_def del: scons_sconc)
   apply (case_tac "#s")
-   apply (simp add: inat_defs)
+   apply (simp add: iSuc_Fin)
    apply (case_tac "a=UU",auto simp del: scons_sconc)
    apply (simp)
   apply (simp add: sconc_def)