# HG changeset patch
# User huffman
# Date 1200278993 -3600
# Node ID 0eaadfa8889e21322540c5c98f4b28a4eb28e82b
# Parent  0ee6e01c5572e4857d272248941c8539ae9a377b
converted adm_all and adm_ball to rule_format; cleaned up

diff -r 0ee6e01c5572 -r 0eaadfa8889e src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Sun Jan 13 11:54:36 2008 +0100
+++ b/src/HOLCF/Adm.thy	Mon Jan 14 03:49:53 2008 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOLCF/Adm.thy
     ID:         $Id$
-    Author:     Franz Regensburger
+    Author:     Franz Regensburger and Brian Huffman
 *)
 
 header {* Admissibility and compactness *}
@@ -19,14 +19,14 @@
 
 lemma admI:
    "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
-by (unfold adm_def, fast)
+unfolding adm_def by fast
+
+lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
+unfolding adm_def by fast
 
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
 by (rule admI, erule spec)
 
-lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
-by (unfold adm_def, fast)
-
 text {* improved admissibility introduction *}
 
 lemma admI2:
@@ -41,7 +41,7 @@
 
 text {* for chain-finite (easy) types every formula is admissible *}
 
-lemma adm_max_in_chain: 
+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)
@@ -56,15 +56,12 @@
 lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
 by (fast elim: admD intro: admI)
 
-lemma adm_all: "\<forall>y. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
+lemma adm_all: "(\<And>y. adm (P y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
 by (fast intro: admI elim: admD)
 
-lemma adm_ball: "\<forall>y\<in>A. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P y x)"
+lemma adm_ball: "(\<And>y. y \<in> A \<Longrightarrow> adm (P y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P y x)"
 by (fast intro: admI elim: admD)
 
-lemmas adm_all2 = adm_all [rule_format]
-lemmas adm_ball2 = adm_ball [rule_format]
-
 text {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *}
 
 lemma adm_disj_lemma1: 
@@ -103,7 +100,7 @@
 apply (erule contrapos_pp)
 apply (clarsimp, rename_tac a b)
 apply (rule_tac x="max a b" in exI)
-apply (simp add: le_maxI1 le_maxI2)
+apply simp
 done
 
 lemma adm_disj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
@@ -216,7 +213,7 @@
 by (rule admI, drule spec, erule P, erule is_ub_thelub)
 
 lemmas adm_lemmas [simp] =
-  adm_not_free adm_conj adm_all2 adm_ball2 adm_disj adm_imp adm_iff
+  adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
   adm_less adm_eq adm_not_less
   adm_compact_not_less adm_compact_neq adm_neq_compact adm_not_UU
 
diff -r 0ee6e01c5572 -r 0eaadfa8889e src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Jan 13 11:54:36 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Jan 14 03:49:53 2008 +0100
@@ -13,7 +13,7 @@
 local
 
 val adm_impl_admw = @{thm adm_impl_admw};
-val adm_all2 = @{thm adm_all2};
+val adm_all = @{thm adm_all};
 val adm_conj = @{thm adm_conj};
 val adm_subst = @{thm adm_subst};
 val antisym_less_inverse = @{thm antisym_less_inverse};
@@ -897,7 +897,7 @@
           map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
           quant_tac 1,
           rtac (adm_impl_admw RS wfix_ind) 1,
-          REPEAT_DETERM (rtac adm_all2 1),
+          REPEAT_DETERM (rtac adm_all 1),
           REPEAT_DETERM (
             TRY (rtac adm_conj 1) THEN 
             rtac adm_subst 1 THEN 
diff -r 0ee6e01c5572 -r 0eaadfa8889e src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Sun Jan 13 11:54:36 2008 +0100
+++ b/src/HOLCF/ex/Hoare.thy	Mon Jan 14 03:49:53 2008 +0100
@@ -234,7 +234,6 @@
 lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
 apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
 apply (rule adm_all)
-apply (rule allI)
 apply (rule adm_eq)
 apply (tactic "cont_tacR 1")
 apply (rule allI)
@@ -259,7 +258,6 @@
 lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
 apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
 apply (rule adm_all)
-apply (rule allI)
 apply (rule adm_eq)
 apply (tactic "cont_tacR 1")
 apply (rule allI)
@@ -289,7 +287,6 @@
 lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
 apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
 apply (rule adm_all)
-apply (rule allI)
 apply (rule adm_eq)
 apply (tactic "cont_tacR 1")
 apply (rule allI)
diff -r 0ee6e01c5572 -r 0eaadfa8889e src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Sun Jan 13 11:54:36 2008 +0100
+++ b/src/HOLCF/ex/Loop.thy	Mon Jan 14 03:49:53 2008 +0100
@@ -138,7 +138,7 @@
     ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
 apply (simplesubst while_def2)
 apply (rule fix_ind)
-apply (rule allI [THEN adm_all])
+apply (rule adm_all)
 apply (rule adm_eq)
 apply (tactic "cont_tacR 1")
 apply (simp (no_asm))