# HG changeset patch
# User krauss
# Date 1274648205 -7200
# Node ID 805d18dae0260c53d99d3475dc0648800c9e6b65
# Parent  2e93e29a809af389d1a223b7f6c8a17cff653ec9
used sledgehammer[isar_proof] to replace slow metis call

diff -r 2e93e29a809a -r 805d18dae026 src/HOL/Library/Kleene_Algebra.thy
--- 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 @@
 by (metis add_est1 add_est2 less_add(1) mult_assoc order_def plus_leI star_absorb_one star_mono star_slide2 star_unfold2 star_unfold_left x_less_star)
 
 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"