Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
authorballarin
Thu Aug 02 18:13:42 2007 +0200 (2007-08-02)
changeset 241311099f6c73649
parent 24130 5ab8044b6d46
child 24132 dc95373bd69f
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
src/HOL/Algebra/IntRing.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Aug 02 17:31:10 2007 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Thu Aug 02 18:13:42 2007 +0200
     1.3 @@ -195,16 +195,36 @@
     1.4    by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
     1.5  
     1.6  
     1.7 -interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
     1.8 -  where "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
     1.9 +text {* Removal of occurrences of @{term UNIV} in interpretation result
    1.10 +  --- experimental. *}
    1.11 +
    1.12 +lemma UNIV:
    1.13 +  "x \<in> UNIV = True"
    1.14 +  "A \<subseteq> UNIV = True"
    1.15 +  "(ALL x : UNIV. P x) = (ALL x. P x)"
    1.16 +  "(EX x : UNIV. P x) = (EX x. P x)"
    1.17 +  "(True --> Q) = Q"
    1.18 +  "(True ==> PROP R) == PROP R"
    1.19 +  by simp_all
    1.20 +
    1.21 +interpretation int [unfolded UNIV]:
    1.22 +  partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
    1.23 +  where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
    1.24 +    and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
    1.25 +    and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
    1.26  proof -
    1.27    show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
    1.28      by unfold_locales simp_all
    1.29 +  show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
    1.30 +    by simp
    1.31 +  show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
    1.32 +    by simp
    1.33    show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
    1.34      by (simp add: lless_def) auto
    1.35  qed
    1.36  
    1.37 -interpretation int: lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
    1.38 +interpretation int [unfolded UNIV]:
    1.39 +  lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
    1.40    where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
    1.41      and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
    1.42  proof -
    1.43 @@ -229,67 +249,10 @@
    1.44      done
    1.45  qed
    1.46  
    1.47 -interpretation int: total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
    1.48 +interpretation int [unfolded UNIV]:
    1.49 +  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
    1.50    by unfold_locales clarsimp
    1.51  
    1.52 -(*
    1.53 -lemma int_le_total_order:
    1.54 -  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
    1.55 -  apply (rule partial_order.total_orderI)
    1.56 -   apply (rule partial_order.intro, simp+)
    1.57 -  apply clarsimp
    1.58 -  done
    1.59 -
    1.60 -lemma less_int:
    1.61 -  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
    1.62 -  by (auto simp add: expand_fun_eq lless_def)
    1.63 -
    1.64 -lemma join_int:
    1.65 -  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
    1.66 -  apply (simp add: expand_fun_eq max_def)
    1.67 -  apply (rule+)
    1.68 -  apply (rule lattice.joinI)
    1.69 -  apply (simp add: int_le_total_order total_order.axioms)
    1.70 -  apply (simp add: least_def Upper_def)
    1.71 -  apply arith
    1.72 -  apply simp apply simp
    1.73 -  apply (rule lattice.joinI)
    1.74 -  apply (simp add: int_le_total_order total_order.axioms)
    1.75 -  apply (simp add: least_def Upper_def)
    1.76 -  apply arith
    1.77 -  apply simp apply simp
    1.78 -  done
    1.79 -
    1.80 -lemma meet_int:
    1.81 -  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
    1.82 -  apply (simp add: expand_fun_eq min_def)
    1.83 -  apply (rule+)
    1.84 -  apply (rule lattice.meetI)
    1.85 -  apply (simp add: int_le_total_order total_order.axioms)
    1.86 -  apply (simp add: greatest_def Lower_def)
    1.87 -  apply arith
    1.88 -  apply simp apply simp
    1.89 -  apply (rule lattice.meetI)
    1.90 -  apply (simp add: int_le_total_order total_order.axioms)
    1.91 -  apply (simp add: greatest_def Lower_def)
    1.92 -  apply arith
    1.93 -  apply simp apply simp
    1.94 -  done
    1.95 -
    1.96 -lemma carrier_int:
    1.97 -  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
    1.98 -  apply simp
    1.99 -  done
   1.100 -
   1.101 -text {* Interpretation unfolding @{text lless}, @{text join} and @{text
   1.102 -  meet} since they have natural representations in @{typ int}. *}
   1.103 -
   1.104 -interpretation 
   1.105 -  int [unfolded less_int join_int meet_int carrier_int]:
   1.106 -  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   1.107 -  by (rule int_le_total_order)
   1.108 -*)
   1.109 -
   1.110  
   1.111  subsubsection {* Generated Ideals of @{text "\<Z>"} *}
   1.112