pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
authorhuffman
Mon Dec 06 08:59:58 2010 -0800 (2010-12-06)
changeset 41029f7d8cfa6e7fc
parent 41028 0acff85f95c7
child 41030 ff7d177128ef
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/Tools/cpodef.ML
     1.1 --- a/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 08:43:52 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Mon Dec 06 08:59:58 2010 -0800
     1.3 @@ -250,20 +250,6 @@
     1.4   apply (simp add: type_definition.Rep_inject [OF type])
     1.5  done
     1.6  
     1.7 -theorem typedef_Abs_defined:
     1.8 -  assumes type: "type_definition Rep Abs A"
     1.9 -    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.10 -    and UU_in_A: "\<bottom> \<in> A"
    1.11 -  shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
    1.12 -by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
    1.13 -
    1.14 -theorem typedef_Rep_defined:
    1.15 -  assumes type: "type_definition Rep Abs A"
    1.16 -    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    1.17 -    and UU_in_A: "\<bottom> \<in> A"
    1.18 -  shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
    1.19 -by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
    1.20 -
    1.21  subsection {* Proving a subtype is flat *}
    1.22  
    1.23  theorem typedef_flat:
     2.1 --- a/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:43:52 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:59:58 2010 -0800
     2.3 @@ -36,10 +36,10 @@
     2.4  done
     2.5  
     2.6  lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>"
     2.7 -by (simp add: succeed_def cont_Abs_match Abs_match_defined)
     2.8 +by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff)
     2.9  
    2.10  lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
    2.11 -by (simp add: fail_def Abs_match_defined)
    2.12 +by (simp add: fail_def Abs_match_bottom_iff)
    2.13  
    2.14  lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)"
    2.15  by (simp add: succeed_def cont_Abs_match Abs_match_inject)
     3.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 08:43:52 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 08:59:58 2010 -0800
     3.3 @@ -11,8 +11,8 @@
     3.4      { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
     3.5        lub: thm, compact: thm }
     3.6    type pcpo_info =
     3.7 -    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
     3.8 -      Rep_defined: thm, Abs_defined: thm }
     3.9 +    { Rep_strict: thm, Abs_strict: thm,
    3.10 +      Rep_bottom_iff: thm, Abs_bottom_iff: thm }
    3.11  
    3.12    val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
    3.13      term -> (binding * binding) option -> tactic -> theory ->
    3.14 @@ -48,8 +48,8 @@
    3.15      lub: thm, compact: thm }
    3.16  
    3.17  type pcpo_info =
    3.18 -  { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
    3.19 -    Rep_defined: thm, Abs_defined: thm }
    3.20 +  { Rep_strict: thm, Abs_strict: thm,
    3.21 +    Rep_bottom_iff: thm, Abs_bottom_iff: thm }
    3.22  
    3.23  (* building terms *)
    3.24  
    3.25 @@ -136,8 +136,6 @@
    3.26      val Abs_strict = make @{thm typedef_Abs_strict}
    3.27      val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff}
    3.28      val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff}
    3.29 -    val Rep_defined = make @{thm typedef_Rep_defined}
    3.30 -    val Abs_defined = make @{thm typedef_Abs_defined}
    3.31      val (_, thy) =
    3.32        thy
    3.33        |> Sign.add_path (Binding.name_of name)
    3.34 @@ -145,14 +143,11 @@
    3.35          ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
    3.36            ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
    3.37            ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
    3.38 -          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
    3.39 -          ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
    3.40 -          ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
    3.41 +          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), [])])
    3.42        ||> Sign.parent_path
    3.43      val pcpo_info =
    3.44        { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
    3.45 -        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
    3.46 -        Rep_defined = Rep_defined, Abs_defined = Abs_defined }
    3.47 +        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff }
    3.48    in
    3.49      (pcpo_info, thy)
    3.50    end