change class axiom chfin to rule_format
authorhuffman
Thu Jan 17 00:51:20 2008 +0100 (2008-01-17)
changeset 259210ca392ab7f37
parent 25920 8df5eabda5f6
child 25922 cb04d05e95fb
change class axiom chfin to rule_format
src/HOLCF/Adm.thy
src/HOLCF/Cfun.thy
src/HOLCF/Cprod.thy
src/HOLCF/Discrete.thy
src/HOLCF/Ffun.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Adm.thy	Wed Jan 16 22:41:49 2008 +0100
     1.2 +++ b/src/HOLCF/Adm.thy	Thu Jan 17 00:51:20 2008 +0100
     1.3 @@ -41,12 +41,8 @@
     1.4  
     1.5  text {* for chain-finite (easy) types every formula is admissible *}
     1.6  
     1.7 -lemma adm_max_in_chain:
     1.8 -  "\<forall>Y. chain (Y::nat \<Rightarrow> 'a) \<longrightarrow> (\<exists>n. max_in_chain n Y)
     1.9 -    \<Longrightarrow> adm (P::'a \<Rightarrow> bool)"
    1.10 -by (auto simp add: adm_def maxinch_is_thelub)
    1.11 -
    1.12 -lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
    1.13 +lemma adm_chfin: "adm (P::'a::chfin \<Rightarrow> bool)"
    1.14 +by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
    1.15  
    1.16  subsection {* Admissibility of special formulae and propagation *}
    1.17  
     2.1 --- a/src/HOLCF/Cfun.thy	Wed Jan 16 22:41:49 2008 +0100
     2.2 +++ b/src/HOLCF/Cfun.thy	Thu Jan 17 00:51:20 2008 +0100
     2.3 @@ -404,7 +404,7 @@
     2.4      \<Longrightarrow> \<forall>Y::nat \<Rightarrow> 'b. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
     2.5  apply clarify
     2.6  apply (drule_tac f=g in chain_monofun)
     2.7 -apply (drule chfin [rule_format])
     2.8 +apply (drule chfin)
     2.9  apply (unfold max_in_chain_def)
    2.10  apply (simp add: injection_eq)
    2.11  done
     3.1 --- a/src/HOLCF/Cprod.thy	Wed Jan 16 22:41:49 2008 +0100
     3.2 +++ b/src/HOLCF/Cprod.thy	Thu Jan 17 00:51:20 2008 +0100
     3.3 @@ -306,7 +306,7 @@
     3.4  done
     3.5  
     3.6  instance "*" :: (chfin, chfin) chfin
     3.7 -apply (intro_classes, clarify)
     3.8 +apply intro_classes
     3.9  apply (erule compact_imp_max_in_chain)
    3.10  apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
    3.11  done
     4.1 --- a/src/HOLCF/Discrete.thy	Wed Jan 16 22:41:49 2008 +0100
     4.2 +++ b/src/HOLCF/Discrete.thy	Thu Jan 17 00:51:20 2008 +0100
     4.3 @@ -61,7 +61,7 @@
     4.4  qed
     4.5  
     4.6  instance discr :: (type) chfin
     4.7 -apply (intro_classes, clarify)
     4.8 +apply intro_classes
     4.9  apply (rule_tac x=0 in exI)
    4.10  apply (unfold max_in_chain_def)
    4.11  apply (clarify, erule discr_chain0 [symmetric])
     5.1 --- a/src/HOLCF/Ffun.thy	Wed Jan 16 22:41:49 2008 +0100
     5.2 +++ b/src/HOLCF/Ffun.thy	Thu Jan 17 00:51:20 2008 +0100
     5.3 @@ -119,14 +119,14 @@
     5.4  qed
     5.5  
     5.6  instance "fun" :: (finite, chfin) chfin
     5.7 -proof (intro_classes, clarify)
     5.8 +proof
     5.9    fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
    5.10    let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
    5.11    assume "chain Y"
    5.12    hence "\<And>x. chain (\<lambda>i. Y i x)"
    5.13      by (rule ch2ch_fun)
    5.14    hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
    5.15 -    by (rule chfin [rule_format])
    5.16 +    by (rule chfin)
    5.17    hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
    5.18      by (rule LeastI_ex)
    5.19    hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
     6.1 --- a/src/HOLCF/Pcpo.thy	Wed Jan 16 22:41:49 2008 +0100
     6.2 +++ b/src/HOLCF/Pcpo.thy	Thu Jan 17 00:51:20 2008 +0100
     6.3 @@ -255,7 +255,7 @@
     6.4  axclass finite_po < finite, po
     6.5  
     6.6  axclass chfin < po
     6.7 -  chfin: "\<forall>Y. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
     6.8 +  chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
     6.9  
    6.10  axclass flat < pcpo
    6.11    ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
    6.12 @@ -263,7 +263,7 @@
    6.13  text {* finite partial orders are chain-finite and directed-complete *}
    6.14  
    6.15  instance finite_po < chfin
    6.16 -apply (intro_classes, clarify)
    6.17 +apply intro_classes
    6.18  apply (drule finite_range_imp_finch)
    6.19  apply (rule finite)
    6.20  apply (simp add: finite_chain_def)
    6.21 @@ -281,21 +281,17 @@
    6.22  
    6.23  text {* chfin types are cpo *}
    6.24  
    6.25 -lemma chfin_imp_cpo:
    6.26 -  "chain (S::nat \<Rightarrow> 'a::chfin) \<Longrightarrow> \<exists>x. range S <<| x"
    6.27 -apply (frule chfin [rule_format])
    6.28 +instance chfin < cpo
    6.29 +apply intro_classes
    6.30 +apply (frule chfin)
    6.31  apply (blast intro: lub_finch1)
    6.32  done
    6.33  
    6.34 -instance chfin < cpo
    6.35 -by intro_classes (rule chfin_imp_cpo)
    6.36 -
    6.37  text {* flat types are chfin *}
    6.38  
    6.39  instance flat < chfin
    6.40  apply intro_classes
    6.41  apply (unfold max_in_chain_def)
    6.42 -apply clarify
    6.43  apply (case_tac "\<forall>i. Y i = \<bottom>")
    6.44  apply simp
    6.45  apply simp
     7.1 --- a/src/HOLCF/Pcpodef.thy	Wed Jan 16 22:41:49 2008 +0100
     7.2 +++ b/src/HOLCF/Pcpodef.thy	Thu Jan 17 00:51:20 2008 +0100
     7.3 @@ -80,14 +80,13 @@
     7.4    assumes type: "type_definition Rep Abs A"
     7.5      and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     7.6    shows "OFCLASS('b, chfin_class)"
     7.7 - apply (intro_classes, clarify)
     7.8 + apply intro_classes
     7.9   apply (drule ch2ch_Rep [OF less])
    7.10 - apply (drule chfin [rule_format])
    7.11 + apply (drule chfin)
    7.12   apply (unfold max_in_chain_def)
    7.13   apply (simp add: type_definition.Rep_inject [OF type])
    7.14  done
    7.15  
    7.16 -
    7.17  subsection {* Proving a subtype is complete *}
    7.18  
    7.19  text {*
     8.1 --- a/src/HOLCF/Up.thy	Wed Jan 16 22:41:49 2008 +0100
     8.2 +++ b/src/HOLCF/Up.thy	Thu Jan 17 00:51:20 2008 +0100
     8.3 @@ -293,7 +293,7 @@
     8.4  by (safe elim!: compact_up compact_upD)
     8.5  
     8.6  instance u :: (chfin) chfin
     8.7 -apply (intro_classes, clarify)
     8.8 +apply intro_classes
     8.9  apply (erule compact_imp_max_in_chain)
    8.10  apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
    8.11  done