author  nipkow 
Fri, 03 May 2013 02:52:25 +0200  
changeset 51870  a331fbefcdb1 
parent 51826  054a40461449 
child 51871  f16bd7d2359c 
permissions  rwrr 
47613  1 
(* Author: Tobias Nipkow *) 
2 

3 
theory Abs_Int2_ivl 

51390  4 
imports Abs_Int2 
47613  5 
begin 
6 

7 
subsection "Interval Analysis" 

8 

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

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

10 
type_synonym eint2 = "eint * eint" 
51245  11 

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

12 
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

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

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

15 
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

16 
"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)" 
47613  17 

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

18 
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

19 
by(auto simp: eq_ivl_def) 
51245  20 

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

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

22 
by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def) 
47613  23 

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

24 
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

25 
by(simp add: eq_ivl_def) 
47613  26 

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

27 
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

28 
"[l\<dots>h] == abs_ivl(l,h)" 
47613  29 

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

30 
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

31 
by(auto simp: eq_ivl_def) 
51245  32 

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

33 
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

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

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

36 
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

37 
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

38 

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

39 
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

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

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

42 
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

43 
(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

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

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

46 
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

47 
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

48 
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

49 
done 
51245  50 

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

51 
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

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

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

54 
definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)" 
51245  55 

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

56 
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

57 
by simp 
51245  58 

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

59 
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

60 
by(auto simp add: is_empty_rep_def empty_rep_def) 
47613  61 

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

62 
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

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

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

65 
declare is_empty_rep_iff[THEN iffD1, simp] 
47613  66 

67 

51826  68 
instantiation ivl :: semilattice_sup_top 
47613  69 
begin 
70 

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

71 
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

72 
"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

73 
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

74 
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

75 

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

76 
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

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

78 
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

79 
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

80 
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

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

82 

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

83 
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

84 
by(auto simp: eq_ivl_def le_iff_subset) 
47613  85 

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

86 
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

87 

51389  88 
definition sup_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where 
89 
"sup_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 

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

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

51389  92 
lift_definition sup_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is sup_rep 
93 
by(auto simp: eq_ivl_iff sup_rep_def) 

47613  94 

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

95 
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

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

97 

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

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

99 
"\<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

100 
by(auto simp add: is_empty_rep_def max_def min_def split: if_splits) 
47613  101 

102 
instance 

103 
proof 

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

104 
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

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

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

108 
case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_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 goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits) 
47613  111 
next 
51389  112 
case goal5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max) 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

113 
next 
51389  114 
case goal6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max) 
47613  115 
next 
51389  116 
case goal7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def) 
47613  117 
next 
51389  118 
case goal8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def) 
47613  119 
qed 
120 

121 
end 

122 

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

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

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

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

126 

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

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

128 
"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

129 

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

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

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

132 
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

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

134 

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

135 
end 
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 
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

138 
by(simp add: not_less) 
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> Minf < x) = (x = Minf)" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

140 
by(simp add: not_less) 
47613  141 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

142 
instantiation ivl :: bounded_lattice 
47613  143 
begin 
144 

51389  145 
definition inf_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where 
146 
"inf_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))" 

47613  147 

51389  148 
lemma \<gamma>_inf_rep: "\<gamma>_rep(inf_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2" 
149 
by(auto simp:inf_rep_def \<gamma>_rep_cases split: prod.splits extended.splits) 

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

150 

51389  151 
lift_definition inf_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is inf_rep 
152 
by(auto simp: \<gamma>_inf_rep eq_ivl_def) 

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

153 

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

154 
definition "\<bottom> = empty_ivl" 
47613  155 

156 
instance 

157 
proof 

51389  158 
case goal1 thus ?case 
159 
unfolding inf_rep_def by transfer (auto simp: le_iff_subset \<gamma>_inf_rep) 

160 
next 

47613  161 
case goal2 thus ?case 
51389  162 
unfolding inf_rep_def by transfer (auto simp: le_iff_subset \<gamma>_inf_rep) 
47613  163 
next 
164 
case goal3 thus ?case 

51389  165 
unfolding inf_rep_def by transfer (auto simp: le_iff_subset \<gamma>_inf_rep) 
47613  166 
next 
51389  167 
case goal4 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset) 
47613  168 
qed 
169 

170 
end 

171 

51245  172 

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

173 
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

174 
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

175 

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

176 
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

177 
(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

178 
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

179 
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

180 

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

182 
(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

183 
if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])" 
51389  184 
unfolding bot_ivl_def by transfer (simp add: sup_rep_def eq_ivl_empty) 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

185 

51389  186 
lemma inf_ivl_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]" 
187 
by transfer (simp add: inf_rep_def) 

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

188 

51870  189 
lemma top_ivl_nice: "\<top> = [\<infinity>\<dots>\<infinity>]" 
190 
by (simp add: top_ivl_def) 

191 

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

192 

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

193 
instantiation ivl :: plus 
47613  194 
begin 
195 

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

196 
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

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

198 
(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

199 
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

200 

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

201 
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

202 
by(auto simp: plus_rep_def eq_ivl_iff) 
51245  203 

204 
instance .. 

205 
end 

206 

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

207 
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

208 
(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

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

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

211 
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

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

213 
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

214 
by(cases x) auto 
47613  215 

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

216 
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

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

218 
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

219 
by(cases x) auto 
51245  220 

221 
instantiation ivl :: uminus 

222 
begin 

223 

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

224 
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

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

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

227 
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

228 
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

229 
split: prod.split) 
51261  230 

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

231 
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

232 
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

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

235 
instance .. 

236 
end 

237 

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

238 
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

239 
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

240 

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

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

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

243 
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

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

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

246 

47613  247 

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

248 
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

249 
"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

250 

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

251 
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

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

253 
(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

254 
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

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

256 
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

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

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

259 
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

260 
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

261 
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

262 

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

263 
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

264 
(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

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

266 
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

267 
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

268 
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

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

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

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

272 
"\<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

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

274 

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

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

276 
"\<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

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

278 

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

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

280 
"\<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

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

283 
interpretation Val_abs 

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

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

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

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

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

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

294 
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

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

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

298 

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

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

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

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

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

309 
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

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

51389  312 
lemma non_empty_inf: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow> 
313 
\<not> is_empty_rep (inf_rep a1 (plus_rep a (uminus_rep a2)))" 

314 
by (auto simp add: \<gamma>_inf_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv) 

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

315 
(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

316 

51389  317 
lemma filter_plus: "\<lbrakk>eq_ivl (inf_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and> 
318 
eq_ivl (inf_rep a2 (plus_rep a (uminus_rep a1))) b2; 

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

319 
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

320 
\<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2" 
51389  321 
by (auto simp: eq_ivl_iff \<gamma>_inf_rep non_empty_inf add_ac) 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

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

324 
interpretation Val_abs1 

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

328 
proof 

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

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

331 
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

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

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

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

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

337 
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

338 
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

339 
done 
47613  340 
qed 
341 

342 
interpretation Abs_Int1 

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

346 
defines afilter_ivl is afilter 

347 
and bfilter_ivl is bfilter 

348 
and step_ivl is step' 

349 
and AI_ivl is AI 

350 
and aval_ivl' is aval'' 

351 
.. 

352 

353 

354 
text{* Monotonicity: *} 

355 

51389  356 
lemma mono_inf_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (inf_rep p1 q1) (inf_rep p2 q2)" 
357 
by(auto simp add: le_iff_subset \<gamma>_inf_rep) 

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

358 

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

359 
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

360 
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

361 
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

362 

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

363 
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

364 
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

365 
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

366 

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

371 
proof 

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

372 
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

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

374 
case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def 
51389  375 
by transfer (auto simp: mono_inf_rep mono_plus_rep mono_minus_rep) 
47613  376 
next 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset

377 
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

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

379 
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

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

383 

384 
subsubsection "Tests" 

385 

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

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

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

388 
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

389 
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

390 

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

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

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

396 
value "show_acom_opt (AI_ivl test6_const)" 

47613  397 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

398 
definition "steps c i = (step_ivl \<top> ^^ i) (bot c)" 
47613  399 

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

403 
value "show_acom (steps test2_ivl 2)" 

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

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

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

412 
value "show_acom (steps test3_ivl 2)" 

413 
value "show_acom (steps test3_ivl 3)" 

414 
value "show_acom (steps test3_ivl 4)" 

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

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

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

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

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

421 

422 
value "show_acom (steps test4_ivl 50)" 

423 

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

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

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

428 
value "show_acom (steps test6_ivl 50)" 

429 

430 
end 