# HG changeset patch
# User huffman
# Date 1200527480 -3600
# Node ID 0ca392ab7f37ee02b71f9e99d711662eb023d9cb
# Parent  8df5eabda5f6044f2b2c53db8e8bb852d36e5f6e
change class axiom chfin to rule_format

diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Adm.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -41,12 +41,8 @@
 
 text {* for chain-finite (easy) types every formula is admissible *}
 
-lemma adm_max_in_chain:
-  "\<forall>Y. chain (Y::nat \<Rightarrow> 'a) \<longrightarrow> (\<exists>n. max_in_chain n Y)
-    \<Longrightarrow> adm (P::'a \<Rightarrow> bool)"
-by (auto simp add: adm_def maxinch_is_thelub)
-
-lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
+lemma adm_chfin: "adm (P::'a::chfin \<Rightarrow> bool)"
+by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
 
 subsection {* Admissibility of special formulae and propagation *}
 
diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -404,7 +404,7 @@
     \<Longrightarrow> \<forall>Y::nat \<Rightarrow> 'b. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
 apply clarify
 apply (drule_tac f=g in chain_monofun)
-apply (drule chfin [rule_format])
+apply (drule chfin)
 apply (unfold max_in_chain_def)
 apply (simp add: injection_eq)
 done
diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -306,7 +306,7 @@
 done
 
 instance "*" :: (chfin, chfin) chfin
-apply (intro_classes, clarify)
+apply intro_classes
 apply (erule compact_imp_max_in_chain)
 apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
 done
diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Discrete.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -61,7 +61,7 @@
 qed
 
 instance discr :: (type) chfin
-apply (intro_classes, clarify)
+apply intro_classes
 apply (rule_tac x=0 in exI)
 apply (unfold max_in_chain_def)
 apply (clarify, erule discr_chain0 [symmetric])
diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -119,14 +119,14 @@
 qed
 
 instance "fun" :: (finite, chfin) chfin
-proof (intro_classes, clarify)
+proof
   fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
   let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
   assume "chain Y"
   hence "\<And>x. chain (\<lambda>i. Y i x)"
     by (rule ch2ch_fun)
   hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
-    by (rule chfin [rule_format])
+    by (rule chfin)
   hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
     by (rule LeastI_ex)
   hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -255,7 +255,7 @@
 axclass finite_po < finite, po
 
 axclass chfin < po
-  chfin: "\<forall>Y. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
+  chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
 
 axclass flat < pcpo
   ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
@@ -263,7 +263,7 @@
 text {* finite partial orders are chain-finite and directed-complete *}
 
 instance finite_po < chfin
-apply (intro_classes, clarify)
+apply intro_classes
 apply (drule finite_range_imp_finch)
 apply (rule finite)
 apply (simp add: finite_chain_def)
@@ -281,21 +281,17 @@
 
 text {* chfin types are cpo *}
 
-lemma chfin_imp_cpo:
-  "chain (S::nat \<Rightarrow> 'a::chfin) \<Longrightarrow> \<exists>x. range S <<| x"
-apply (frule chfin [rule_format])
+instance chfin < cpo
+apply intro_classes
+apply (frule chfin)
 apply (blast intro: lub_finch1)
 done
 
-instance chfin < cpo
-by intro_classes (rule chfin_imp_cpo)
-
 text {* flat types are chfin *}
 
 instance flat < chfin
 apply intro_classes
 apply (unfold max_in_chain_def)
-apply clarify
 apply (case_tac "\<forall>i. Y i = \<bottom>")
 apply simp
 apply simp
diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -80,14 +80,13 @@
   assumes type: "type_definition Rep Abs A"
     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   shows "OFCLASS('b, chfin_class)"
- apply (intro_classes, clarify)
+ apply intro_classes
  apply (drule ch2ch_Rep [OF less])
- apply (drule chfin [rule_format])
+ apply (drule chfin)
  apply (unfold max_in_chain_def)
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
-
 subsection {* Proving a subtype is complete *}
 
 text {*
diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Up.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -293,7 +293,7 @@
 by (safe elim!: compact_up compact_upD)
 
 instance u :: (chfin) chfin
-apply (intro_classes, clarify)
+apply intro_classes
 apply (erule compact_imp_max_in_chain)
 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
 done