# HG changeset patch
# User nipkow
# Date 1362738484 -3600
# Node ID d315e9a9ee72ab549a46dae48be51b056983346c
# Parent  716a94cc5aaf1f4dbc11c11f26b2fca946020e80
simplified basic termination proof

diff -r 716a94cc5aaf -r d315e9a9ee72 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri Mar 08 11:28:04 2013 +0100
@@ -197,7 +197,6 @@
 locale Measure1 =
 fixes m :: "'av::order \<Rightarrow> nat"
 fixes h :: "nat"
-assumes m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
 assumes h: "m x \<le> h"
 begin
 
@@ -208,31 +207,12 @@
 by(simp add: L_st_def m_s_def)
   (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
 
-lemma m_s1: "S1 \<le> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
-proof(auto simp add: less_eq_st_def m_s_def)
-  assume "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
-  hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
-  thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
-    by (metis setsum_mono)
-qed
-
 definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
 "m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_s S)"
 
 lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)"
 by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h)
 
-lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
-  o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
-proof(induction o1 o2 rule: less_eq_option.induct)
-  case 1 thus ?case by (simp add: m_o_def)(metis m_s1)
-next
-  case 2 thus ?case
-    by(simp add: L_option_def m_o_def le_SucI m_s_h split: option.splits)
-next
-  case 3 thus ?case by simp
-qed
-
 definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
 "m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
 
@@ -257,6 +237,9 @@
 assumes m2: "x < y \<Longrightarrow> m x > m y"
 begin
 
+lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
+by(auto simp: le_less m2)
+
 lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 > m_s S2"
 proof(auto simp add: less_st_def less_eq_st_def m_s_def)
   assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
@@ -277,7 +260,10 @@
   case 3 thus ?case by (auto simp: less_option_def)
 qed
 
-find_theorems "(_<_) = _"
+lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
+  o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
+by(auto simp: le_less m_o2)
+
 lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow>
   C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
 proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] less_acom_def L_acom_def)
diff -r 716a94cc5aaf -r d315e9a9ee72 src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Fri Mar 08 11:28:04 2013 +0100
@@ -143,9 +143,7 @@
 proof
   case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
 next
-  case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
-next
-  case goal3 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
+  case goal2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
 qed
 
 thm AI_Some_measure
diff -r 716a94cc5aaf -r d315e9a9ee72 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Mar 08 11:28:04 2013 +0100
@@ -173,9 +173,7 @@
 proof
   case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
 next
-  case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
-next
-  case goal3 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
+  case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
 qed
 
 thm AI_Some_measure
diff -r 716a94cc5aaf -r d315e9a9ee72 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Fri Mar 08 11:28:04 2013 +0100
@@ -426,18 +426,27 @@
 
 locale Measure_WN = Measure1 where m=m for m :: "'av::WN \<Rightarrow> nat" +
 fixes n :: "'av \<Rightarrow> nat"
+assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
 assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
 assumes n_mono: "x \<le> y \<Longrightarrow> n x \<le> n y"
 assumes n_narrow: "y \<le> x \<Longrightarrow> ~ x \<le> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
 
 begin
 
+lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
+proof(auto simp add: less_eq_st_def m_s_def)
+  assume "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
+  hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m_anti_mono)
+  thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
+    by (metis setsum_mono)
+qed
+
 lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
   ~ S2 \<le> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
 proof(auto simp add: less_eq_st_def m_s_def L_st_def widen_st_def)
   assume "finite(dom S1)"
   have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
-    by (metis m1 WN_class.widen1)
+    by (metis m_anti_mono WN_class.widen1)
   fix x assume "x \<in> dom S1" "\<not> fun S2 x \<le> fun S1 x"
   hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
     using m_widen by blast
@@ -445,6 +454,17 @@
   show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
 qed
 
+lemma m_o_anti_mono: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
+  o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
+proof(induction o1 o2 rule: less_eq_option.induct)
+  case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
+next
+  case 2 thus ?case
+    by(simp add: L_option_def m_o_def le_SucI m_s_h split: option.splits)
+next
+  case 3 thus ?case by simp
+qed
+
 lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
   m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1"
 by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
@@ -458,7 +478,7 @@
 apply(rule setsum_strict_mono_ex1)
 apply simp
 apply (clarsimp)
-apply(simp add: m_o1 finite_cvars widen1[where c = "strip C2"])
+apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
 apply(auto simp: le_iff_le_annos listrel_iff_nth)
 apply(rule_tac x=i in bexI)
 prefer 2 apply simp
@@ -622,9 +642,9 @@
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 and m = m_ivl and n = n_ivl and h = 3
 proof
-  case goal1 thus ?case by(rule m_ivl_anti_mono)
+  case goal2 thus ?case by(rule m_ivl_anti_mono)
 next
-  case goal2 thus ?case by(rule m_ivl_height)
+  case goal1 thus ?case by(rule m_ivl_height)
 next
   case goal3 thus ?case by(rule m_ivl_widen)
 next