author krauss Sun, 23 May 2010 22:56:45 +0200 changeset 37095 805d18dae026 parent 37094 2e93e29a809a child 37100 c11cdb5e7e97
used sledgehammer[isar_proof] to replace slow metis call
```--- a/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 17:23:18 2010 +0100
+++ b/src/HOL/Library/Kleene_Algebra.thy	Sun May 23 22:56:45 2010 +0200
@@ -319,8 +319,14 @@

lemma ka25: "star y * star x \<le> star x * star y \<Longrightarrow> star (star y * star x) \<le> star x * star y"
--- {* Takes several minutes on my computer. *}
-by (metis mult_assoc mult_right_mono order_trans star_idemp star_mult_idem star_simulation_leq_2 star_slide x_less_star zero_minimum)
+proof -
+  assume "star y * star x \<le> star x * star y"
+  hence "\<forall>x\<^isub>1. star y * (star x * x\<^isub>1) \<le> star x * (star y * x\<^isub>1)" by (metis mult_assoc mult_right_mono zero_minimum)
+  hence "star y * (star x * star y) \<le> star x * star y" by (metis star_mult_idem)
+  hence "\<exists>x\<^isub>1. star (star y * star x) * star x\<^isub>1 \<le> star x * star y" by (metis star_decomp star_idemp star_simulation_leq_2 star_slide)
+  hence "\<exists>x\<^isub>1\<ge>star (star y * star x). x\<^isub>1 \<le> star x * star y" by (metis x_less_star)
+  thus "star (star y * star x) \<le> star x * star y" by (metis order_trans)
+qed

lemma church_rosser:
"star y * star x \<le> star x * star y \<Longrightarrow> star (x + y) \<le> star x * star y"```