--- 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
--- 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
--- 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)
--- 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))