# HG changeset patch
# User huffman
# Date 1237241459 25200
# Node ID 5e6088e1d6dfa86e345f7723d59f1b3f65397dfe
# Parent  24e156db414c0c35dace32bd0d544ab20bc5c593
clean up proofs

diff -r 24e156db414c -r 5e6088e1d6df src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Mon Mar 16 19:40:03 2009 +0100
+++ b/src/HOLCF/Universal.thy	Mon Mar 16 15:10:59 2009 -0700
@@ -159,20 +159,24 @@
 lemma ubasis_until_mono:
   assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b"
   shows "ubasis_le a b \<Longrightarrow> ubasis_le (ubasis_until P a) (ubasis_until P b)"
- apply (induct set: ubasis_le)
-    apply (rule ubasis_le_refl)
-   apply (erule (1) ubasis_le_trans)
-  apply (simp add: ubasis_le_refl)
-  apply (rule impI)
-  apply (rule ubasis_le_trans)
-   apply (rule ubasis_until_less)
-  apply (erule ubasis_le_lower)
- apply simp
- apply (rule impI)
- apply (subst ubasis_until_same)
-  apply (erule (3) prems)
- apply (erule (2) ubasis_le_upper)
-done
+proof (induct set: ubasis_le)
+  case (ubasis_le_refl a) show ?case by (rule ubasis_le.ubasis_le_refl)
+next
+  case (ubasis_le_trans a b c) thus ?case by - (rule ubasis_le.ubasis_le_trans)
+next
+  case (ubasis_le_lower S a i) thus ?case
+    apply (clarsimp simp add: ubasis_le_refl)
+    apply (rule ubasis_le_trans [OF ubasis_until_less])
+    apply (erule ubasis_le.ubasis_le_lower)
+    done
+next
+  case (ubasis_le_upper S b a i) thus ?case
+    apply clarsimp
+    apply (subst ubasis_until_same)
+     apply (erule (3) prems)
+    apply (erule (2) ubasis_le.ubasis_le_upper)
+    done
+qed
 
 lemma finite_range_ubasis_until:
   "finite {x. P x} \<Longrightarrow> finite (range (ubasis_until P))"
@@ -780,7 +784,7 @@
   case (ubasis_le_trans a b c) thus ?case by - (rule trans_less)
 next
   case (ubasis_le_lower S a i) thus ?case
-    apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
+    apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
      apply (erule rangeE, rename_tac x)
      apply (simp add: basis_prj_basis_emb)
      apply (simp add: node_eq_basis_emb_iff)
@@ -790,7 +794,7 @@
     done
 next
   case (ubasis_le_upper S b a i) thus ?case
-    apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
+    apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
      apply (erule rangeE, rename_tac x)
      apply (simp add: basis_prj_basis_emb)
      apply (clarsimp simp add: node_eq_basis_emb_iff)