# HG changeset patch
# User huffman
# Date 1238446505 25200
# Node ID a167ed35ec0d4fb296f0c50f7ea40d5f19261c1f
# Parent  f9e9e800d27e46c631263274cb60c34761013cb2
domain package declares more simp rules

diff -r f9e9e800d27e -r a167ed35ec0d src/HOLCF/FOCUS/Fstream.thy
--- 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]:
diff -r f9e9e800d27e -r a167ed35ec0d src/HOLCF/FOCUS/Fstreams.thy
--- 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
-
-
-
-
diff -r f9e9e800d27e -r a167ed35ec0d src/HOLCF/IOA/meta_theory/Sequence.thy
--- 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
diff -r f9e9e800d27e -r a167ed35ec0d src/HOLCF/Tools/domain/domain_theorems.ML
--- 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)
diff -r f9e9e800d27e -r a167ed35ec0d src/HOLCF/ex/Stream.thy
--- 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"