remove unneeded lemmas Lift_exhaust, Lift_cases
authorhuffman
Tue Oct 12 09:32:21 2010 -0700 (2010-10-12)
changeset 40009f2c78550c0b7
parent 40008 58ead6f77f8e
child 40010 d7fdd84b959f
remove unneeded lemmas Lift_exhaust, Lift_cases
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/Lift.thy
     1.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Tue Oct 12 09:08:27 2010 -0700
     1.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Oct 12 09:32:21 2010 -0700
     1.3 @@ -95,7 +95,7 @@
     1.4  apply (safe)
     1.5  apply (erule_tac [!] contrapos_np)
     1.6  prefer 2 apply (fast elim: DefE)
     1.7 -apply (rule Lift_cases)
     1.8 +apply (rule lift.exhaust)
     1.9  apply (erule (1) notE)
    1.10  apply (safe)
    1.11  apply (drule Def_inject_less_eq [THEN iffD1])
     2.1 --- a/src/HOLCF/Lift.thy	Tue Oct 12 09:08:27 2010 -0700
     2.2 +++ b/src/HOLCF/Lift.thy	Tue Oct 12 09:32:21 2010 -0700
     2.3 @@ -43,12 +43,6 @@
     2.4  
     2.5  text {* @{term UU} and @{term Def} *}
     2.6  
     2.7 -lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)"
     2.8 -  by (induct x) simp_all
     2.9 -
    2.10 -lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    2.11 -  by (insert Lift_exhaust) blast
    2.12 -
    2.13  lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
    2.14    by (cases x) simp_all
    2.15