# HG changeset patch
# User nipkow
# Date 1348622200 -7200
# Node ID 1c73b107d20d0c436bf60b9e8cade8177d745eea
# Parent  10f9f8608b4d5743f8e18535c709270c4deb7a56
tuned

diff -r 10f9f8608b4d -r 1c73b107d20d src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Sep 26 03:03:11 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Sep 26 03:16:40 2012 +0200
@@ -6,30 +6,30 @@
 
 subsection "Interval Analysis"
 
-datatype ivl = I "int option" "int option"
+datatype ivl = Ivl "int option" "int option"
 
 definition "\<gamma>_ivl i = (case i of
-  I (Some l) (Some h) \<Rightarrow> {l..h} |
-  I (Some l) None \<Rightarrow> {l..} |
-  I None (Some h) \<Rightarrow> {..h} |
-  I None None \<Rightarrow> UNIV)"
+  Ivl (Some l) (Some h) \<Rightarrow> {l..h} |
+  Ivl (Some l) None \<Rightarrow> {l..} |
+  Ivl None (Some h) \<Rightarrow> {..h} |
+  Ivl None None \<Rightarrow> UNIV)"
 
-abbreviation I_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
-"{lo\<dots>hi} == I (Some lo) (Some hi)"
-abbreviation I_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
-"{lo\<dots>} == I (Some lo) None"
-abbreviation I_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
-"{\<dots>hi} == I None (Some hi)"
-abbreviation I_None_None :: "ivl"  ("{\<dots>}") where
-"{\<dots>} == I None None"
+abbreviation Ivl_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
+"{lo\<dots>hi} == Ivl (Some lo) (Some hi)"
+abbreviation Ivl_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
+"{lo\<dots>} == Ivl (Some lo) None"
+abbreviation Ivl_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
+"{\<dots>hi} == Ivl None (Some hi)"
+abbreviation Ivl_None_None :: "ivl"  ("{\<dots>}") where
+"{\<dots>} == Ivl None None"
 
 definition "num_ivl n = {n\<dots>n}"
 
 fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
-"in_ivl k (I (Some l) (Some h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
-"in_ivl k (I (Some l) None) \<longleftrightarrow> l \<le> k" |
-"in_ivl k (I None (Some h)) \<longleftrightarrow> k \<le> h" |
-"in_ivl k (I None None) \<longleftrightarrow> True"
+"in_ivl k (Ivl (Some l) (Some h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
+"in_ivl k (Ivl (Some l) None) \<longleftrightarrow> l \<le> k" |
+"in_ivl k (Ivl None (Some h)) \<longleftrightarrow> k \<le> h" |
+"in_ivl k (Ivl None None) \<longleftrightarrow> True"
 
 instantiation option :: (plus)plus
 begin
@@ -48,7 +48,7 @@
 "is_empty {l\<dots>h} = (h<l)" |
 "is_empty _ = False"
 
-lemma [simp]: "is_empty(I l h) =
+lemma [simp]: "is_empty(Ivl l h) =
   (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
 by(auto split:option.split)
 
@@ -56,7 +56,7 @@
 by(auto simp add: \<gamma>_ivl_def split: ivl.split option.split)
 
 definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
-  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
+  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))"
 
 instantiation ivl :: semilattice
 begin
@@ -67,7 +67,7 @@
   | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
 
 fun le_aux where
-"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
+"le_aux (Ivl l1 h1) (Ivl l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
 
 definition le_ivl where
 "i1 \<sqsubseteq> i2 =
@@ -82,8 +82,8 @@
 
 definition "i1 \<squnion> i2 =
  (if is_empty i1 then i2 else if is_empty i2 then i1
-  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
-          I (min_option False l1 l2) (max_option True h1 h2))"
+  else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
+          Ivl (min_option False l1 l2) (max_option True h1 h2))"
 
 definition "\<top> = {\<dots>}"
 
@@ -115,8 +115,8 @@
 begin
 
 definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
-  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
-    I (max_option False l1 l2) (min_option True h1 h2))"
+  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
+    Ivl (max_option False l1 l2) (min_option True h1 h2))"
 
 definition "\<bottom> = empty"
 
@@ -148,7 +148,7 @@
 end
 
 definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
-  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
+  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1-h2) (h1-l2))"
 
 lemma gamma_minus_ivl:
   "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
@@ -158,12 +158,12 @@
   i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
 
 fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
-"filter_less_ivl res (I l1 h1) (I l2 h2) =
-  (if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else
+"filter_less_ivl res (Ivl l1 h1) (Ivl l2 h2) =
+  (if is_empty(Ivl l1 h1) \<or> is_empty(Ivl l2 h2) then (empty, empty) else
    if res
-   then (I l1 (min_option True h1 (h2 - Some 1)),
-         I (max_option False (l1 + Some 1) l2) h2)
-   else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
+   then (Ivl l1 (min_option True h1 (h2 - Some 1)),
+         Ivl (max_option False (l1 + Some 1) l2) h2)
+   else (Ivl (max_option False l1 l2) h1, Ivl l2 (min_option True h1 h2)))"
 
 interpretation Val_abs
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
diff -r 10f9f8608b4d -r 1c73b107d20d src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Wed Sep 26 03:03:11 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Wed Sep 26 03:16:40 2012 +0200
@@ -86,15 +86,15 @@
 definition "widen_ivl ivl1 ivl2 =
   ((*if is_empty ivl1 then ivl2 else
    if is_empty ivl2 then ivl1 else*)
-     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
-       I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
-         (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
+     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
+       Ivl (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
+           (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
 
 definition "narrow_ivl ivl1 ivl2 =
   ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
-     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
-       I (if l1 = None then l2 else l1)
-         (if h1 = None then h2 else h1))"
+     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
+       Ivl (if l1 = None then l2 else l1)
+           (if h1 = None then h2 else h1))"
 
 instance
 proof qed
@@ -583,7 +583,7 @@
 subsubsection "Termination: Intervals"
 
 definition m_ivl :: "ivl \<Rightarrow> nat" where
-"m_ivl ivl = (case ivl of I l h \<Rightarrow>
+"m_ivl ivl = (case ivl of Ivl l h \<Rightarrow>
      (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))"
 
 lemma m_ivl_height: "m_ivl ivl \<le> 2"