src/HOL/IMP/Abs_Int2_ivl.thy
author nipkow
Wed, 06 Mar 2013 16:10:56 +0100
changeset 51359 00b45c7e831f
parent 51261 d301ba7da9b6
child 51389 8a9f0503b1c0
permissions -rw-r--r--
major redesign: order instead of preorder, new definition of intervals as quotients
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     2
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     7
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     8
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
     9
subsection "Interval Analysis"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    68
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    69
49396
73fb17ed2e08 converted wt into a set, tuned names
nipkow
parents: 49188
diff changeset
    70
instantiation ivl :: semilattice
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    71
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
    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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   103
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   104
instance
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   121
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   122
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   123
end
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   143
49396
73fb17ed2e08 converted wt into a set, tuned names
nipkow
parents: 49188
diff changeset
   144
instantiation ivl :: lattice
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   145
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   157
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   158
instance
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   159
proof
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   162
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   165
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   170
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   171
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   172
end
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   173
51245
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   193
begin
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   202
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   203
instance ..
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   204
end
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   219
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   220
instantiation ivl :: uminus
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   221
begin
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   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
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   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
d301ba7da9b6 improved orderings
nipkow
parents: 51245
diff changeset
   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
d301ba7da9b6 improved orderings
nipkow
parents: 51245
diff changeset
   233
d301ba7da9b6 improved orderings
nipkow
parents: 51245
diff changeset
   234
instance ..
d301ba7da9b6 improved orderings
nipkow
parents: 51245
diff changeset
   235
end
d301ba7da9b6 improved orderings
nipkow
parents: 51245
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   281
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   282
interpretation Val_abs
51245
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   283
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   290
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   295
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   296
51359
00b45c7e831f major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents: 51261
diff changeset
   297
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   298
interpretation Val_abs1_gamma
51245
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   299
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   300
defines aval_ivl is aval'
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   306
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   322
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   323
interpretation Val_abs1
51245
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   324
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   325
and test_num' = in_ivl
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   326
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   332
next
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   339
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   340
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   341
interpretation Abs_Int1
51245
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   342
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   343
and test_num' = in_ivl
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   344
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   345
defines afilter_ivl is afilter
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   346
and bfilter_ivl is bfilter
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   347
and step_ivl is step'
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   348
and AI_ivl is AI
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   349
and aval_ivl' is aval''
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   350
..
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   351
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   352
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   353
text{* Monotonicity: *}
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   366
interpretation Abs_Int1_mono
51245
311fe56541ea more abstract intervals
nipkow
parents: 51036
diff changeset
   367
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   368
and test_num' = in_ivl
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   369
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   380
qed
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   381
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   382
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   383
subsubsection "Tests"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   390
value "show_acom_opt (AI_ivl test1_ivl)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   391
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   392
text{* Better than @{text AI_const}: *}
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   393
value "show_acom_opt (AI_ivl test3_const)"
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   394
value "show_acom_opt (AI_ivl test4_const)"
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   395
value "show_acom_opt (AI_ivl test6_const)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   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
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   398
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   399
value "show_acom_opt (AI_ivl test2_ivl)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   400
value "show_acom (steps test2_ivl 0)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   401
value "show_acom (steps test2_ivl 1)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   402
value "show_acom (steps test2_ivl 2)"
49188
22f7e7b68f50 adjusted examples
nipkow
parents: 47613
diff changeset
   403
value "show_acom (steps test2_ivl 3)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   404
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   405
text{* Fixed point reached in 2 steps.
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   406
 Not so if the start value of x is known: *}
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   407
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   408
value "show_acom_opt (AI_ivl test3_ivl)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   409
value "show_acom (steps test3_ivl 0)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   410
value "show_acom (steps test3_ivl 1)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   411
value "show_acom (steps test3_ivl 2)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   412
value "show_acom (steps test3_ivl 3)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   413
value "show_acom (steps test3_ivl 4)"
49188
22f7e7b68f50 adjusted examples
nipkow
parents: 47613
diff changeset
   414
value "show_acom (steps test3_ivl 5)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   415
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   416
text{* Takes as many iterations as the actual execution. Would diverge if
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   417
loop did not terminate. Worse still, as the following example shows: even if
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   418
the actual execution terminates, the analysis may not. The value of y keeps
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   419
decreasing as the analysis is iterated, no matter how long: *}
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   420
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   421
value "show_acom (steps test4_ivl 50)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   422
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   423
text{* Relationships between variables are NOT captured: *}
51036
e7b54119c436 tuned top
nipkow
parents: 50995
diff changeset
   424
value "show_acom_opt (AI_ivl test5_ivl)"
47613
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   425
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   426
text{* Again, the analysis would not terminate: *}
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   427
value "show_acom (steps test6_ivl 50)"
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   428
e72e44cee6f2 added revised version of Abs_Int
nipkow
parents:
diff changeset
   429
end