# HG changeset patch
# User webertj
# Date 1154372800 -7200
# Node ID 0ca998e83447b6efb261ba0cb63ed7315513a415
# Parent  e76e77e0d615fe447ebf6aefac50ce4c52ac39f2
lin_arith_prover splits certain operators (e.g. min, max, abs)

diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Jul 31 20:56:49 2006 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Jul 31 21:06:40 2006 +0200
@@ -329,7 +329,7 @@
 apply(rule_tac x=0 in exI,simp)
 done
 
-lemma Basic_sound: 
+lemma Basic_sound:
   " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; 
   stable pre rely; stable post rely\<rbrakk>
   \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
@@ -369,16 +369,15 @@
 apply(drule_tac s="Some (Basic f)" in sym,simp)
 apply(case_tac "x!Suc j",simp)
 apply(rule ctran.elims,simp)
-apply(simp_all)
+       apply(simp_all)
 apply(drule_tac c=sa in subsetD,simp)
 apply clarify
 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
- apply(case_tac x,simp+)
+  apply(case_tac x,simp+)
  apply(erule_tac x=i in allE)
-apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
-  apply arith+
+ apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
 apply(case_tac x)
-apply(simp add:last_length)+
+ apply(simp add:last_length)+
 done
 
 subsubsection{* Soundness of the Await rule *}
@@ -497,7 +496,7 @@
 apply(drule_tac s="Some (Await b P)" in sym,simp)
 apply(case_tac "x!Suc j",simp)
 apply(rule ctran.elims,simp)
-apply(simp_all)
+       apply(simp_all)
 apply(drule Star_imp_cptn) 
 apply clarify
 apply(erule_tac x=sa in allE)
@@ -511,16 +510,17 @@
 apply simp
 apply clarify
 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
- apply(case_tac x,simp+)
+  apply(case_tac x,simp+)
  apply(erule_tac x=i in allE)
-apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
- apply arith+
+ apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
 apply(case_tac x)
-apply(simp add:last_length)+
+ apply(simp add:last_length)+
 done
 
 subsubsection{* Soundness of the Conditional rule *}
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 lemma Cond_sound: 
   "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; 
   \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
@@ -537,6 +537,7 @@
     apply(simp add:assum_def)
    apply(simp add:assum_def)
   apply(erule_tac m="length x" in etran_or_ctran,simp+)
+  apply(case_tac x,simp+)
  apply(case_tac x, (simp add:last_length)+)
 apply(erule exE)
 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
@@ -548,7 +549,18 @@
  apply(erule_tac x="sa" in allE)
  apply(drule_tac c="drop (Suc m) x" in subsetD)
   apply simp
+  apply(rule conjI)
+   apply force
   apply clarify
+  apply(subgoal_tac "(Suc m) + i \<le> length x")
+   apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
+    apply(rotate_tac -2)
+    apply simp
+    apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
+    apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
+    apply arith
+   apply arith
+  apply arith
  apply simp
  apply clarify
  apply(case_tac "i\<le>m")
@@ -557,34 +569,52 @@
    apply(erule_tac x=i in allE, erule impE, assumption)
    apply simp+
  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
- apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
-  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
-   apply(rotate_tac -2)
+  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+    apply(rotate_tac -2)
+    apply simp
+    apply(erule mp)
+    apply arith
+   apply arith
+  apply arith
+  apply(case_tac "length (drop (Suc m) x)",simp)
+  apply(erule_tac x="sa" in allE)
+  back
+  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
+   apply(rule conjI)
+    apply force
+   apply clarify
+   apply(subgoal_tac "(Suc m) + i \<le> length x")
+    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
+     apply(rotate_tac -2)
+     apply simp
+     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
+     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
+      apply simp
+     apply arith
+    apply arith
+   apply arith
+  apply simp
+  apply clarify
+  apply(case_tac "i\<le>m")
+   apply(drule le_imp_less_or_eq)
+   apply(erule disjE)
+    apply(erule_tac x=i in allE, erule impE, assumption)
+    apply simp
    apply simp
+  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+    apply(rotate_tac -2)
+    apply simp
+    apply(erule mp)
+   apply arith
   apply arith
  apply arith
-apply(case_tac "length (drop (Suc m) x)",simp)
-apply(erule_tac x="sa" in allE)
-back
-apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
- apply clarify
-apply simp
-apply clarify
-apply(case_tac "i\<le>m")
- apply(drule le_imp_less_or_eq)
- apply(erule disjE)
-  apply(erule_tac x=i in allE, erule impE, assumption)
-  apply simp
- apply simp
-apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
-apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
- apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
-  apply(rotate_tac -2)
-  apply simp
- apply arith
-apply arith
 done
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+
 subsubsection{* Soundness of the Sequential rule *}
 
 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
@@ -626,6 +656,7 @@
  apply(simp add:lift_def)
 apply simp
 done
+
 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
 
 lemma Seq_sound2 [rule_format]: 
@@ -683,6 +714,7 @@
   apply simp+
 apply(simp add:lift_def)
 done
+
 (*
 lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
 apply(simp only:last_length [THEN sym])
@@ -705,6 +737,8 @@
 apply simp
 done
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 lemma Seq_sound: 
   "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
   \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
@@ -828,6 +862,8 @@
       apply simp
       apply(erule mp)
       apply(case_tac ys,simp+)
+     apply arith
+    apply arith
    apply force
   apply arith
  apply force
@@ -841,6 +877,8 @@
  apply(case_tac ys,simp+)
 done
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+
 subsubsection{* Soundness of the While rule *}
 
 lemma last_append[rule_format]:
@@ -886,6 +924,8 @@
 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
 done
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 lemma While_sound_aux [rule_format]: 
   "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
    stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk> 
@@ -1052,6 +1092,8 @@
 apply simp
 done
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+
 lemma While_sound: 
   "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely;
     \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Mon Jul 31 20:56:49 2006 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy	Mon Jul 31 21:06:40 2006 +0200
@@ -317,7 +317,6 @@
       apply simp
      apply clarsimp
     apply clarsimp
-   apply arith
    prefer 2
    apply clarsimp
   apply (clarsimp simp: nat_distrib)
diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Jul 31 20:56:49 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Jul 31 21:06:40 2006 +0200
@@ -968,14 +968,14 @@
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
+apply simp
 apply (rule progression_refl)
 
  (* case b= False *)
 apply simp
 apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
+apply simp
 apply fast
 
 (* case exit Loop *)
@@ -1003,7 +1003,7 @@
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
-apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
+apply simp
 apply (rule progression_refl)
 
 
diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Jul 31 20:56:49 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Jul 31 21:06:40 2006 +0200
@@ -663,7 +663,7 @@
   (* show P x of bspec *)
 apply simp
   apply (subgoal_tac "length mt_pre \<le> pc'")
-  apply (simp add: nth_append) apply arith
+  apply (simp add: nth_append)
 
   (* subgoals *)
 apply (simp add: eff_def xcpt_eff_def)
@@ -965,7 +965,6 @@
 apply (simp only:)
 apply (rule check_type_mono) apply assumption
 apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
-apply arith
 apply (simp add: nth_append)
 
 apply (erule conjE)+
@@ -1283,6 +1282,7 @@
   apply auto
   done
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
 
 lemma bc_mt_corresp_Invoke: "\<lbrakk> wf_prog wf_mb G; 
   max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
@@ -1319,6 +1319,7 @@
 apply (simp add: max_def)
   done
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemma wt_instr_Ifcmpeq: "\<lbrakk>Suc pc < max_pc; 
   0 \<le> (int pc + i);  nat (int pc + i) < max_pc;
@@ -1643,7 +1644,7 @@
 done
 
 
-
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
 
 lemma wt_method_compTpExpr_Exprs_corresp: "
   \<lbrakk> jmb = (pns,lvars,blk,res); 
@@ -1922,6 +1923,7 @@
 
 done
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = 
   wt_method_compTpExpr_Exprs_corresp [THEN conjunct1]
diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Mon Jul 31 20:56:49 2006 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Mon Jul 31 21:06:40 2006 +0200
@@ -175,11 +175,6 @@
      apply (rule_tac [!] funprod_zgcd)
      apply safe
      apply simp_all
-   apply (subgoal_tac "i<n")
-    prefer 2
-    apply arith
-   apply (case_tac [2] i)
-    apply simp_all
   done
 
 lemma x_sol_lin_aux:
diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Mon Jul 31 20:56:49 2006 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Mon Jul 31 21:06:40 2006 +0200
@@ -72,7 +72,6 @@
    apply (simp add: fib.Suc_Suc mod_Suc)
   apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
                    mod_Suc zmult_int [symmetric])
-  apply (presburger (no_abs))
   done
 
 text{*We now obtain a version for the natural numbers via the coercion 
diff -r e76e77e0d615 -r 0ca998e83447 src/HOL/NumberTheory/Gauss.thy
--- a/src/HOL/NumberTheory/Gauss.thy	Mon Jul 31 20:56:49 2006 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy	Mon Jul 31 21:06:40 2006 +0200
@@ -253,8 +253,6 @@
 lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   by (auto simp add: D_eq)
 
-ML {* fast_arith_split_limit := 0; *} (*FIXME*)
-
 lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   apply (auto simp add: F_eq A_def)
 proof -
@@ -270,8 +268,6 @@
     using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
 qed
 
-ML {* fast_arith_split_limit := 9; *} (*FIXME*)
-
 lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)