# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1597916366 -3600
# Node ID 6f20a44c3cb173f931a512c54536b50ab62000f0
# Parent  7075fe8ffd76c80302cff513c98f27285d9317a6
two more lex fixes

diff -r 7075fe8ffd76 -r 6f20a44c3cb1 src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Wed Aug 19 14:58:02 2020 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Thu Aug 20 10:39:26 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
+  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b \<Longrightarrow> a\<noteq>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> thesis"
+    \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> a\<noteq>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> xs = u @ a # v \<and> ys = u @ b # w"
+    assume "\<exists>u a b v w. r a b \<and> a\<noteq>b \<and> xs = u @ a # v \<and> ys = u @ b # w"
     from this 2 have thesis by (fastforce simp add: append)
   } moreover
   note lexord
diff -r 7075fe8ffd76 -r 6f20a44c3cb1 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Wed Aug 19 14:58:02 2020 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Thu Aug 20 10:39:26 2020 +0100
@@ -327,6 +327,10 @@
     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;
@@ -446,13 +450,13 @@
 proof -
   interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P"
-apply (unfold kildall_def)
-apply(case_tac "iter f step ss0 (unstables r step ss0)")
-apply(simp)
-apply (rule iter_properties)
-apply (simp_all add: unstables_def stable_def)
-apply (rule semilat)
-done
+    apply (unfold kildall_def)
+    apply(case_tac "iter f step ss0 (unstables r step ss0)")
+    apply(simp)
+    apply (rule iter_properties)
+            apply (simp_all add: unstables_def stable_def)
+    apply (rule semilat)
+    done
 qed
 
 lemma is_bcv_kildall: