domain package declares more simp rules
authorhuffman
Mon Mar 30 13:55:05 2009 -0700 (2009-03-30)
changeset 30807a167ed35ec0d
parent 30802 f9e9e800d27e
child 30808 a3d9cad81ae5
domain package declares more simp rules
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Mon Mar 30 12:07:59 2009 -0700
     1.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Mon Mar 30 13:55:05 2009 -0700
     1.3 @@ -87,9 +87,6 @@
     1.4  apply (cut_tac fscons_not_empty)
     1.5  apply (fast dest: eq_UU_iff [THEN iffD2])
     1.6  apply (simp add: fscons_def2)
     1.7 -apply (drule stream_flat_prefix)
     1.8 -apply (rule Def_not_UU)
     1.9 -apply (fast)
    1.10  done
    1.11  
    1.12  lemma fstream_prefix' [simp]:
     2.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Mon Mar 30 12:07:59 2009 -0700
     2.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Mon Mar 30 13:55:05 2009 -0700
     2.3 @@ -173,13 +173,12 @@
     2.4  lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt &  s << tt"
     2.5  apply (simp add: fsingleton_def2)
     2.6  apply (insert stream_prefix [of "Def a" s t], auto)
     2.7 -by (auto simp add: stream.inverts)
     2.8 +done
     2.9  
    2.10  lemma fstreams_prefix': "x << <a> ooo z = (x = <> |  (EX y. x = <a> ooo y &  y << z))"
    2.11  apply (auto, case_tac "x=UU", auto)
    2.12  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    2.13  apply (simp add: fsingleton_def2, auto)
    2.14 -apply (auto simp add: stream.inverts)
    2.15  apply (drule ax_flat, simp)
    2.16  by (erule sconc_mono)
    2.17  
    2.18 @@ -197,8 +196,7 @@
    2.19  by auto
    2.20  
    2.21  lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
    2.22 -apply (simp add: fsingleton_def2)
    2.23 -by (auto simp add: stream.inverts)
    2.24 +by (simp add: fsingleton_def2)
    2.25  
    2.26  lemma fsmap_UU[simp]: "fsmap f$UU = UU"
    2.27  by (simp add: fsmap_def)
    2.28 @@ -220,7 +218,6 @@
    2.29  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    2.30  apply (case_tac "y=UU", auto)
    2.31  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    2.32 -apply (auto simp add: stream.inverts)
    2.33  apply (simp add: flat_less_iff)
    2.34  apply (case_tac "s=UU", auto)
    2.35  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    2.36 @@ -344,7 +341,3 @@
    2.37  by (erule ch2ch_monofun, simp)
    2.38  
    2.39  end
    2.40 -
    2.41 -
    2.42 -
    2.43 -
     3.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Mar 30 12:07:59 2009 -0700
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Mar 30 13:55:05 2009 -0700
     3.3 @@ -322,7 +322,6 @@
     3.4  
     3.5  lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
     3.6  apply (simp add: Consq_def2)
     3.7 -apply (simp add: seq.inverts)
     3.8  done
     3.9  
    3.10  lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
    3.11 @@ -661,7 +660,7 @@
    3.12     (Forall (%x. ~P x) ys & Finite ys)"
    3.13  apply (rule_tac x="ys" in Seq_induct)
    3.14  (* adm *)
    3.15 -apply (simp add: seq.compacts Forall_def sforall_def)
    3.16 +apply (simp add: Forall_def sforall_def)
    3.17  (* base cases *)
    3.18  apply simp
    3.19  apply simp
     4.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Mar 30 12:07:59 2009 -0700
     4.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Mar 30 13:55:05 2009 -0700
     4.3 @@ -607,23 +607,23 @@
     4.4  in
     4.5    thy
     4.6      |> Sign.add_path (Long_Name.base_name dname)
     4.7 -    |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
     4.8 -        ("iso_rews" , iso_rews  ),
     4.9 -        ("exhaust"  , [exhaust] ),
    4.10 -        ("casedist" , [casedist]),
    4.11 -        ("when_rews", when_rews ),
    4.12 -        ("compacts", con_compacts),
    4.13 -        ("con_rews", con_rews),
    4.14 -        ("sel_rews", sel_rews),
    4.15 -        ("dis_rews", dis_rews),
    4.16 -        ("pat_rews", pat_rews),
    4.17 -        ("dist_les", dist_les),
    4.18 -        ("dist_eqs", dist_eqs),
    4.19 -        ("inverts" , inverts ),
    4.20 -        ("injects" , injects ),
    4.21 -        ("copy_rews", copy_rews)])))
    4.22 -    |> (snd o PureThy.add_thmss
    4.23 -        [((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])])
    4.24 +    |> (snd o PureThy.add_thmss [
    4.25 +        ((Binding.name "iso_rews" , iso_rews  ), [Simplifier.simp_add]),
    4.26 +        ((Binding.name "exhaust"  , [exhaust] ), []),
    4.27 +        ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]),
    4.28 +        ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
    4.29 +        ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
    4.30 +        ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
    4.31 +        ((Binding.name "sel_rews", sel_rews), [Simplifier.simp_add]),
    4.32 +        ((Binding.name "dis_rews", dis_rews), [Simplifier.simp_add]),
    4.33 +        ((Binding.name "pat_rews", pat_rews), [Simplifier.simp_add]),
    4.34 +        ((Binding.name "dist_les", dist_les), [Simplifier.simp_add]),
    4.35 +        ((Binding.name "dist_eqs", dist_eqs), [Simplifier.simp_add]),
    4.36 +        ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
    4.37 +        ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
    4.38 +        ((Binding.name "copy_rews", copy_rews), [Simplifier.simp_add]),
    4.39 +        ((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])
    4.40 +       ])
    4.41      |> Sign.parent_path
    4.42      |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    4.43          pat_rews @ dist_les @ dist_eqs @ copy_rews)
     5.1 --- a/src/HOLCF/ex/Stream.thy	Mon Mar 30 12:07:59 2009 -0700
     5.2 +++ b/src/HOLCF/ex/Stream.thy	Mon Mar 30 13:55:05 2009 -0700
     5.3 @@ -81,15 +81,13 @@
     5.4  
     5.5  lemma stream_prefix:
     5.6    "[| a && s << t; a ~= UU  |] ==> EX b tt. t = b && tt &  b ~= UU &  s << tt"
     5.7 -apply (insert stream.exhaust [of t], auto)
     5.8 -by (auto simp add: stream.inverts)
     5.9 +by (insert stream.exhaust [of t], auto)
    5.10  
    5.11  lemma stream_prefix':
    5.12    "b ~= UU ==> x << b && z =
    5.13     (x = UU |  (EX a y. x = a && y &  a ~= UU &  a << b &  y << z))"
    5.14  apply (case_tac "x=UU",auto)
    5.15 -apply (drule stream_exhaust_eq [THEN iffD1],auto)
    5.16 -by (auto simp add: stream.inverts)
    5.17 +by (drule stream_exhaust_eq [THEN iffD1],auto)
    5.18  
    5.19  
    5.20  (*
    5.21 @@ -100,7 +98,6 @@
    5.22  lemma stream_flat_prefix:
    5.23    "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
    5.24  apply (case_tac "y=UU",auto)
    5.25 -apply (auto simp add: stream.inverts)
    5.26  by (drule ax_flat,simp)
    5.27  
    5.28  
    5.29 @@ -280,17 +277,17 @@
    5.30  section "coinduction"
    5.31  
    5.32  lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R"
    5.33 -apply (simp add: stream.bisim_def,clarsimp)
    5.34 -apply (case_tac "x=UU",clarsimp)
    5.35 -apply (erule_tac x="UU" in allE,simp)
    5.36 -apply (case_tac "x'=UU",simp)
    5.37 -apply (drule stream_exhaust_eq [THEN iffD1],auto)+
    5.38 -apply (case_tac "x'=UU",auto)
    5.39 -apply (erule_tac x="a && y" in allE)
    5.40 -apply (erule_tac x="UU" in allE)+
    5.41 -apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
    5.42 -apply (erule_tac x="a && y" in allE)
    5.43 -apply (erule_tac x="aa && ya" in allE)
    5.44 + apply (simp add: stream.bisim_def,clarsimp)
    5.45 + apply (case_tac "x=UU",clarsimp)
    5.46 +  apply (erule_tac x="UU" in allE,simp)
    5.47 +  apply (case_tac "x'=UU",simp)
    5.48 +  apply (drule stream_exhaust_eq [THEN iffD1],auto)+
    5.49 + apply (case_tac "x'=UU",auto)
    5.50 +  apply (erule_tac x="a && y" in allE)
    5.51 +  apply (erule_tac x="UU" in allE)+
    5.52 +  apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
    5.53 + apply (erule_tac x="a && y" in allE)
    5.54 + apply (erule_tac x="aa && ya" in allE) back
    5.55  by auto
    5.56  
    5.57  
    5.58 @@ -327,7 +324,6 @@
    5.59  apply (erule stream_finite_ind [of s], auto)
    5.60  apply (case_tac "t=UU", auto)
    5.61  apply (drule stream_exhaust_eq [THEN iffD1],auto)
    5.62 -apply (auto simp add: stream.inverts)
    5.63  apply (erule_tac x="y" in allE, simp)
    5.64  by (rule stream_finite_lemma1, simp)
    5.65  
    5.66 @@ -374,8 +370,6 @@
    5.67  lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y &  a ~= \<bottom> &  Fin n < #y)"
    5.68  apply (auto, case_tac "x=UU",auto)
    5.69  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    5.70 -apply (rule_tac x="a" in exI)
    5.71 -apply (rule_tac x="y" in exI, simp)
    5.72  apply (case_tac "#y") apply simp_all
    5.73  apply (case_tac "#y") apply simp_all
    5.74  done
    5.75 @@ -387,15 +381,11 @@
    5.76  by (simp add: slen_def)
    5.77  
    5.78  lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
    5.79 -apply (rule stream.casedist [of x], auto)
    5.80 -apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
    5.81 -apply (simp add: zero_inat_def)
    5.82 -apply (subgoal_tac "s=y & aa=a", simp)
    5.83 -apply (simp_all add: not_less iSuc_Fin)
    5.84 -apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
    5.85 -apply (case_tac "aa=UU", auto)
    5.86 -apply (erule_tac x="a" in allE, simp)
    5.87 -apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
    5.88 + apply (rule stream.casedist [of x], auto)
    5.89 +    apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
    5.90 +   apply (simp add: zero_inat_def)
    5.91 +  apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
    5.92 + apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
    5.93  done
    5.94  
    5.95  lemma slen_take_lemma4 [rule_format]:
    5.96 @@ -463,8 +453,7 @@
    5.97  apply (erule stream_finite_ind [of s], auto)
    5.98  apply (case_tac "t=UU", auto)
    5.99  apply (drule stream_exhaust_eq [THEN iffD1], auto)
   5.100 -apply (erule_tac x="y" in allE, auto)
   5.101 -by (auto simp add: stream.inverts)
   5.102 +done
   5.103  
   5.104  lemma slen_mono: "s << t ==> #s <= #t"
   5.105  apply (case_tac "stream_finite t")
   5.106 @@ -493,7 +482,6 @@
   5.107  apply (case_tac "y=UU", clarsimp)
   5.108  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
   5.109  apply (erule_tac x="ya" in allE, simp)
   5.110 -apply (auto simp add: stream.inverts)
   5.111  by (drule ax_flat, simp)
   5.112  
   5.113  lemma slen_strict_mono_lemma:
   5.114 @@ -501,7 +489,6 @@
   5.115  apply (erule stream_finite_ind, auto)
   5.116  apply (case_tac "sa=UU", auto)
   5.117  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
   5.118 -apply (simp add: stream.inverts, clarsimp)
   5.119  by (drule ax_flat, simp)
   5.120  
   5.121  lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
   5.122 @@ -653,7 +640,7 @@
   5.123  apply (simp add: i_th_def i_rt_Suc_back)
   5.124  apply (rule stream.casedist [of "i_rt n s1"],simp)
   5.125  apply (rule stream.casedist [of "i_rt n s2"],auto)
   5.126 -by (intro monofun_cfun, auto)
   5.127 +done
   5.128  
   5.129  lemma i_th_stream_take_Suc [rule_format]:
   5.130   "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"