# HG changeset patch
# User webertj
# Date 1154476089 -7200
# Node ID b59a02641f85e987cc253f85f3bbf574cca4ebe7
# Parent  28be109916660f613bc7aeccfddc4b791ab544b7
lin_arith_prover splits certain operators (e.g. min, max, abs)

diff -r 28be10991666 -r b59a02641f85 src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Wed Aug 02 00:57:41 2006 +0200
+++ b/src/HOL/HoareParallel/Graph.thy	Wed Aug 02 01:48:09 2006 +0200
@@ -111,6 +111,8 @@
 apply(erule Ex_first_occurrence)
 done
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 lemma Graph2: 
   "\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])"
 apply (unfold Reach_def)
@@ -126,6 +128,7 @@
  apply(case_tac "j=R")
   apply(erule_tac x = "Suc i" in allE)
   apply simp
+  apply arith
  apply (force simp add:nth_list_update)
 apply simp
 apply(erule exE)
@@ -153,6 +156,7 @@
 apply simp
 apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
  prefer 2 apply arith
+apply simp
 apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
  prefer 2 apply arith
 apply simp
@@ -173,19 +177,26 @@
  prefer 2 apply arith
  apply(drule_tac n = "Suc nata" in Compl_lemma)
  apply clarify
- ML {* fast_arith_split_limit := 0; *}  (*FIXME*)
  apply force
- ML {* fast_arith_split_limit := 9; *}  (*FIXME*)
 apply(drule leI)
 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
  apply(erule_tac x = "m - (Suc nata)" in allE)
  apply(case_tac "m")
   apply simp
  apply simp
+ apply(subgoal_tac "natb - nata < Suc natb")
+  prefer 2 apply(erule thin_rl)+ apply arith
+ apply simp
+ apply(case_tac "length path")
+  apply force
+apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
 apply simp
+apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
+apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
+apply simp
+apply arith
 done
 
-
 subsubsection{* Graph 3 *}
 
 lemma Graph3: 
@@ -243,6 +254,8 @@
   apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
     prefer 2 apply arith
    apply simp
+  apply(erule mp)
+  apply arith
 --{* T is a root *}
  apply(case_tac "m=0")
   apply force
@@ -269,6 +282,8 @@
 apply(force simp add: nth_list_update)
 done
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+
 subsubsection{* Graph 4 *}
 
 lemma Graph4: