Commit d834e817 authored by nipkow's avatar nipkow
Browse files

Fixes due to new order prover

parent 589a6dadfa84
......@@ -182,14 +182,17 @@ proof
by blast
have "length xs1 < length xs2"
using \<open>prefix xs1 xs2\<close> \<open>xs1 \<noteq> xs2\<close> prefix_length_prefix by fastforce
have "xs = (xs1 @ (drop (length xs1) xs))"
by (metis (no_types) \<open>(vs @ xs2) @ drop (length xs2) xs = vs @ xs\<close> \<open>prefix xs1 xs2\<close>
append_assoc append_eq_conv_conj prefixE)
have "length xs1 < length xs"
using \<open>prefix xs1 xs2\<close> \<open>prefix xs2 xs'\<close> \<open>xs = xs1 @ drop (length xs1) xs\<close> \<open>xs1 \<noteq> xs2\<close>
assms(6) leI
by fastforce
using \<open>prefix xs1 xs2\<close> \<open>xs1 \<noteq> xs2\<close> prefix_length_prefix by fastforce
have prefix_drop: "ys = ys1 @ (drop (length ys1)) ys" if "prefix ys1 ys"
for ys ys1 :: "('a \<times> 'b) list"
using that by (induction ys1) (auto elim: prefixE)
then have "xs = (xs1 @ (drop (length xs1) xs))"
using \<open>prefix xs1 xs2\<close> \<open>prefix xs2 xs'\<close> \<open>prefix xs' xs\<close> by simp
then have "length xs1 < length xs"
using prefix_drop[OF \<open>prefix xs2 xs'\<close>] \<open>prefix xs2 xs'\<close> \<open>prefix xs' xs\<close>
using \<open>length xs1 < length xs2\<close>
by (auto dest!: prefix_length_le)
have "length (xs1@(drop (length xs2) xs)) < length xs"
using \<open>length xs1 < length xs2\<close> \<open>length xs1 < length xs\<close> by auto
......
......@@ -41,7 +41,7 @@ lemma ccw_scale23: "ccw 0 a b \<Longrightarrow> r > 0 \<Longrightarrow> ccw 0 (r
lemma psi_notI: "distinct3 p q r \<Longrightarrow> psi p q r \<Longrightarrow> \<not> psi q p r"
by (auto simp: algebra_simps psi_def lex_def)
lemma not_lex_eq: "\<not> lex a b \<longleftrightarrow> lex b a \<and> a \<noteq> b"
lemma not_lex_eq: "\<not> lex a b \<longleftrightarrow> lex b a \<and> b \<noteq> a"
by (auto simp: algebra_simps lex_def prod_eq_iff)
lemma lex_trans: "lex a b \<Longrightarrow> lex b c \<Longrightarrow> lex a c"
......@@ -253,30 +253,16 @@ lemma lexs_trans: "lexs x y \<Longrightarrow> lexs y z \<Longrightarrow> lexs x
and lexs_imp_neq: "lexs a b \<Longrightarrow> a \<noteq> b"
by (auto simp: lexs_def lex_def prod_eq_iff)
declare
lexs_irrefl[THEN notE, order add less_reflE: linorder "(=) :: point => point => bool" lex lexs]
declare lex_refl[order add le_refl: linorder "(=) :: point => point => bool" lex lexs]
declare lexs_imp_lex[order add less_imp_le: linorder "(=) :: point => point => bool" lex lexs]
declare
not_lexs[THEN iffD2, order add not_lessI: linorder "(=) :: point => point => bool" lex lexs]
declare not_lex[THEN iffD2, order add not_leI: linorder "(=) :: point => point => bool" lex lexs]
declare
not_lexs[THEN iffD1, order add not_lessD: linorder "(=) :: point => point => bool" lex lexs]
declare not_lex[THEN iffD1, order add not_leD: linorder "(=) :: point => point => bool" lex lexs]
declare lex_sym_eqI[order add eqI: linorder "(=) :: point => point => bool" lex lexs]
declare eq_lex_refl[order add eqD1: linorder "(=) :: point => point => bool" lex lexs]
declare sym[THEN eq_lex_refl, order add eqD2: linorder "(=) :: point => point => bool" lex lexs]
declare lexs_trans[order add less_trans: linorder "(=) :: point => point => bool" lex lexs]
declare lexs_lex_trans[order add less_le_trans: linorder "(=) :: point => point => bool" lex lexs]
declare lex_lexs_trans[order add le_less_trans: linorder "(=) :: point => point => bool" lex lexs]
declare lex_trans[order add le_trans: linorder "(=) :: point => point => bool" lex lexs]
declare lex_neq_trans[order add le_neq_trans: linorder "(=) :: point => point => bool" lex lexs]
declare neq_lex_trans[order add neq_le_trans: linorder "(=) :: point => point => bool" lex lexs]
declare lexs_imp_neq[order add less_imp_neq: linorder "(=) :: point => point => bool" lex lexs]
declare
eq_neq_eq_imp_neq[order add eq_neq_eq_imp_neq: linorder "(=) :: point => point => bool" lex lexs]
declare not_sym[order add not_sym: linorder "(=) :: point => point => bool" lex lexs]
local_setup \<open>
HOL_Order_Tac.declare_linorder {
ops = {eq = @{term \<open>(=) :: point \<Rightarrow> point \<Rightarrow> bool\<close>}, le = @{term \<open>lex\<close>}, lt = @{term \<open>lexs\<close>}},
thms = {trans = @{thm lex_trans}, refl = @{thm lex_refl}, eqD1 = @{thm eq_lex_refl},
eqD2 = @{thm eq_lex_refl[OF sym]}, antisym = @{thm lex_sym_eqI}, contr = @{thm notE}},
conv_thms = {less_le = @{thm eq_reflection[OF lexs_def]},
nless_le = @{thm eq_reflection[OF not_lexs]},
nle_le = @{thm eq_reflection[OF not_lex_eq]}}
}
\<close>
subsection \<open>Contradictions\<close>
......
......@@ -383,8 +383,7 @@ proof (rule ccontr, auto)
by (simp add: e)+
with b show False
using piiq[of p i q]
apply auto
using b_rules using disjoint_iff_not_equal by auto
using b_rules by safe fast+
next
assume "a = END i"
with a0 have "END i \<lless> END i" by simp
......
......@@ -290,8 +290,7 @@ proof (induction bp s pc arbitrary: pc' rule: exec'.induct[case_names C])
apply (rule_tac x="TestI bexp int" in bexI, auto simp: array_idx_in_set) []
apply (rename_tac list)
apply (clarsimp split: if_split_asm simp add: Let_def)
apply (elim disjE conjE, auto) []
apply (auto split: if_split_asm)[]
apply (frule (1) C.IH(3), auto) []
apply (force)
apply (force)
......
......@@ -170,7 +170,8 @@ begin
apply (cases a)
apply (auto
simp: la_ex'_def eval_dep_vars eq_on_def
split: option.splits Option.bind_splits if_split_asm)
split: option.splits Option.bind_splits)
apply (auto split: if_split_asm)
done
lemma ex_dep_pres:
......
......@@ -289,23 +289,7 @@ apply (case_tac "ok bb", simp_all)
apply (case_tac "tr bb \<le> tr c", simp_all)
apply (case_tac "ok ca", simp_all)
apply (case_tac "tr ca \<le> tr c", simp_all)
apply (simp add: prefix_def)
apply (erule exE)+
apply (erule_tac x="zs@zsa" in allE, simp)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all add: true_def)+
apply (case_tac "ok ca", simp_all)
apply (case_tac "tr ca \<le> tr c", simp_all)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="zsa@zs" in exI, simp)
apply (rule_tac b=bb in comp_intro, simp_all)
apply (split cond_splits, simp_all)+
apply (case_tac "tr bb \<le> tr c", simp_all)
apply (simp add: prefix_def)
apply (erule exE | erule conjE)+
apply (erule_tac x="zsa@zs" in allE, simp)
apply (auto simp add: prefix_def)
apply (auto simp add: prefix_def comp_def true_def split: cond_splits)
done
......
......@@ -298,7 +298,7 @@ proof -
moreover have "?le (\<langle>\<V> s\<rangle> x) c"
using cmp c dir unfolding bound_compare_defs by auto
ultimately show ?thesis
using c dir by auto
using c dir by (auto simp del: Simplex.bounds_lg)
qed
then show ?thesis
using c by simp
......@@ -322,7 +322,7 @@ proof -
moreover have "?le c (\<langle>\<V> s\<rangle> x)"
using cmp c dir unfolding bound_compare_defs by auto
ultimately show ?thesis
using c dir by auto
using c dir by (auto simp del: Simplex.bounds_lg)
qed
then show ?thesis
using c by simp
......@@ -1630,4 +1630,4 @@ proof -
qed
end
\ No newline at end of file
end
......@@ -2047,7 +2047,8 @@ proof -
by auto
moreover from INV 1 have "insert v (set p) \<subseteq> set p \<union> set p'"
unfolding rec_loop_invar_def
apply (cases p, simp)
apply (cases p)
apply blast
apply (cases p')
apply (auto simp: path_simps)
done
......
......@@ -1100,8 +1100,9 @@ proof -
next
case False
with stk' idxI ins no_x heap_ok tconf meth a ha Xel \<Phi>_pc frame frames
wf_preallocatedD[OF wf, of h ArrayIndexOutOfBounds] preh
show ?thesis by(fastforce split: if_split_asm)
wf_preallocatedD[OF wf, of h ArrayIndexOutOfBounds]
show ?thesis
by (fastforce simp: preh split: if_split_asm simp del: Listn.lesub_list_impl_same_size)
qed
qed
qed
......@@ -1222,9 +1223,11 @@ proof -
by(auto split: if_split_asm simp del: correct_state_def intro: widen_trans)
next
case False
with stk' idxI ins no_x heap_ok tconf meth a ha Xel Te \<Phi>_pc frame frames si' preh
with stk' idxI ins no_x heap_ok tconf meth a ha Xel Te \<Phi>_pc frame frames si'
wf_preallocatedD[OF wf, of h ArrayStore]
show ?thesis by(fastforce split: if_split_asm)
show ?thesis
by (fastforce split: if_splits list.splits simp: preh
simp del: Listn.lesub_list_impl_same_size)
qed
next
case False
......
......@@ -749,7 +749,7 @@ proof(cases i)
by(rule addr_loc_type.intros)
from v' vs adal have "P,shr s \<turnstile> v' :\<le> T" by(auto dest!: vs_confD dest: addr_loc_type_fun)
with hrt adal have "heap_read (shr s) ?a (ACell (nat (sint ?i))) v'" using hconf by(rule heap_read_typeableD)
with type bounds Null aok exec_i show ?thesis by(fastforce)
with type Null aok exec_i show ?thesis apply auto using bounds by fastforce+
next
case [simp]: (Getfield F D)
let ?a = "the_Addr (hd stk)"
......
......@@ -680,7 +680,8 @@ proof -
have mset_eq: "mset xs = mset ls + mset es + mset gs" unfolding ls_def es_def gs_def
by (induction xs) auto
have length_eq: "length xs = length ls + length es + length gs" unfolding ls_def es_def gs_def
by (induction xs) auto
by (induction xs) (auto simp del: filter_True)
have [simp]: "select i es = x" if "i < length es" for i
proof -
have "select i es \<in> set (sort es)" unfolding select_def
......@@ -882,7 +883,7 @@ proof induction
next
assume *: "\<not>k < nl" "\<not>k < nl + ne"
have **: "length xs = length ls + length es + length gs"
unfolding ls_def es_def gs_def by (induction xs) auto
unfolding ls_def es_def gs_def by (induction xs) (auto simp del: filter_True)
show "fast_select (k - nl - ne) gs = select (k - nl - ne) gs"
unfolding nl_def ne_def
by (rule 1; (rule refl tw)?) (insert False * ** \<open>k < length xs\<close>, auto simp: nl_def ne_def)
......
......@@ -909,8 +909,6 @@ lemma isets_of_iivls[autoref_rules]:
le[of e _ f _, OF lv_relI lv_relI]
apply (auto simp: appr_rel_br br_def lvivl_rel_br set_of_ivl_def lv_rel_def)
using atLeastAtMost_iff apply blast
apply (drule order_trans)
apply assumption apply simp
done
done
subgoal for a b c d e f g
......
......@@ -2172,10 +2172,6 @@ lemma reduce_ivl[le, refine_vcg]: "reduce_ivl Y b \<le> SPEC (\<lambda>R. Y \<su
unfolding reduce_ivl_def
apply refine_vcg
apply (auto simp add: scaleR2_def image_def vimage_def plane_of_def )
prefer 2
subgoal using basic_trans_rules(23) by blast
prefer 3
subgoal using basic_trans_rules(23) by blast
proof goal_cases
case (1 i0 i1 s0 s1 y0 y1)
from 1 have le: "1 \<le> (y1 \<bullet> b) / (i1 \<bullet> b)"
......
......@@ -2797,7 +2797,7 @@ next
from dir ind some have *: "LB dir ?s x = Some d" "LI dir ?s x = j" by (auto simp: boundsl_def boundsu_def indexl_def indexu_def)
have d_le_vx: "lt dir d (v x) \<or> d = v x" by (intro vL[rule_format, OF *], insert some ind, auto)
from dir d_le_vx vx_le_c lt
have False by auto
have False by (auto simp del: Simplex.bounds_lg)
}
thus ?case by blast
next
......@@ -3836,7 +3836,7 @@ proof -
then show "lt dir 0 (\<langle>\<V> s\<rangle> x - v x)"
using \<open>0 \<noteq> \<langle>\<V> s\<rangle> x - v x\<close> *
using minus_gt[of "v x" "\<langle>\<V> s\<rangle> x"] minus_lt[of "\<langle>\<V> s\<rangle> x" "v x"]
by auto
by (auto simp del: Simplex.bounds_lg)
next
fix x
assume x: "x \<in> rvars_eq eq" "0 > coeff (rhs eq) x" "\<langle>\<V> s\<rangle> x - v x \<noteq> 0"
......@@ -3861,20 +3861,20 @@ proof -
then show "lt dir (\<langle>\<V> s\<rangle> x - v x) 0"
using \<open>\<langle>\<V> s\<rangle> x - v x \<noteq> 0\<close> *
using minus_lt[of "\<langle>\<V> s\<rangle> x" "v x"] minus_gt[of "v x" "\<langle>\<V> s\<rangle> x"]
by auto
by (auto simp del: Simplex.bounds_lg)
qed
then have "le (lt dir) 0 (rhs eq \<lbrace> \<lambda> x. \<langle>\<V> s\<rangle> x - v x\<rbrace>)"
using *
apply auto
using valuate_nonneg[of "rhs eq" "\<lambda>x. \<langle>\<V> s\<rangle> x - v x"]
apply force
apply (force simp del: Simplex.bounds_lg)
using valuate_nonpos[of "rhs eq" "\<lambda>x. \<langle>\<V> s\<rangle> x - v x"]
apply force
apply (force simp del: Simplex.bounds_lg)
done
then show "le (lt dir) rhs eq \<lbrace> v \<rbrace> rhs eq \<lbrace> \<langle>\<V> s\<rangle> \<rbrace>"
using \<open>dir = Positive \<or> dir = Negative\<close>
using minus_gt[of "rhs eq \<lbrace> v \<rbrace>" "rhs eq \<lbrace> \<langle>\<V> s\<rangle> \<rbrace>"]
by (auto simp add: valuate_diff[THEN sym])
by (auto simp add: valuate_diff[THEN sym] simp del: Simplex.bounds_lg)
qed
end
......@@ -5618,7 +5618,7 @@ proof (rule acyclicI, rule allI)
then show "lt dir2 0 (\<langle>?bp\<rangle> x - \<langle>?bl\<rangle> x)"
using \<open>0 \<noteq> \<langle>?bp\<rangle> x - \<langle>?bl\<rangle> x\<close>
using minus_gt[of "\<langle>?bl\<rangle> x" "\<langle>?bp\<rangle> x"] minus_lt[of "\<langle>?bp\<rangle> x" "\<langle>?bl\<rangle> x"] dir2
by auto
by (auto simp del: Simplex.bounds_lg)
next
assume "coeff (rhs ?eq) x < 0" "\<langle>?bp\<rangle> x - \<langle>?bl\<rangle> x \<noteq> 0"
then have "\<unlhd>\<^sub>l\<^sub>b (lt dir2) (\<langle>\<V> (l' ! sp)\<rangle> x) (LB dir2 (l' ! sp) x)"
......@@ -5634,7 +5634,7 @@ proof (rule acyclicI, rule allI)
then show "lt dir2 (\<langle>?bp\<rangle> x - \<langle>?bl\<rangle> x) 0"
using \<open>\<langle>?bp\<rangle> x - \<langle>?bl\<rangle> x \<noteq> 0\<close>
using minus_gt[of "\<langle>?bl\<rangle> x" "\<langle>?bp\<rangle> x"] minus_lt[of "\<langle>?bp\<rangle> x" "\<langle>?bl\<rangle> x"] dir2
by auto
by (auto simp del: Simplex.bounds_lg)
qed
next
case False
......@@ -5680,7 +5680,7 @@ proof (rule acyclicI, rule allI)
show ?thesis
using \<open>x = xr\<close>
using minus_lt[of "\<langle>?bp\<rangle> xr" "\<langle>?bl\<rangle> xr"] minus_gt[of "\<langle>?bl\<rangle> xr" "\<langle>?bp\<rangle> xr"]
by (auto split: if_splits)
by (auto split: if_splits simp del: Simplex.bounds_lg)
next
case False
then have "x > xr"
......@@ -5699,25 +5699,25 @@ proof (rule acyclicI, rule allI)
using dir2
apply auto
using valuate_nonneg[of "rhs ?eq" "\<lambda> x. \<langle>?bp\<rangle> x - \<langle>?bl\<rangle> x"]
apply force
apply (force simp del: Simplex.bounds_lg)
using valuate_nonpos[of "rhs ?eq" "\<lambda> x. \<langle>?bp\<rangle> x - \<langle>?bl\<rangle> x"]
apply force
apply (force simp del: Simplex.bounds_lg)
done
then have "le (lt dir2) 0 ((rhs ?eq) \<lbrace> \<langle>?bp\<rangle> \<rbrace> - (rhs ?eq) \<lbrace> \<langle>?bl\<rangle> \<rbrace>)"
by (subst valuate_diff)+ simp
then have "le (lt dir2) ((rhs ?eq) \<lbrace> \<langle>?bl\<rangle> \<rbrace>) ((rhs ?eq) \<lbrace> \<langle>?bp\<rangle> \<rbrace>)"
using minus_lt[of "(rhs ?eq) \<lbrace> \<langle>?bp\<rangle> \<rbrace>" "(rhs ?eq) \<lbrace> \<langle>?bl\<rangle> \<rbrace>"] dir2
by auto
by (auto simp del: Simplex.bounds_lg)
then show ?thesis
using dir2
using minus_lt[of "(rhs ?eq) \<lbrace> \<langle>?bl\<rangle> \<rbrace>" "(rhs ?eq) \<lbrace> \<langle>?bp\<rangle> \<rbrace>"]
using minus_gt[of "(rhs ?eq) \<lbrace> \<langle>?bp\<rangle> \<rbrace>" "(rhs ?eq) \<lbrace> \<langle>?bl\<rangle> \<rbrace>"]
by auto
by (auto simp del: Simplex.bounds_lg)
qed
ultimately
have False
using diff_satified dir2
by (auto split: if_splits)
by (auto split: if_splits simp del: Simplex.bounds_lg)
}
then show False
by auto
......@@ -6145,7 +6145,8 @@ proof (rule check_induct'')
with c dist[of x i c y d] dir
have yx: "y = x" "d = c" by auto
from y[unfolded yx] have "x \<in> rvars (\<T> s')" using **(1) unfolding rvars_def by force
from in_bnds[OF this] le LB not_gt i have "\<langle>\<V> s'\<rangle> x = c" unfolding yx using dir by auto
from in_bnds[OF this] le LB not_gt i have "\<langle>\<V> s'\<rangle> x = c" unfolding yx using dir
by (auto simp del: Simplex.bounds_lg)
note yx(1) this
}
moreover
......@@ -6159,7 +6160,8 @@ proof (rule check_induct'')
with c dist[of x i c y d] dir
have yx: "y = x" "d = c" by auto
from y[unfolded yx] have "x \<in> rvars (\<T> s')" using **(1) unfolding rvars_def by force
from in_bnds[OF this] le UB not_gt i have "\<langle>\<V> s'\<rangle> x = c" unfolding yx using dir by auto
from in_bnds[OF this] le UB not_gt i have "\<langle>\<V> s'\<rangle> x = c" unfolding yx using dir
by (auto simp del: Simplex.bounds_lg)
note yx(1) this
}
ultimately have "y = x" "\<langle>\<V> s'\<rangle> x = c" using coeff by blast+
......@@ -6221,7 +6223,7 @@ proof (rule check_induct'')
define diff where "diff = l\<^sub>i - \<langle>\<V> s'\<rangle> x\<^sub>i"
have "\<langle>\<V> s'\<rangle> x\<^sub>i < l\<^sub>i \<Longrightarrow> 0 < l\<^sub>i - \<langle>\<V> s'\<rangle> x\<^sub>i" "l\<^sub>i < \<langle>\<V> s'\<rangle> x\<^sub>i \<Longrightarrow> l\<^sub>i - \<langle>\<V> s'\<rangle> x\<^sub>i < 0"
using minus_gt by (blast, insert minus_lt, blast)
with lt dir have diff: "lt dir 0 diff" by (auto simp: diff_def)
with lt dir have diff: "lt dir 0 diff" by (auto simp: diff_def simp del: Simplex.bounds_lg)
define up where "up = inverse (coeff (rhs ?eq) y) *R diff"
define v where "v = \<langle>\<V> (rev.update y (\<langle>\<V> s'\<rangle> y + up) s')\<rangle>"
show ?thesis unfolding satisfies_state_index'.simps
......
......@@ -2,7 +2,7 @@
theory AndersonProof
imports IHOML
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 4, atoms e = a b c d]
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 4, atoms e = a b c d, timeout=60]
sledgehammer_params[verbose=true]
(*>*)
......
......@@ -2,7 +2,7 @@
theory FittingProof
imports IHOML
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 4, atoms e = a b c d]
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 4, atoms e = a b c d, timeout=60]
sledgehammer_params[verbose=true]
(*>*)
......
......@@ -2,7 +2,7 @@
theory GoedelProof_P2
imports IHOML
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3, atoms e = a b c d]
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3, atoms e = a b c d, timeout=60]
sledgehammer_params[verbose=true]
(*>*)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment