author wenzelm Sun, 26 Feb 2012 18:26:26 +0100 changeset 46685 866a798d051c parent 46684 7f741b2c82a3 child 46686 b2ae19322ff8
tuned proofs;
 src/HOL/ex/CTL.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/CTL.thy	Sun Feb 26 18:25:28 2012 +0100
+++ b/src/HOL/ex/CTL.thy	Sun Feb 26 18:26:26 2012 +0100
@@ -4,7 +4,9 @@

-theory CTL imports Main begin
+theory CTL
+imports Main
+begin

text {*
We formalize basic concepts of Computational Tree Logic (CTL)
@@ -127,19 +129,19 @@

lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
proof -
-  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
+  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
qed

lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
proof -
-  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
qed

lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
proof -
-  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
+  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
qed

@@ -152,7 +154,7 @@

lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
proof -
-  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
qed
```