author  nipkow 
Wed, 06 Mar 2013 16:10:56 +0100  
changeset 51359  00b45c7e831f 
parent 51261  d301ba7da9b6 
child 51389  8a9f0503b1c0 
permissions  rwrr 
47613  1 
(* Author: Tobias Nipkow *) 
2 

3 
theory Abs_Int2_ivl 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

4 
imports "~~/src/HOL/Library/Quotient_List" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

5 
"~~/src/HOL/Library/Extended" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

6 
Abs_Int2 
47613  7 
begin 
8 

9 
subsection "Interval Analysis" 

10 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

11 
type_synonym eint = "int extended" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

12 
type_synonym eint2 = "eint * eint" 
51245  13 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

14 
definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

15 
"\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})" 
47613  16 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

17 
definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

18 
"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)" 
47613  19 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

20 
lemma refl_eq_ivl[simp]: "eq_ivl p p" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

21 
by(auto simp: eq_ivl_def) 
51245  22 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

23 
quotient_type ivl = eint2 / eq_ivl 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

24 
by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def) 
47613  25 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

26 
lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

27 
by(simp add: eq_ivl_def) 
47613  28 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

29 
abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

30 
"[l\<dots>h] == abs_ivl(l,h)" 
47613  31 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

32 
lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

33 
by(auto simp: eq_ivl_def) 
51245  34 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

35 
fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

36 
"in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h" 
47613  37 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

38 
lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

39 
by(auto simp: eq_ivl_def \<gamma>_rep_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

40 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

41 
definition is_empty_rep :: "eint2 \<Rightarrow> bool" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

42 
"is_empty_rep p = (let (l,h) = p in l>h  l=Pinf & h=Pinf  l=Minf & h=Minf)" 
47613  43 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

44 
lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j}  (Fin i,Pinf) => {i..}  
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

45 
(Minf,Fin i) \<Rightarrow> {..i}  (Minf,Pinf) \<Rightarrow> UNIV  _ \<Rightarrow> {})" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

46 
by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits) 
51245  47 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

48 
lift_definition is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

49 
apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

50 
apply(auto simp: not_less less_eq_extended_cases split: extended.splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

51 
done 
51245  52 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

53 
lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2  p1 = p2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

54 
by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits) 
51245  55 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

56 
definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)" 
51245  57 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

58 
lift_definition empty_ivl :: ivl is empty_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

59 
by simp 
51245  60 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

61 
lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

62 
by(auto simp add: is_empty_rep_def empty_rep_def) 
47613  63 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

64 
lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

65 
by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits) 
47613  66 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

67 
declare is_empty_rep_iff[THEN iffD1, simp] 
47613  68 

69 

49396  70 
instantiation ivl :: semilattice 
47613  71 
begin 
72 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

73 
definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

74 
"le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

75 
if is_empty_rep(l1,h1) then True else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

76 
if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

77 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

78 
lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

79 
apply rule 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

80 
apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1] 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

81 
apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

82 
apply(auto simp: not_less split: extended.splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

83 
done 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

84 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

85 
lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

86 
by(auto simp: eq_ivl_def le_iff_subset) 
47613  87 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

88 
definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

89 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

90 
definition join_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

91 
"join_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

92 
else let (l1,h1) = p1; (l2,h2) = p2 in (min l1 l2, max h1 h2))" 
47613  93 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

94 
lift_definition join_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is join_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

95 
by(auto simp: eq_ivl_iff join_rep_def) 
47613  96 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

97 
lift_definition top_ivl :: ivl is "(Minf,Pinf)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

98 
by(auto simp: eq_ivl_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

99 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

100 
lemma is_empty_min_max: 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

101 
"\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

102 
by(auto simp add: is_empty_rep_def max_def min_def split: if_splits) 
47613  103 

104 
instance 

105 
proof 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

106 
case goal1 show ?case by (rule less_ivl_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

107 
next 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

108 
case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits) 
47613  109 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

110 
case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits) 
47613  111 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

112 
case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits) 
47613  113 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

114 
case goal6 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

115 
next 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

116 
case goal7 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max) 
47613  117 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

118 
case goal8 thus ?case by transfer (auto simp add: le_rep_def join_rep_def) 
47613  119 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

120 
case goal5 show ?case by transfer (simp add: le_rep_def is_empty_rep_def) 
47613  121 
qed 
122 

123 
end 

124 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

125 
text{* Implement (naive) executable equality: *} 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

126 
instantiation ivl :: equal 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

127 
begin 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

128 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

129 
definition equal_ivl where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

130 
"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

131 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

132 
instance 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

133 
proof 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

134 
case goal1 show ?case by(simp add: equal_ivl_def eq_iff) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

135 
qed 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

136 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

137 
end 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

138 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

139 
lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

140 
by(simp add: not_less) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

141 
lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

142 
by(simp add: not_less) 
47613  143 

49396  144 
instantiation ivl :: lattice 
47613  145 
begin 
146 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

147 
definition meet_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

148 
"meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))" 
47613  149 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

150 
lemma \<gamma>_meet_rep: "\<gamma>_rep(meet_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

151 
by(auto simp:meet_rep_def \<gamma>_rep_cases split: prod.splits extended.splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

152 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

153 
lift_definition meet_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is meet_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

154 
by(auto simp: \<gamma>_meet_rep eq_ivl_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

155 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

156 
definition "\<bottom> = empty_ivl" 
47613  157 

158 
instance 

159 
proof 

160 
case goal2 thus ?case 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

161 
unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep) 
47613  162 
next 
163 
case goal3 thus ?case 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

164 
unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep) 
47613  165 
next 
166 
case goal4 thus ?case 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

167 
unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep) 
47613  168 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

169 
case goal1 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset) 
47613  170 
qed 
171 

172 
end 

173 

51245  174 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

175 
lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

176 
by (metis eq_ivl_iff is_empty_empty_rep) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

177 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

178 
lemma le_ivl_nice: "[l1\<dots>h1] \<le> [l2\<dots>h2] \<longleftrightarrow> 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

179 
(if [l1\<dots>h1] = \<bottom> then True else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

180 
if [l2\<dots>h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

181 
unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

182 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

183 
lemma join_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] = 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

184 
(if [l1\<dots>h1] = \<bottom> then [l2\<dots>h2] else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

185 
if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

186 
unfolding bot_ivl_def by transfer (simp add: join_rep_def eq_ivl_empty) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

187 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

188 
lemma meet_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

189 
by transfer (simp add: meet_rep_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

190 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

191 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

192 
instantiation ivl :: plus 
47613  193 
begin 
194 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

195 
definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

196 
"plus_rep p1 p2 = 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

197 
(if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

198 
let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

199 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

200 
lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

201 
by(auto simp: plus_rep_def eq_ivl_iff) 
51245  202 

203 
instance .. 

204 
end 

205 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

206 
lemma plus_ivl_nice: "[l1\<dots>h1] + [l2\<dots>h2] = 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

207 
(if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then \<bottom> else [l1+l2 \<dots> h1+h2])" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

208 
unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty) 
51245  209 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

210 
lemma uminus_eq_Minf[simp]: "x = Minf \<longleftrightarrow> x = Pinf" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

211 
by(cases x) auto 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

212 
lemma uminus_eq_Pinf[simp]: "x = Pinf \<longleftrightarrow> x = Minf" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

213 
by(cases x) auto 
47613  214 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

215 
lemma uminus_le_Fin_iff: " x \<le> Fin(y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

216 
by(cases x) auto 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

217 
lemma Fin_uminus_le_iff: "Fin(y) \<le> x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

218 
by(cases x) auto 
51245  219 

220 
instantiation ivl :: uminus 

221 
begin 

222 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

223 
definition uminus_rep :: "eint2 \<Rightarrow> eint2" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

224 
"uminus_rep p = (let (l,h) = p in (h, l))" 
51245  225 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

226 
lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> i \<in> \<gamma>_rep(uminus_rep p)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

227 
by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

228 
split: prod.split) 
51261  229 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

230 
lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

231 
by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

232 
(auto simp: Icc_eq_Icc split: extended.splits) 
51261  233 

234 
instance .. 

235 
end 

236 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

237 
lemma uminus_nice: "[l\<dots>h] = [h\<dots>l]" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

238 
by transfer (simp add: uminus_rep_def) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

239 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

240 
instantiation ivl :: minus 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

241 
begin 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

242 
definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where "(iv1::ivl)  iv2 = iv1 + iv2" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

243 
instance .. 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

244 
end 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

245 

47613  246 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

247 
definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

248 
"filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv  iv2), iv2 \<sqinter> (iv  iv1))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

249 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

250 
definition filter_less_rep :: "bool \<Rightarrow> eint2 \<Rightarrow> eint2 \<Rightarrow> eint2 * eint2" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

251 
"filter_less_rep res p1 p2 = 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

252 
(if is_empty_rep p1 \<or> is_empty_rep p2 then (empty_rep,empty_rep) else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

253 
let (l1,h1) = p1; (l2,h2) = p2 in 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

254 
if res 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

255 
then ((l1, min h1 (h2 + Fin 1)), (max (l1 + Fin 1) l2, h2)) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

256 
else ((max l1 l2, h1), (l2, min h1 h2)))" 
47613  257 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

258 
lift_definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" is filter_less_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

259 
by(auto simp: prod_pred_def filter_less_rep_def eq_ivl_iff) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

260 
declare filter_less_ivl.abs_eq[code] (* bug in lifting *) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

261 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

262 
lemma filter_less_ivl_nice: "filter_less_ivl b [l1\<dots>h1] [l2\<dots>h2] = 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

263 
(if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then (\<bottom>,\<bottom>) else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

264 
if b 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

265 
then ([l1 \<dots> min h1 (h2 + Fin 1)], [max (l1 + Fin 1) l2 \<dots> h2]) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

266 
else ([max l1 l2 \<dots> h1], [l2 \<dots> min h1 h2]))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

267 
unfolding prod_rel_eq[symmetric] bot_ivl_def 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

268 
by transfer (auto simp: filter_less_rep_def eq_ivl_empty) 
47613  269 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

270 
lemma add_mono_le_Fin: 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

271 
"\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

272 
by(drule (1) add_mono) simp 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

273 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

274 
lemma add_mono_Fin_le: 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

275 
"\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

276 
by(drule (1) add_mono) simp 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

277 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

278 
lemma plus_rep_plus: 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

279 
"\<lbrakk> i1 \<in> \<gamma>_rep (l1,h1); i2 \<in> \<gamma>_rep (l2, h2)\<rbrakk> \<Longrightarrow> i1 + i2 \<in> \<gamma>_rep (l1 + l2, h1 + h2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

280 
by(simp add: \<gamma>_rep_def add_mono_Fin_le add_mono_le_Fin) 
47613  281 

282 
interpretation Val_abs 

51245  283 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" 
47613  284 
proof 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

285 
case goal1 thus ?case by transfer (simp add: le_iff_subset) 
47613  286 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

287 
case goal2 show ?case by transfer (simp add: \<gamma>_rep_def) 
47613  288 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

289 
case goal3 show ?case by transfer (simp add: \<gamma>_rep_def) 
47613  290 
next 
291 
case goal4 thus ?case 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

292 
apply transfer 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

293 
apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

294 
by(auto simp: empty_rep_def is_empty_rep_def) 
47613  295 
qed 
296 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

297 

47613  298 
interpretation Val_abs1_gamma 
51245  299 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" 
47613  300 
defines aval_ivl is aval' 
301 
proof 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

302 
case goal1 show ?case 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

303 
by transfer (auto simp add:meet_rep_def \<gamma>_rep_cases split: prod.split extended.split) 
47613  304 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

305 
case goal2 show ?case unfolding bot_ivl_def by transfer simp 
47613  306 
qed 
307 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

308 
lemma \<gamma>_plus_rep: "i1 : \<gamma>_rep p1 \<Longrightarrow> i2 : \<gamma>_rep p2 \<Longrightarrow> i1+i2 \<in> \<gamma>_rep(plus_rep p1 p2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

309 
by(auto simp: plus_rep_def plus_rep_plus split: prod.splits) 
47613  310 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

311 
lemma non_empty_meet: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow> 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

312 
\<not> is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

313 
by (auto simp add: \<gamma>_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

314 
(metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_minus) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

315 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

316 
lemma filter_plus: "\<lbrakk>eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and> 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

317 
eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2; 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

318 
n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a\<rbrakk> 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

319 
\<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

320 
by (auto simp: eq_ivl_iff \<gamma>_meet_rep non_empty_meet add_ac) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

321 
(metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_def add_commute)+ 
47613  322 

323 
interpretation Val_abs1 

51245  324 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" 
47613  325 
and test_num' = in_ivl 
326 
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl 

327 
proof 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

328 
case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def) 
47613  329 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

330 
case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def prod_rel_eq[symmetric] 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

331 
by transfer (simp add: filter_plus) 
47613  332 
next 
333 
case goal3 thus ?case 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

334 
unfolding prod_rel_eq[symmetric] 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

335 
apply transfer 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

336 
apply (auto simp add: filter_less_rep_def eq_ivl_iff max_def min_def split: if_splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

337 
apply(auto simp: \<gamma>_rep_cases is_empty_rep_def split: extended.splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

338 
done 
47613  339 
qed 
340 

341 
interpretation Abs_Int1 

51245  342 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" 
47613  343 
and test_num' = in_ivl 
344 
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl 

345 
defines afilter_ivl is afilter 

346 
and bfilter_ivl is bfilter 

347 
and step_ivl is step' 

348 
and AI_ivl is AI 

349 
and aval_ivl' is aval'' 

350 
.. 

351 

352 

353 
text{* Monotonicity: *} 

354 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

355 
lemma mono_meet_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (meet_rep p1 q1) (meet_rep p2 q2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

356 
by(auto simp add: le_iff_subset \<gamma>_meet_rep) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

357 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

358 
lemma mono_plus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (plus_rep p1 q1) (plus_rep p2 q2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

359 
apply(auto simp: plus_rep_def le_iff_subset split: if_splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

360 
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

361 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

362 
lemma mono_minus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep (uminus_rep p1) (uminus_rep p2)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

363 
apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

364 
by(auto simp: \<gamma>_rep_cases split: extended.splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

365 

47613  366 
interpretation Abs_Int1_mono 
51245  367 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" 
47613  368 
and test_num' = in_ivl 
369 
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl 

370 
proof 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

371 
case goal1 thus ?case by transfer (rule mono_plus_rep) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

372 
next 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

373 
case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

374 
by transfer (auto simp: mono_meet_rep mono_plus_rep mono_minus_rep) 
47613  375 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

376 
case goal3 thus ?case unfolding less_eq_prod_def 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

377 
apply transfer 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

378 
apply(auto simp:filter_less_rep_def le_iff_subset min_def max_def split: if_splits) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

379 
by(auto simp:is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) 
47613  380 
qed 
381 

382 

383 
subsubsection "Tests" 

384 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

385 
(* Hide Fin in numerals on output *) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

386 
declare 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

387 
Fin_numeral [code_post] Fin_neg_numeral [code_post] 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

388 
zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post] 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

389 

51036  390 
value "show_acom_opt (AI_ivl test1_ivl)" 
47613  391 

392 
text{* Better than @{text AI_const}: *} 

51036  393 
value "show_acom_opt (AI_ivl test3_const)" 
394 
value "show_acom_opt (AI_ivl test4_const)" 

395 
value "show_acom_opt (AI_ivl test6_const)" 

47613  396 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

397 
definition "steps c i = (step_ivl(Top(vars c)) ^^ i) (bot c)" 
47613  398 

51036  399 
value "show_acom_opt (AI_ivl test2_ivl)" 
47613  400 
value "show_acom (steps test2_ivl 0)" 
401 
value "show_acom (steps test2_ivl 1)" 

402 
value "show_acom (steps test2_ivl 2)" 

49188  403 
value "show_acom (steps test2_ivl 3)" 
47613  404 

51036  405 
text{* Fixed point reached in 2 steps. 
47613  406 
Not so if the start value of x is known: *} 
407 

51036  408 
value "show_acom_opt (AI_ivl test3_ivl)" 
47613  409 
value "show_acom (steps test3_ivl 0)" 
410 
value "show_acom (steps test3_ivl 1)" 

411 
value "show_acom (steps test3_ivl 2)" 

412 
value "show_acom (steps test3_ivl 3)" 

413 
value "show_acom (steps test3_ivl 4)" 

49188  414 
value "show_acom (steps test3_ivl 5)" 
47613  415 

416 
text{* Takes as many iterations as the actual execution. Would diverge if 

417 
loop did not terminate. Worse still, as the following example shows: even if 

418 
the actual execution terminates, the analysis may not. The value of y keeps 

419 
decreasing as the analysis is iterated, no matter how long: *} 

420 

421 
value "show_acom (steps test4_ivl 50)" 

422 

423 
text{* Relationships between variables are NOT captured: *} 

51036  424 
value "show_acom_opt (AI_ivl test5_ivl)" 
47613  425 

426 
text{* Again, the analysis would not terminate: *} 

427 
value "show_acom (steps test6_ivl 50)" 

428 

429 
end 