--- a/src/Doc/Codegen/Inductive_Predicate.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Fri Aug 21 12:43:07 2020 +0100
@@ -167,7 +167,7 @@
(*<*)unfolding lexordp_def by (auto simp add: append)(*>*)
lemma %quote [code_pred_intro]:
- "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b \<Longrightarrow> a\<noteq>b
+ "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b
\<Longrightarrow> lexordp r xs ys"
(*<*)unfolding lexordp_def append apply simp
apply (rule disjI2) by auto(*>*)
@@ -179,14 +179,14 @@
assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
\<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
- \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> a\<noteq>b \<Longrightarrow> thesis"
+ \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis"
{
assume "\<exists>a v. ys = xs @ a # v"
from this 1 have thesis
by (fastforce simp add: append)
} moreover
{
- assume "\<exists>u a b v w. r a b \<and> a\<noteq>b \<and> xs = u @ a # v \<and> ys = u @ b # w"
+ assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w"
from this 2 have thesis by (fastforce simp add: append)
} moreover
note lexord
--- a/src/HOL/Corec_Examples/Stream_Processor.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/HOL/Corec_Examples/Stream_Processor.thy Fri Aug 21 12:43:07 2020 +0100
@@ -61,26 +61,20 @@
lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)"
by (subst copy.code; simp)
-lemma wf_imp_irrefl:
- assumes "wf r" shows "irrefl r"
- using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
-
-
corecursive sp_comp (infixl "oo" 65) where
"sp oo sp' = (case (out sp, out sp') of
(Put b sp, _) \<Rightarrow> In (Put b (sp oo sp'))
| (Get f, Put b sp) \<Rightarrow> In (f b) oo sp
| (_, Get g) \<Rightarrow> get (\<lambda>a. (sp oo In (g a))))"
- apply(relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
- apply(auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
- by (metis Get_neq)
+ by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
+ (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
lemma run_copy_unique:
- "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
- apply corec_unique
- apply(rule ext)
- apply(subst copy.code)
- apply simp
- done
+ "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
+apply corec_unique
+apply(rule ext)
+apply(subst copy.code)
+apply simp
+done
end
--- a/src/HOL/Fun_Def.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/HOL/Fun_Def.thy Fri Aug 21 12:43:07 2020 +0100
@@ -208,7 +208,7 @@
by (auto simp: pair_less_def)
lemma total_pair_less [iff]: "total_on A pair_less" and trans_pair_less [iff]: "trans pair_less"
- by (auto simp: total_on_def pair_less_def antisym_def)
+ by (auto simp: total_on_def pair_less_def)
text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
--- a/src/HOL/Library/List_Lenlexorder.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/HOL/Library/List_Lenlexorder.thy Fri Aug 21 12:43:07 2020 +0100
@@ -25,20 +25,17 @@
proof
have tr: "trans {(u, v::'a). u < v}"
using trans_def by fastforce
- have ant: "antisym {(u, v::'a). u < v}"
- using antisym_def order.asym by auto
have \<section>: False
if "(xs,ys) \<in> lenlex {(u, v). u < v}" "(ys,xs) \<in> lenlex {(u, v). u < v}" for xs ys :: "'a list"
proof -
have "(xs,xs) \<in> lenlex {(u, v). u < v}"
- using that ant transD [OF lenlex_transI [OF tr]] by blast
+ using that transD [OF lenlex_transI [OF tr]] by blast
then show False
by (meson case_prodD lenlex_irreflexive less_irrefl mem_Collect_eq)
qed
show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def)
show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list"
- using that ant transD [OF lenlex_transI [OF tr]]
- by (auto simp add: list_le_def list_less_def)
+ using that transD [OF lenlex_transI [OF tr]] by (auto simp add: list_le_def list_less_def)
show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list"
using \<section> that list_le_def list_less_def by blast
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
@@ -72,12 +69,19 @@
lemma Nil_less_Cons [simp]: "[] < a # x"
by (simp add: list_less_def)
+lemma Cons_less_Cons: "a # x < b # y \<longleftrightarrow> length x < length y \<or> length x = length y \<and> (a < b \<or> a = b \<and> x < y)"
+ using lenlex_length
+ by (fastforce simp: list_less_def Cons_lenlex_iff)
+
lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
unfolding list_le_def by (cases x) auto
lemma Nil_le_Cons [simp]: "[] \<le> x"
unfolding list_le_def by (cases x) auto
+lemma Cons_le_Cons: "a # x \<le> b # y \<longleftrightarrow> length x < length y \<or> length x = length y \<and> (a < b \<or> a = b \<and> x \<le> y)"
+ by (auto simp: list_le_def Cons_less_Cons)
+
instantiation list :: (order) order_bot
begin
@@ -88,15 +92,4 @@
end
-lemma Cons_less_Cons:
- fixes a :: "'a::order"
- shows "a # xs < b # ys \<longleftrightarrow> length xs < length ys \<or> length xs = length ys \<and> (a < b \<or> a = b \<and> xs < ys)"
- using lenlex_length
- by (fastforce simp: list_less_def Cons_lenlex_iff)
-
-lemma Cons_le_Cons:
- fixes a :: "'a::order"
- shows "a # xs \<le> b # ys \<longleftrightarrow> length xs < length ys \<or> length xs = length ys \<and> (a < b \<or> a = b \<and> xs \<le> ys)"
- by (auto simp: list_le_def Cons_less_Cons)
-
end
--- a/src/HOL/Library/List_Lexorder.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/HOL/Library/List_Lexorder.thy Fri Aug 21 12:43:07 2020 +0100
@@ -26,20 +26,17 @@
let ?r = "{(u, v::'a). u < v}"
have tr: "trans ?r"
using trans_def by fastforce
- have *: "antisym {(u, v::'a). u < v}"
- using antisym_def by fastforce
have \<section>: False
if "(xs,ys) \<in> lexord ?r" "(ys,xs) \<in> lexord ?r" for xs ys :: "'a list"
proof -
have "(xs,xs) \<in> lexord ?r"
- using lexord_trans that tr * by blast
+ using that transD [OF lexord_transI [OF tr]] by blast
then show False
by (meson case_prodD lexord_irreflexive less_irrefl mem_Collect_eq)
qed
show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def)
show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list"
- using that transD [OF lexord_transI [OF tr]] *
- by (auto simp add: list_le_def list_less_def)
+ using that transD [OF lexord_transI [OF tr]] by (auto simp add: list_le_def list_less_def)
show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list"
using \<section> that list_le_def list_less_def by blast
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
@@ -73,7 +70,7 @@
lemma Nil_less_Cons [simp]: "[] < a # x"
by (simp add: list_less_def)
-lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> (if a = b then x < y else a < b)"
+lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
by (simp add: list_less_def)
lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
@@ -82,7 +79,7 @@
lemma Nil_le_Cons [simp]: "[] \<le> x"
unfolding list_le_def by (cases x) auto
-lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> (if a = b then x \<le> y else a < b)"
+lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
unfolding list_le_def by auto
instantiation list :: (order) order_bot
--- a/src/HOL/List.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/HOL/List.thy Fri Aug 21 12:43:07 2020 +0100
@@ -6348,11 +6348,11 @@
lemma lexn_conv:
"lexn r n =
{(xs,ys). length xs = n \<and> length ys = n \<and>
- (\<exists>xys x y xs' ys'. xs = xys @ x#xs' \<and> ys = xys @ y # ys' \<and> x\<noteq>y \<and> (x,y) \<in> r)}"
+ (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"
proof (induction n)
case (Suc n)
- show ?case
- apply (simp add: Suc image_Collect lex_prod_def, safe, blast)
+ then show ?case
+ apply (simp add: image_Collect lex_prod_def, safe, blast)
apply (rule_tac x = "ab # xys" in exI, simp)
apply (case_tac xys; force)
done
@@ -6360,7 +6360,7 @@
text\<open>By Mathias Fleury:\<close>
proposition lexn_transI:
- assumes "trans r" "antisym r" shows "trans (lexn r n)"
+ assumes "trans r" shows "trans (lexn r n)"
unfolding trans_def
proof (intro allI impI)
fix as bs cs
@@ -6369,13 +6369,13 @@
n: "length as = n" and "length bs = n" and
as: "as = abs @ a # as'" and
bs: "bs = abs @ b # bs'" and
- abr: "(a, b) \<in> r" "a\<noteq>b"
+ abr: "(a, b) \<in> r"
using asbs unfolding lexn_conv by blast
obtain bcs b' c' cs' bs' where
n': "length cs = n" and "length bs = n" and
bs': "bs = bcs @ b' # bs'" and
cs: "cs = bcs @ c' # cs'" and
- b'c'r: "(b', c') \<in> r" "b'\<noteq>c'"
+ b'c'r: "(b', c') \<in> r"
using bscs unfolding lexn_conv by blast
consider (le) "length bcs < length abs"
| (eq) "length bcs = length abs"
@@ -6385,7 +6385,7 @@
let ?k = "length bcs"
case le
hence "as ! ?k = bs ! ?k" unfolding as bs by (simp add: nth_append)
- hence "(as ! ?k, cs ! ?k) \<in> r" "as ! ?k \<noteq> cs ! ?k" using b'c'r unfolding bs' cs by auto
+ hence "(as ! ?k, cs ! ?k) \<in> r" using b'c'r unfolding bs' cs by auto
moreover
have "length bcs < length as" using le unfolding as by simp
from id_take_nth_drop[OF this]
@@ -6397,12 +6397,12 @@
moreover have "take ?k as = take ?k cs"
using le arg_cong[OF bs, of "take (length bcs)"]
unfolding cs as bs' by auto
- ultimately show ?thesis using n n' \<open>b'\<noteq>c'\<close> unfolding lexn_conv by auto
+ ultimately show ?thesis using n n' unfolding lexn_conv by auto
next
let ?k = "length abs"
case ge
hence "bs ! ?k = cs ! ?k" unfolding bs' cs by (simp add: nth_append)
- hence "(as ! ?k, cs ! ?k) \<in> r" "as ! ?k \<noteq> cs ! ?k" using abr unfolding as bs by auto
+ hence "(as ! ?k, cs ! ?k) \<in> r" using abr unfolding as bs by auto
moreover
have "length abs < length as" using ge unfolding as by simp
from id_take_nth_drop[OF this]
@@ -6418,23 +6418,21 @@
let ?k = "length abs"
case eq
hence *: "abs = bcs" "b = b'" using bs bs' by auto
- then have "a\<noteq>c'"
- using abr(1) antisymD assms(2) b'c'r(1) b'c'r(2) by fastforce
- have "(a, c') \<in> r"
- using * abr b'c'r assms unfolding trans_def by blast
- with * \<open>a\<noteq>c'\<close> show ?thesis using n n' unfolding lexn_conv as bs cs by auto
+ hence "(a, c') \<in> r"
+ using abr b'c'r assms unfolding trans_def by blast
+ with * show ?thesis using n n' unfolding lexn_conv as bs cs by auto
qed
qed
corollary lex_transI:
- assumes "trans r" "antisym r" shows "trans (lex r)"
+ assumes "trans r" shows "trans (lex r)"
using lexn_transI [OF assms]
by (clarsimp simp add: lex_def trans_def) (metis lexn_length)
lemma lex_conv:
"lex r =
{(xs,ys). length xs = length ys \<and>
- (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> x\<noteq>y \<and> (x,y) \<in> r)}"
+ (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y) \<in> r)}"
by (force simp add: lex_def lexn_conv)
lemma wf_lenlex [intro!]: "wf r \<Longrightarrow> wf (lenlex r)"
@@ -6457,15 +6455,15 @@
then consider "(x,y) \<in> r" | "(y,x) \<in> r"
by (meson UNIV_I assms total_on_def)
then show ?thesis
- by cases (use len \<open>x\<noteq>y\<close> in \<open>(force simp add: lexn_conv xs ys)+\<close>)
+ by cases (use len in \<open>(force simp add: lexn_conv xs ys)+\<close>)
qed
then show ?thesis
by (fastforce simp: lenlex_def total_on_def lex_def)
qed
-lemma lenlex_transI [intro]: "\<lbrakk>trans r; antisym r\<rbrakk> \<Longrightarrow> trans (lenlex r)"
+lemma lenlex_transI [intro]: "trans r \<Longrightarrow> trans (lenlex r)"
unfolding lenlex_def
- by (simp add: antisym_def lex_transI trans_inv_image)
+ by (meson lex_transI trans_inv_image trans_less_than trans_lex_prod)
lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
by (simp add: lex_conv)
@@ -6474,8 +6472,8 @@
by (simp add:lex_conv)
lemma Cons_in_lex [simp]:
- "(x # xs, y # ys) \<in> lex r \<longleftrightarrow> x\<noteq>y \<and> (x,y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r"
- (is "?lhs = ?rhs")
+ "(x # xs, y # ys) \<in> lex r \<longleftrightarrow> (x, y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r"
+ (is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
by (simp add: lex_conv) (metis hd_append list.sel(1) list.sel(3) tl_append2)
@@ -6491,7 +6489,7 @@
lemma Cons_lenlex_iff:
"((m # ms, n # ns) \<in> lenlex r) \<longleftrightarrow>
length ms < length ns
- \<or> length ms = length ns \<and> m\<noteq>n \<and> (m,n) \<in> r
+ \<or> length ms = length ns \<and> (m,n) \<in> r
\<or> (m = n \<and> (ms,ns) \<in> lenlex r)"
by (auto simp: lenlex_def)
@@ -6499,7 +6497,7 @@
by (induction xs) (auto simp add: Cons_lenlex_iff)
lemma lenlex_trans:
- "\<lbrakk>(x,y) \<in> lenlex r; (y,z) \<in> lenlex r; trans r; antisym r\<rbrakk> \<Longrightarrow> (x,z) \<in> lenlex r"
+ "\<lbrakk>(x,y) \<in> lenlex r; (y,z) \<in> lenlex r; trans r\<rbrakk> \<Longrightarrow> (x,z) \<in> lenlex r"
by (meson lenlex_transI transD)
lemma lenlex_length: "(ms, ns) \<in> lenlex r \<Longrightarrow> length ms \<le> length ns"
@@ -6547,30 +6545,23 @@
definition lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
"lexord r = {(x,y). \<exists> a v. y = x @ a # v \<or>
- (\<exists> u a b v w. (a,b) \<in> r \<and> a\<noteq>b \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
-
+ (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
- by (unfold lexord_def, induct_tac y, auto)
+by (unfold lexord_def, induct_tac y, auto)
lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
- by (unfold lexord_def, induct_tac x, auto)
+by (unfold lexord_def, induct_tac x, auto)
lemma lexord_cons_cons[simp]:
- "(a # x, b # y) \<in> lexord r \<longleftrightarrow> (if a=b then (x,y)\<in> lexord r else (a,b)\<in> r)" (is "?lhs = ?rhs")
+ "(a # x, b # y) \<in> lexord r \<longleftrightarrow> (a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r)" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
apply (simp add: lexord_def)
apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
done
-next
- assume ?rhs
- then show ?lhs
- apply (simp add: lexord_def split: if_split_asm)
- apply (meson Cons_eq_appendI)
- by blast
-qed
+qed (auto simp add: lexord_def; (blast | meson Cons_eq_appendI))
lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
@@ -6578,7 +6569,7 @@
by (induct_tac x, auto)
lemma lexord_append_left_rightI:
- "\<lbrakk>(a,b) \<in> r; a\<noteq>b\<rbrakk> \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
+ "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
by (induct_tac u, auto)
lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
@@ -6591,13 +6582,13 @@
lemma lexord_take_index_conv:
"((x,y) \<in> lexord r) =
((length x < length y \<and> take (length x) y = x) \<or>
- (\<exists>i. i < min(length x)(length y) \<and> take i x = take i y \<and> (x!i,y!i) \<in> r \<and> x!i \<noteq> y!i))"
+ (\<exists>i. i < min(length x)(length y) \<and> take i x = take i y \<and> (x!i,y!i) \<in> r))"
proof -
have "(\<exists>a v. y = x @ a # v) = (length x < length y \<and> take (length x) y = x)"
by (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le)
moreover
- have "(\<exists>u a b. (a,b) \<in> r \<and> a\<noteq>b \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
- (\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r \<and> x!i \<noteq> y!i)"
+ have "(\<exists>u a b. (a, b) \<in> r \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
+ (\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r)"
apply safe
using less_iff_Suc_add apply auto[1]
by (metis id_take_nth_drop)
@@ -6613,12 +6604,10 @@
qed auto
lemma lexord_irreflexive: "\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
- by (induct xs) auto
+by (induct xs) auto
text\<open>By Ren\'e Thiemann:\<close>
lemma lexord_partial_trans:
- assumes "antisym r"
- shows
"(\<And>x y z. x \<in> set xs \<Longrightarrow> (x,y) \<in> r \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> (x,z) \<in> r)
\<Longrightarrow> (xs,ys) \<in> lexord r \<Longrightarrow> (ys,zs) \<in> lexord r \<Longrightarrow> (xs,zs) \<in> lexord r"
proof (induct xs arbitrary: ys zs)
@@ -6629,13 +6618,11 @@
from Cons(3) obtain y ys where yys: "yys = y # ys" unfolding lexord_def
by (cases yys, auto)
note Cons = Cons[unfolded yys]
- from Cons(3) have one: "x\<noteq>y \<and> (x,y) \<in> r \<or> x = y \<and> (xs,ys) \<in> lexord r"
- by (auto split: if_split_asm)
+ from Cons(3) have one: "(x,y) \<in> r \<or> x = y \<and> (xs,ys) \<in> lexord r" by auto
from Cons(4) obtain z zs where zzs: "zzs = z # zs" unfolding lexord_def
by (cases zzs, auto)
note Cons = Cons[unfolded zzs]
- from Cons(4) have two: "y \<noteq> z \<and> (y,z) \<in> r \<or> y = z \<and> (ys,zs) \<in> lexord r"
- by (auto split: if_split_asm)
+ from Cons(4) have two: "(y,z) \<in> r \<or> y = z \<and> (ys,zs) \<in> lexord r" by auto
{
assume "(xs,ys) \<in> lexord r" and "(ys,zs) \<in> lexord r"
from Cons(1)[OF _ this] Cons(2)
@@ -6646,16 +6633,15 @@
from Cons(2)[OF _ this] have "(x,z) \<in> r" by auto
} note ind2 = this
from one two ind1 ind2
- have "x\<noteq>z \<and> (x,z) \<in> r \<or> x = z \<and> (xs,zs) \<in> lexord r"
- using assms by (auto simp: antisym_def)
- thus ?case unfolding zzs by (auto split: if_split_asm)
+ have "(x,z) \<in> r \<or> x = z \<and> (xs,zs) \<in> lexord r" by blast
+ thus ?case unfolding zzs by auto
qed
lemma lexord_trans:
- "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r; antisym r\<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
- by(auto simp: trans_def intro: lexord_partial_trans)
-
-lemma lexord_transI: "\<lbrakk>trans r; antisym r\<rbrakk> \<Longrightarrow> trans (lexord r)"
+ "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
+ by(auto simp: trans_def intro:lexord_partial_trans)
+
+lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
by (meson lexord_trans transI)
lemma total_lexord: "total r \<Longrightarrow> total (lexord r)"
@@ -6673,7 +6659,7 @@
by (metis lexord_Nil_left list.exhaust)
next
case (Cons a x y) then show ?case
- by (metis eq_Nil_appendI lexord_append_rightI lexord_cons_cons list.exhaust)
+ by (cases y) (force+)
qed
qed
@@ -6860,7 +6846,7 @@
lemma lexordp_conv_lexord:
"lexordp xs ys \<longleftrightarrow> (xs, ys) \<in> lexord {(x, y). x < y}"
- by (simp add: lexordp_iff lexord_def; blast)
+by(simp add: lexordp_iff lexord_def)
lemma lexordp_eq_antisym:
assumes "lexordp_eq xs ys" "lexordp_eq ys xs"
@@ -7415,8 +7401,8 @@
lemma [code]:
"lexordp r xs [] = False"
"lexordp r [] (y#ys) = True"
- "lexordp r (x # xs) (y # ys) = (if x = y then lexordp r xs ys else r x y)"
- unfolding lexordp_def by auto
+ "lexordp r (x # xs) (y # ys) = (r x y \<or> (x = y \<and> lexordp r xs ys))"
+unfolding lexordp_def by auto
text \<open>Bounded quantification and summation over nats.\<close>
--- a/src/HOL/MicroJava/DFA/Kildall.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 21 12:43:07 2020 +0100
@@ -327,10 +327,6 @@
done
qed
-(*for lex*)
-lemma ne_lesssub_iff [simp]: "y\<noteq>x \<and> x <[r] y \<longleftrightarrow> x <[r] y"
- by (meson lesssub_def)
-
lemma iter_properties[rule_format]:
assumes semilat: "semilat (A, r, f)"
shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
--- a/src/HOL/Wellfounded.thy Thu Aug 20 21:56:28 2020 +0200
+++ b/src/HOL/Wellfounded.thy Fri Aug 21 12:43:07 2020 +0100
@@ -770,13 +770,9 @@
definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
(infixr "<*lex*>" 80)
- where "ra <*lex*> rb = {((a, b), (a', b')). a \<noteq> a' \<and> (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
+ where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
-lemma in_lex_prod[simp]: "NO_MATCH less_than r \<Longrightarrow> ((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> a \<noteq> a' \<and> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
- by (auto simp:lex_prod_def)
-
-text\<open>compared with @{thm[source]in_lex_prod} this yields simpler results\<close>
-lemma in_lex_prod_less_than[simp]: "((a, b), (a', b')) \<in> less_than <*lex*> s \<longleftrightarrow>a<a' \<or> a = a' \<and> (b, b') \<in> s"
+lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
by (auto simp:lex_prod_def)
lemma wf_lex_prod [intro!]:
@@ -803,9 +799,8 @@
qed auto
text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
-lemma trans_lex_prod [simp,intro!]: "\<lbrakk>trans R1; trans R2; antisym R1\<rbrakk> \<Longrightarrow> trans (R1 <*lex*> R2)"
- unfolding trans_def antisym_def lex_prod_def by blast
-
+lemma trans_lex_prod [simp,intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
+ unfolding trans_def lex_prod_def by blast
lemma total_on_lex_prod [simp]: "total_on A r \<Longrightarrow> total_on B s \<Longrightarrow> total_on (A \<times> B) (r <*lex*> s)"
by (auto simp: total_on_def)