# HG changeset patch
# User nipkow
# Date 1348551462 -7200
# Node ID 6abbede3ae128e13afddc8638be3d390401a98cc
# Parent  47e4178f9a94bc3d3d8acc42fbc0c06e765293f6
tuned

diff -r 47e4178f9a94 -r 6abbede3ae12 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Mon Sep 24 19:11:35 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Tue Sep 25 07:37:42 2012 +0200
@@ -277,7 +277,7 @@
 
 definition pfp_wn :: "('a::{preord,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
 where "pfp_wn f x =
-  (case iter_widen f x of None \<Rightarrow> None | Some y \<Rightarrow> iter_narrow f y)"
+  (case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
 
 
 lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<sqsubseteq> p"
@@ -306,24 +306,24 @@
 
 lemma iter_narrow_pfp:
 assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
-and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)" and "P x0"
-and "f x0 \<sqsubseteq> x0" and "iter_narrow f x0 = Some x"
-shows "P x \<and> f x \<sqsubseteq> x"
+and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
+and "P p0" and "f p0 \<sqsubseteq> p0" and "iter_narrow f p0 = Some p"
+shows "P p \<and> f p \<sqsubseteq> p"
 proof-
-  let ?Q = "%x. P x \<and> f x \<sqsubseteq> x \<and> x \<sqsubseteq> x0"
-  { fix x assume "?Q x"
+  let ?Q = "%p. P p \<and> f p \<sqsubseteq> p \<and> p \<sqsubseteq> p0"
+  { fix p assume "?Q p"
     note P = conjunct1[OF this] and 12 = conjunct2[OF this]
     note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
-    let ?x' = "x \<triangle> f x"
-    have "?Q ?x'"
+    let ?p' = "p \<triangle> f p"
+    have "?Q ?p'"
     proof auto
-      show "P ?x'" by (blast intro: P Pinv)
-      have "f ?x' \<sqsubseteq> f x" by(rule mono[OF `P (x \<triangle> f x)`  P narrow2[OF 1]])
-      also have "\<dots> \<sqsubseteq> ?x'" by(rule narrow1[OF 1])
-      finally show "f ?x' \<sqsubseteq> ?x'" .
-      have "?x' \<sqsubseteq> x" by (rule narrow2[OF 1])
-      also have "x \<sqsubseteq> x0" by(rule 2)
-      finally show "?x' \<sqsubseteq> x0" .
+      show "P ?p'" by (blast intro: P Pinv)
+      have "f ?p' \<sqsubseteq> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
+      also have "\<dots> \<sqsubseteq> ?p'" by(rule narrow1[OF 1])
+      finally show "f ?p' \<sqsubseteq> ?p'" .
+      have "?p' \<sqsubseteq> p" by (rule narrow2[OF 1])
+      also have "p \<sqsubseteq> p0" by(rule 2)
+      finally show "?p' \<sqsubseteq> p0" .
     qed
   }
   thus ?thesis
@@ -332,16 +332,16 @@
 qed
 
 lemma pfp_wn_pfp:
-assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow>  P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
+assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
 and Pinv: "P x"  "!!x. P x \<Longrightarrow> P(f x)"
   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
-and pfp_wn: "pfp_wn f x = Some x'" shows "P x' \<and> f x' \<sqsubseteq> x'"
+and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<sqsubseteq> p"
 proof-
-  from pfp_wn obtain p
-    where its: "iter_widen f x = Some p" "iter_narrow f p = Some x'"
+  from pfp_wn obtain p0
+    where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
     by(auto simp: pfp_wn_def split: option.splits)
-  have "P p" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
+  have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
   thus ?thesis
     by - (assumption |
           rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+
@@ -433,7 +433,7 @@
 fixes n :: "'av \<Rightarrow> nat"
 assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
 assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
-assumes n_narrow: "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
+assumes n_narrow: "y \<sqsubseteq> x \<Longrightarrow> ~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
 
 begin
 
@@ -473,9 +473,10 @@
 done
 
 
-definition "n_s S = (\<Sum>x\<in>dom S. n(fun S x))"
+definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where
+"n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))"
 
-lemma n_s_mono: assumes "S1 \<sqsubseteq> S2" shows "n_s S1 \<le> n_s S2"
+lemma n_s_mono: assumes "S1 \<sqsubseteq> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
 proof-
   from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
     by(simp_all add: le_st_def)
@@ -486,14 +487,14 @@
 
 lemma n_s_narrow:
 assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
-shows "n_s (S1 \<triangle> S2) < n_s S1"
+shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1"
 proof-
   from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
     by(simp_all add: le_st_def)
   have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
     by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
   have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<sqsubseteq> S1 \<triangle> S2`
-    by(auto simp: le_st_def narrow_st_def intro: n_narrow)
+    by(force simp: le_st_def narrow_st_def intro: n_narrow)
   have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
     apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
   moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
@@ -501,22 +502,25 @@
 qed
 
 
-definition "n_o opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n_s x + 1)"
+definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
+"n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
 
-lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n_o S1 \<le> n_o S2"
+lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
 by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_s_mono)
 
 lemma n_o_narrow:
   "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
-  \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n_o (S1 \<triangle> S2) < n_o S1"
+  \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
 apply(induction S1 S2 rule: narrow_option.induct)
 apply(auto simp: n_o_def L_st_def n_s_narrow)
 done
 
-definition "n_c C = (let as = annos C in \<Sum>i=0..<size as. n_o (as!i))"
+
+definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^isub>c") where
+"n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))"
 
 lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow>
-  C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n_c (C1 \<triangle> C2) < n_c C1"
+  C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
 apply(auto simp: n_c_def Let_def Lc_acom_def narrow_acom_def)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
 prefer 2 apply (simp add: size_annos_same2)
@@ -620,7 +624,8 @@
 next
   case goal4 thus ?case by(rule n_ivl_mono)
 next
-  case goal5 thus ?case by(rule n_ivl_narrow)
+  case goal5 from goal5(2) show ?case by(rule n_ivl_narrow)
+  -- "note that the first assms is unnecessary for intervals"
 qed