tuned
authorwenzelm
Thu May 31 20:52:51 2001 +0200 (2001-05-31)
changeset 11355778c369559d9
parent 11354 9b80fe19407f
child 11356 8fbb19b84f94
tuned
src/HOL/CTL/CTL.thy
src/HOL/CTL/document/root.bib
src/HOL/CTL/document/root.tex
src/HOL/Library/Continuity.thy
src/HOL/Library/Nat_Infinity.thy
src/HOLCF/FOCUS/Buffer.ML
src/HOLCF/FOCUS/Buffer.thy
src/HOLCF/FOCUS/Buffer_adm.ML
src/HOLCF/FOCUS/Buffer_adm.thy
src/HOLCF/FOCUS/FOCUS.ML
src/HOLCF/FOCUS/FOCUS.thy
src/HOLCF/FOCUS/Fstream.ML
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/ROOT.ML
src/HOLCF/FOCUS/Stream_adm.ML
src/HOLCF/FOCUS/Stream_adm.thy
src/HOLCF/ex/Stream.ML
     1.1 --- a/src/HOL/CTL/CTL.thy	Thu May 31 18:28:23 2001 +0200
     1.2 +++ b/src/HOL/CTL/CTL.thy	Thu May 31 20:52:51 2001 +0200
     1.3 @@ -4,13 +4,16 @@
     1.4  section {* CTL formulae *}
     1.5  
     1.6  text {*
     1.7 -  \tweakskip By using the common technique of ``shallow embedding'', a
     1.8 -  CTL formula is identified with the corresponding set of states where
     1.9 -  it holds.  Consequently, CTL operations such as negation,
    1.10 -  conjunction, disjunction simply become complement, intersection,
    1.11 -  union of sets.  We only require a separate operation for
    1.12 -  implication, as point-wise inclusion is usually not encountered in
    1.13 -  plain set-theory.
    1.14 +  \tweakskip We formalize basic concepts of Computational Tree Logic
    1.15 +  (CTL) \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
    1.16 +  simply-typed set theory of HOL.
    1.17 +
    1.18 +  By using the common technique of ``shallow embedding'', a CTL
    1.19 +  formula is identified with the corresponding set of states where it
    1.20 +  holds.  Consequently, CTL operations such as negation, conjunction,
    1.21 +  disjunction simply become complement, intersection, union of sets.
    1.22 +  We only require a separate operation for implication, as point-wise
    1.23 +  inclusion is usually not encountered in plain set-theory.
    1.24  *}
    1.25  
    1.26  lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
    1.27 @@ -25,16 +28,16 @@
    1.28  
    1.29  
    1.30  text {*
    1.31 -  \smallskip The CTL path operators are more interesting; they are 
    1.32 -  based on an arbitrary, but fixed model @{text \<M>}, which is simply 
    1.33 -  a transition relation over states @{typ "'a"}. 
    1.34 +  \smallskip The CTL path operators are more interesting; they are
    1.35 +  based on an arbitrary, but fixed model @{text \<M>}, which is simply
    1.36 +  a transition relation over states @{typ "'a"}.
    1.37  *}
    1.38  
    1.39  consts model :: "('a \<times> 'a) set"    ("\<M>")
    1.40  
    1.41  text {*
    1.42 -  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken as
    1.43 -  primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
    1.44 +  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
    1.45 +  as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
    1.46    defined as derived ones.  The formula @{text "\<EX> p"} holds in a
    1.47    state @{term s}, iff there is a successor state @{term s'} (with
    1.48    respect to the model @{term \<M>}), such that @{term p} holds in
    1.49 @@ -55,8 +58,9 @@
    1.50    EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
    1.51  
    1.52  text {*
    1.53 -  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined 
    1.54 -  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text "\<EG>"}.
    1.55 +  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
    1.56 +  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
    1.57 +  "\<EG>"}.
    1.58  *}
    1.59  
    1.60  constdefs
    1.61 @@ -67,11 +71,11 @@
    1.62  lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
    1.63  
    1.64  
    1.65 -
    1.66  section {* Basic fixed point properties *}
    1.67  
    1.68  text {*
    1.69 -  \tweakskip First of all, we use the de-Morgan property of fixed points
    1.70 +  \tweakskip First of all, we use the de-Morgan property of fixed
    1.71 +  points
    1.72  *}
    1.73  
    1.74  lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
    1.75 @@ -131,7 +135,6 @@
    1.76    then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
    1.77  qed
    1.78  
    1.79 -
    1.80  text {*
    1.81    From the greatest fixed point definition of @{term "\<AG> p"}, we
    1.82    derive as a consequence of the Knaster-Tarski theorem on the one
    1.83 @@ -141,8 +144,8 @@
    1.84  
    1.85  lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
    1.86  proof -
    1.87 -  have "mono (\<lambda>s. p \<inter> \<AX> s)" sorry (* by rule (auto simp add: AX_def EX_def) *)
    1.88 -  then show ?thesis sorry (* by (simp only: AG_gfp) (rule gfp_unfold) *)
    1.89 +  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
    1.90 +  then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
    1.91  qed
    1.92  
    1.93  text {*
    1.94 @@ -188,7 +191,8 @@
    1.95  
    1.96  lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
    1.97  lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
    1.98 -lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q" by (simp only: AG_gfp, rule gfp_mono) auto 
    1.99 +lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
   1.100 +  by (simp only: AG_gfp, rule gfp_mono) auto 
   1.101  
   1.102  text {*
   1.103    The formula @{term "AG p"} implies @{term "AX p"} (we use
   1.104 @@ -221,15 +225,14 @@
   1.105  qed
   1.106  
   1.107  text {*
   1.108 -  \smallskip We now give an alternative characterization of the
   1.109 -  @{text "\<AG>"} operator, which describes the @{text "\<AG>"}
   1.110 -  operator in an ``operational'' way by tree induction:
   1.111 -  In a state holds @{term "AG p"} iff
   1.112 -  in that state holds @{term p}, and in all reachable states @{term s}
   1.113 -  follows from the fact that @{term p} holds in @{term s}, that @{term
   1.114 -  p} also holds in all successor states of @{term s}.  We use the
   1.115 -  co-induction principle @{thm [source] AG_I} to establish this in a
   1.116 -  purely algebraic manner.
   1.117 +  \smallskip We now give an alternative characterization of the @{text
   1.118 +  "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
   1.119 +  an ``operational'' way by tree induction: In a state holds @{term
   1.120 +  "AG p"} iff in that state holds @{term p}, and in all reachable
   1.121 +  states @{term s} follows from the fact that @{term p} holds in
   1.122 +  @{term s}, that @{term p} also holds in all successor states of
   1.123 +  @{term s}.  We use the co-induction principle @{thm [source] AG_I}
   1.124 +  to establish this in a purely algebraic manner.
   1.125  *}
   1.126  
   1.127  theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/CTL/document/root.bib	Thu May 31 20:52:51 2001 +0200
     2.3 @@ -0,0 +1,13 @@
     2.4 +
     2.5 +@Misc{McMillan-LectureNotes,
     2.6 +  author =	 {Ken McMillan},
     2.7 +  title =	 {Lecture notes on verification of digital and hybrid systems},
     2.8 +  note =	 {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
     2.9 +}
    2.10 +
    2.11 +@PhdThesis{McMillan-PhDThesis,
    2.12 +  author = 	 {Ken McMillan},
    2.13 +  title = 	 {Symbolic Model Checking: an approach to the state explosion problem},
    2.14 +  school = 	 {Carnegie Mellon University},
    2.15 +  year = 	 1992
    2.16 +}
     3.1 --- a/src/HOL/CTL/document/root.tex	Thu May 31 18:28:23 2001 +0200
     3.2 +++ b/src/HOL/CTL/document/root.tex	Thu May 31 20:52:51 2001 +0200
     3.3 @@ -2,6 +2,9 @@
     3.4  \documentclass[11pt,a4paper]{article}
     3.5  \usepackage{isabelle,isabellesym,pdfsetup}
     3.6  
     3.7 +\urlstyle{rm}
     3.8 +\isabellestyle{it}
     3.9 +
    3.10  \newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
    3.11  \newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
    3.12  \newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
    3.13 @@ -9,15 +12,13 @@
    3.14  \newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
    3.15  \newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
    3.16  
    3.17 -%for best-style documents ...
    3.18 -\urlstyle{rm}
    3.19 -\isabellestyle{it}
    3.20  
    3.21  \begin{document}
    3.22  
    3.23 -\title{A short case study on CTL}
    3.24 +\title{Some properties of CTL}
    3.25  \author{Gertrud Bauer}
    3.26  \maketitle
    3.27 +
    3.28  \tableofcontents
    3.29  \bigskip
    3.30  
    3.31 @@ -26,7 +27,7 @@
    3.32  
    3.33  \input{session}
    3.34  
    3.35 -%\bibliographystyle{plain}
    3.36 -%\bibliography{root}
    3.37 +\bibliographystyle{abbrv}
    3.38 +\bibliography{root}
    3.39  
    3.40  \end{document}
     4.1 --- a/src/HOL/Library/Continuity.thy	Thu May 31 18:28:23 2001 +0200
     4.2 +++ b/src/HOL/Library/Continuity.thy	Thu May 31 20:52:51 2001 +0200
     4.3 @@ -1,219 +1,222 @@
     4.4  (*  Title:      HOL/Library/Continuity.thy
     4.5 -    ID:         $$
     4.6 -    Author: 	David von Oheimb, TU Muenchen
     4.7 +    ID:         $Id$
     4.8 +    Author:     David von Oheimb, TU Muenchen
     4.9      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    4.10 -
    4.11  *)
    4.12  
    4.13  header {*
    4.14 -  \title{Continuity and interations (of set transformers)}
    4.15 +  \title{Continuity and iterations (of set transformers)}
    4.16    \author{David von Oheimb}
    4.17  *}
    4.18  
    4.19 -theory Continuity = Relation_Power:
    4.20 -
    4.21 +theory Continuity = Main:
    4.22  
    4.23  subsection "Chains"
    4.24  
    4.25  constdefs
    4.26 -  up_chain      :: "(nat => 'a set) => bool"
    4.27 - "up_chain F      == !i. F i <= F (Suc i)"
    4.28 +  up_chain :: "(nat => 'a set) => bool"
    4.29 +  "up_chain F == \<forall>i. F i \<subseteq> F (Suc i)"
    4.30  
    4.31 -lemma up_chainI: "(!!i. F i <= F (Suc i)) ==> up_chain F"
    4.32 -by (simp add: up_chain_def);
    4.33 +lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
    4.34 +  by (simp add: up_chain_def)
    4.35  
    4.36 -lemma up_chainD: "up_chain F ==> F i <= F (Suc i)"
    4.37 -by (simp add: up_chain_def);
    4.38 +lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
    4.39 +  by (simp add: up_chain_def)
    4.40  
    4.41 -lemma up_chain_less_mono [rule_format]: "up_chain F ==> x < y --> F x <= F y"
    4.42 -apply (induct_tac y)
    4.43 -apply (blast dest: up_chainD elim: less_SucE)+
    4.44 -done
    4.45 +lemma up_chain_less_mono [rule_format]:
    4.46 +    "up_chain F ==> x < y --> F x \<subseteq> F y"
    4.47 +  apply (induct_tac y)
    4.48 +  apply (blast dest: up_chainD elim: less_SucE)+
    4.49 +  done
    4.50  
    4.51 -lemma up_chain_mono: "up_chain F ==> x <= y ==> F x <= F y"
    4.52 -apply (drule le_imp_less_or_eq)
    4.53 -apply (blast dest: up_chain_less_mono)
    4.54 -done
    4.55 +lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
    4.56 +  apply (drule le_imp_less_or_eq)
    4.57 +  apply (blast dest: up_chain_less_mono)
    4.58 +  done
    4.59  
    4.60  
    4.61  constdefs
    4.62 -  down_chain      :: "(nat => 'a set) => bool"
    4.63 - "down_chain F == !i. F (Suc i) <= F i"
    4.64 +  down_chain :: "(nat => 'a set) => bool"
    4.65 +  "down_chain F == \<forall>i. F (Suc i) \<subseteq> F i"
    4.66  
    4.67 -lemma down_chainI: "(!!i. F (Suc i) <= F i) ==> down_chain F"
    4.68 -by (simp add: down_chain_def);
    4.69 +lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
    4.70 +  by (simp add: down_chain_def)
    4.71  
    4.72 -lemma down_chainD: "down_chain F ==> F (Suc i) <= F i"
    4.73 -by (simp add: down_chain_def);
    4.74 +lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
    4.75 +  by (simp add: down_chain_def)
    4.76  
    4.77 -lemma down_chain_less_mono[rule_format]: "down_chain F ==> x < y --> F y <= F x"
    4.78 -apply (induct_tac y)
    4.79 -apply (blast dest: down_chainD elim: less_SucE)+
    4.80 -done
    4.81 +lemma down_chain_less_mono [rule_format]:
    4.82 +    "down_chain F ==> x < y --> F y \<subseteq> F x"
    4.83 +  apply (induct_tac y)
    4.84 +  apply (blast dest: down_chainD elim: less_SucE)+
    4.85 +  done
    4.86  
    4.87 -lemma down_chain_mono: "down_chain F ==> x <= y ==> F y <= F x"
    4.88 -apply (drule le_imp_less_or_eq)
    4.89 -apply (blast dest: down_chain_less_mono)
    4.90 -done
    4.91 +lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
    4.92 +  apply (drule le_imp_less_or_eq)
    4.93 +  apply (blast dest: down_chain_less_mono)
    4.94 +  done
    4.95  
    4.96  
    4.97  subsection "Continuity"
    4.98  
    4.99  constdefs
   4.100    up_cont :: "('a set => 'a set) => bool"
   4.101 - "up_cont f == !F. up_chain F --> f (Union (range F)) = Union (f`(range F))"
   4.102 +  "up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)"
   4.103  
   4.104 -lemma up_contI: 
   4.105 - "(!!F. up_chain F ==> f (Union (range F)) = Union (f`(range F))) ==> up_cont f"
   4.106 -apply (unfold up_cont_def)
   4.107 -by blast
   4.108 +lemma up_contI:
   4.109 +    "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
   4.110 +  apply (unfold up_cont_def)
   4.111 +  apply blast
   4.112 +  done
   4.113  
   4.114 -lemma up_contD: 
   4.115 -  "[| up_cont f; up_chain F |] ==> f (Union (range F)) = Union (f`(range F))"
   4.116 -apply (unfold up_cont_def)
   4.117 -by auto
   4.118 +lemma up_contD:
   4.119 +    "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
   4.120 +  apply (unfold up_cont_def)
   4.121 +  apply auto
   4.122 +  done
   4.123  
   4.124  
   4.125  lemma up_cont_mono: "up_cont f ==> mono f"
   4.126 -apply (rule monoI)
   4.127 -apply (drule_tac F = "%i. if i = 0 then A else B" in up_contD)
   4.128 -apply  (rule up_chainI)
   4.129 -apply  simp+
   4.130 -apply (drule Un_absorb1)
   4.131 -apply auto
   4.132 -done
   4.133 +  apply (rule monoI)
   4.134 +  apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
   4.135 +   apply (rule up_chainI)
   4.136 +   apply  simp+
   4.137 +  apply (drule Un_absorb1)
   4.138 +  apply auto
   4.139 +  done
   4.140  
   4.141  
   4.142  constdefs
   4.143    down_cont :: "('a set => 'a set) => bool"
   4.144 - "down_cont f == !F. down_chain F --> f (Inter (range F)) = Inter (f`(range F))"
   4.145 +  "down_cont f ==
   4.146 +    \<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)"
   4.147  
   4.148 -lemma down_contI: 
   4.149 - "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f`(range F))) ==> 
   4.150 -  down_cont f"
   4.151 -apply (unfold down_cont_def)
   4.152 -by blast
   4.153 +lemma down_contI:
   4.154 +  "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
   4.155 +    down_cont f"
   4.156 +  apply (unfold down_cont_def)
   4.157 +  apply blast
   4.158 +  done
   4.159  
   4.160 -lemma down_contD: "[| down_cont f; down_chain F |] ==> 
   4.161 -  f (Inter (range F)) = Inter (f`(range F))"
   4.162 -apply (unfold down_cont_def)
   4.163 -by auto
   4.164 +lemma down_contD: "down_cont f ==> down_chain F ==>
   4.165 +    f (Inter (range F)) = Inter (f ` range F)"
   4.166 +  apply (unfold down_cont_def)
   4.167 +  apply auto
   4.168 +  done
   4.169  
   4.170  lemma down_cont_mono: "down_cont f ==> mono f"
   4.171 -apply (rule monoI)
   4.172 -apply (drule_tac F = "%i. if i = 0 then B else A" in down_contD)
   4.173 -apply  (rule down_chainI)
   4.174 -apply  simp+
   4.175 -apply (drule Int_absorb1)
   4.176 -apply auto
   4.177 -done
   4.178 +  apply (rule monoI)
   4.179 +  apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
   4.180 +   apply (rule down_chainI)
   4.181 +   apply simp+
   4.182 +  apply (drule Int_absorb1)
   4.183 +  apply auto
   4.184 +  done
   4.185  
   4.186  
   4.187  subsection "Iteration"
   4.188  
   4.189  constdefs
   4.190 -
   4.191    up_iterate :: "('a set => 'a set) => nat => 'a set"
   4.192 - "up_iterate f n == (f^n) {}"
   4.193 +  "up_iterate f n == (f^n) {}"
   4.194  
   4.195  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   4.196 -by (simp add: up_iterate_def)
   4.197 +  by (simp add: up_iterate_def)
   4.198  
   4.199 -lemma up_iterate_Suc [simp]: 
   4.200 -  "up_iterate f (Suc i) = f (up_iterate f i)"
   4.201 -by (simp add: up_iterate_def)
   4.202 +lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)"
   4.203 +  by (simp add: up_iterate_def)
   4.204  
   4.205  lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
   4.206 -apply (rule up_chainI)
   4.207 -apply (induct_tac i)
   4.208 -apply simp+
   4.209 -apply (erule (1) monoD)
   4.210 -done
   4.211 +  apply (rule up_chainI)
   4.212 +  apply (induct_tac i)
   4.213 +   apply simp+
   4.214 +  apply (erule (1) monoD)
   4.215 +  done
   4.216  
   4.217 -lemma UNION_up_iterate_is_fp: 
   4.218 -"up_cont F ==> F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
   4.219 -apply (frule up_cont_mono [THEN up_iterate_chain])
   4.220 -apply (drule (1) up_contD)
   4.221 -apply simp
   4.222 -apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
   4.223 -apply (case_tac "xa")
   4.224 -apply auto
   4.225 -done
   4.226 +lemma UNION_up_iterate_is_fp:
   4.227 +  "up_cont F ==>
   4.228 +    F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
   4.229 +  apply (frule up_cont_mono [THEN up_iterate_chain])
   4.230 +  apply (drule (1) up_contD)
   4.231 +  apply simp
   4.232 +  apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
   4.233 +  apply (case_tac xa)
   4.234 +   apply auto
   4.235 +  done
   4.236  
   4.237 -lemma UNION_up_iterate_lowerbound: 
   4.238 -"[| mono F; F P = P |] ==> UNION UNIV (up_iterate F) <= P"
   4.239 -apply (subgoal_tac "(!!i. up_iterate F i <= P)")
   4.240 -apply  fast
   4.241 -apply (induct_tac "i")
   4.242 -prefer 2 apply (drule (1) monoD)
   4.243 -apply auto
   4.244 -done
   4.245 +lemma UNION_up_iterate_lowerbound:
   4.246 +    "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P"
   4.247 +  apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)")
   4.248 +   apply fast
   4.249 +  apply (induct_tac i)
   4.250 +  prefer 2 apply (drule (1) monoD)
   4.251 +   apply auto
   4.252 +  done
   4.253  
   4.254 -lemma UNION_up_iterate_is_lfp: 
   4.255 -  "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
   4.256 -apply (rule set_eq_subset [THEN iffD2])
   4.257 -apply (rule conjI)
   4.258 -prefer 2
   4.259 -apply  (drule up_cont_mono)
   4.260 -apply  (rule UNION_up_iterate_lowerbound)
   4.261 -apply   assumption
   4.262 -apply  (erule lfp_unfold [symmetric])
   4.263 -apply (rule lfp_lowerbound)
   4.264 -apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   4.265 -apply (erule UNION_up_iterate_is_fp [symmetric])
   4.266 -done
   4.267 +lemma UNION_up_iterate_is_lfp:
   4.268 +    "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
   4.269 +  apply (rule set_eq_subset [THEN iffD2])
   4.270 +  apply (rule conjI)
   4.271 +   prefer 2
   4.272 +   apply (drule up_cont_mono)
   4.273 +   apply (rule UNION_up_iterate_lowerbound)
   4.274 +    apply assumption
   4.275 +   apply (erule lfp_unfold [symmetric])
   4.276 +  apply (rule lfp_lowerbound)
   4.277 +  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   4.278 +  apply (erule UNION_up_iterate_is_fp [symmetric])
   4.279 +  done
   4.280  
   4.281  
   4.282  constdefs
   4.283 -
   4.284    down_iterate :: "('a set => 'a set) => nat => 'a set"
   4.285 - "down_iterate f n == (f^n) UNIV"
   4.286 +  "down_iterate f n == (f^n) UNIV"
   4.287  
   4.288  lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   4.289 -by (simp add: down_iterate_def)
   4.290 +  by (simp add: down_iterate_def)
   4.291  
   4.292 -lemma down_iterate_Suc [simp]: 
   4.293 -  "down_iterate f (Suc i) = f (down_iterate f i)"
   4.294 -by (simp add: down_iterate_def)
   4.295 +lemma down_iterate_Suc [simp]:
   4.296 +    "down_iterate f (Suc i) = f (down_iterate f i)"
   4.297 +  by (simp add: down_iterate_def)
   4.298  
   4.299  lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
   4.300 -apply (rule down_chainI)
   4.301 -apply (induct_tac i)
   4.302 -apply simp+
   4.303 -apply (erule (1) monoD)
   4.304 -done
   4.305 +  apply (rule down_chainI)
   4.306 +  apply (induct_tac i)
   4.307 +   apply simp+
   4.308 +  apply (erule (1) monoD)
   4.309 +  done
   4.310  
   4.311 -lemma INTER_down_iterate_is_fp: 
   4.312 -"down_cont F ==> 
   4.313 - F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
   4.314 -apply (frule down_cont_mono [THEN down_iterate_chain])
   4.315 -apply (drule (1) down_contD)
   4.316 -apply simp
   4.317 -apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
   4.318 -apply (case_tac "xa")
   4.319 -apply auto
   4.320 -done
   4.321 +lemma INTER_down_iterate_is_fp:
   4.322 +  "down_cont F ==>
   4.323 +    F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
   4.324 +  apply (frule down_cont_mono [THEN down_iterate_chain])
   4.325 +  apply (drule (1) down_contD)
   4.326 +  apply simp
   4.327 +  apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
   4.328 +  apply (case_tac xa)
   4.329 +   apply auto
   4.330 +  done
   4.331  
   4.332 -lemma INTER_down_iterate_upperbound: 
   4.333 -"[| mono F; F P = P |] ==> P <= INTER UNIV (down_iterate F)"
   4.334 -apply (subgoal_tac "(!!i. P <= down_iterate F i)")
   4.335 -apply  fast
   4.336 -apply (induct_tac "i")
   4.337 -prefer 2 apply (drule (1) monoD)
   4.338 -apply auto
   4.339 -done
   4.340 +lemma INTER_down_iterate_upperbound:
   4.341 +    "mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)"
   4.342 +  apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)")
   4.343 +   apply fast
   4.344 +  apply (induct_tac i)
   4.345 +  prefer 2 apply (drule (1) monoD)
   4.346 +   apply auto
   4.347 +  done
   4.348  
   4.349 -lemma INTER_down_iterate_is_gfp: 
   4.350 -  "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
   4.351 -apply (rule set_eq_subset [THEN iffD2])
   4.352 -apply (rule conjI)
   4.353 -apply  (drule down_cont_mono)
   4.354 -apply  (rule INTER_down_iterate_upperbound)
   4.355 -apply   assumption
   4.356 -apply  (erule gfp_unfold [symmetric])
   4.357 -apply (rule gfp_upperbound)
   4.358 -apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   4.359 -apply (erule INTER_down_iterate_is_fp)
   4.360 -done
   4.361 +lemma INTER_down_iterate_is_gfp:
   4.362 +    "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
   4.363 +  apply (rule set_eq_subset [THEN iffD2])
   4.364 +  apply (rule conjI)
   4.365 +   apply (drule down_cont_mono)
   4.366 +   apply (rule INTER_down_iterate_upperbound)
   4.367 +    apply assumption
   4.368 +   apply (erule gfp_unfold [symmetric])
   4.369 +  apply (rule gfp_upperbound)
   4.370 +  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   4.371 +  apply (erule INTER_down_iterate_is_fp)
   4.372 +  done
   4.373  
   4.374  end
     5.1 --- a/src/HOL/Library/Nat_Infinity.thy	Thu May 31 18:28:23 2001 +0200
     5.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Thu May 31 20:52:51 2001 +0200
     5.3 @@ -1,8 +1,7 @@
     5.4 -(*  Title: 	HOL/Library/Nat_Infinity.thy
     5.5 -    ID:         $ $
     5.6 -    Author: 	David von Oheimb, TU Muenchen
     5.7 +(*  Title:      HOL/Library/Nat_Infinity.thy
     5.8 +    ID:         $Id$
     5.9 +    Author:     David von Oheimb, TU Muenchen
    5.10      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    5.11 -
    5.12  *)
    5.13  
    5.14  header {*
    5.15 @@ -10,14 +9,14 @@
    5.16    \author{David von Oheimb}
    5.17  *}
    5.18  
    5.19 -theory Nat_Infinity = Datatype:
    5.20 +theory Nat_Infinity = Main:
    5.21  
    5.22  subsection "Definitions"
    5.23  
    5.24  text {*
    5.25 - We extend the standard natural numbers by a special value indicating infinity.
    5.26 - This includes extending the ordering relations @{term "op <"} and 
    5.27 - @{term "op <="}.
    5.28 +  We extend the standard natural numbers by a special value indicating
    5.29 +  infinity.  This includes extending the ordering relations @{term "op
    5.30 +  <"} and @{term "op \<le>"}.
    5.31  *}
    5.32  
    5.33  datatype inat = Fin nat | Infty
    5.34 @@ -26,191 +25,159 @@
    5.35  instance inat :: zero ..
    5.36  
    5.37  consts
    5.38 -
    5.39 -  iSuc	:: "inat => inat"
    5.40 +  iSuc :: "inat => inat"
    5.41  
    5.42  syntax (xsymbols)
    5.43 -
    5.44 -  Infty		:: inat					("\<infinity>")
    5.45 +  Infty :: inat    ("\<infinity>")
    5.46  
    5.47  defs
    5.48 -
    5.49 -  iZero_def:	"0      == Fin 0"
    5.50 -  iSuc_def:	"iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    5.51 -  iless_def:	"m < n  == case m of Fin m1 => (case n of Fin n1 => m1 < n1 
    5.52 -						             | \<infinity> => True)
    5.53 -				   | \<infinity>  => False "
    5.54 -  ile_def:	"(m::inat) <= n == \<not>(n<m)"
    5.55 +  iZero_def: "0 == Fin 0"
    5.56 +  iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    5.57 +  iless_def: "m < n ==
    5.58 +    case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
    5.59 +    | \<infinity>  => False"
    5.60 +  ile_def: "(m::inat) \<le> n == \<not> (n < m)"
    5.61  
    5.62  lemmas inat_defs = iZero_def iSuc_def iless_def ile_def
    5.63  lemmas inat_splits = inat.split inat.split_asm
    5.64  
    5.65 -
    5.66 -text {* Below is a not quite complete set of theorems. Use
    5.67 -@{text "apply(simp add:inat_defs split:inat_splits, arith?)"}
    5.68 -to prove new theorems or solve arithmetic subgoals involving @{typ inat} 
    5.69 -on the fly.
    5.70 +text {*
    5.71 +  Below is a not quite complete set of theorems.  Use method @{text
    5.72 +  "(simp add: inat_defs split:inat_splits, arith?)"} to prove new
    5.73 +  theorems or solve arithmetic subgoals involving @{typ inat} on the
    5.74 +  fly.
    5.75  *}
    5.76  
    5.77  subsection "Constructors"
    5.78  
    5.79  lemma Fin_0: "Fin 0 = 0"
    5.80 -by(simp add:inat_defs split:inat_splits, arith?)
    5.81 +  by (simp add:inat_defs split:inat_splits, arith?)
    5.82  
    5.83  lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    5.84 -by(simp add:inat_defs split:inat_splits, arith?)
    5.85 +  by (simp add:inat_defs split:inat_splits, arith?)
    5.86  
    5.87  lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    5.88 -by(simp add:inat_defs split:inat_splits, arith?)
    5.89 +  by (simp add:inat_defs split:inat_splits, arith?)
    5.90  
    5.91  lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
    5.92 -by(simp add:inat_defs split:inat_splits, arith?)
    5.93 +  by (simp add:inat_defs split:inat_splits, arith?)
    5.94  
    5.95  lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
    5.96 -by(simp add:inat_defs split:inat_splits, arith?)
    5.97 +  by (simp add:inat_defs split:inat_splits, arith?)
    5.98  
    5.99  lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
   5.100 -by(simp add:inat_defs split:inat_splits, arith?)
   5.101 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.102  
   5.103  lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
   5.104 -by(simp add:inat_defs split:inat_splits, arith?)
   5.105 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.106  
   5.107  
   5.108  subsection "Ordering relations"
   5.109  
   5.110  lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
   5.111 -by(simp add:inat_defs split:inat_splits, arith?)
   5.112 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.113  
   5.114 -lemma iless_linear: "m < n | m = n | n < (m::inat)"
   5.115 -by(simp add:inat_defs split:inat_splits, arith?)
   5.116 +lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
   5.117 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.118  
   5.119  lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
   5.120 -by(simp add:inat_defs split:inat_splits, arith?)
   5.121 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.122  
   5.123  lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
   5.124 -by(simp add:inat_defs split:inat_splits, arith?)
   5.125 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.126  
   5.127  lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
   5.128 -by(simp add:inat_defs split:inat_splits, arith?)
   5.129 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.130  
   5.131  lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
   5.132 -by(simp add:inat_defs split:inat_splits, arith?)
   5.133 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.134  
   5.135  lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
   5.136 -by(simp add:inat_defs split:inat_splits, arith?)
   5.137 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.138  
   5.139  lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
   5.140 -by(simp add:inat_defs split:inat_splits, arith?)
   5.141 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.142  
   5.143  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
   5.144 -by(simp add:inat_defs split:inat_splits, arith?)
   5.145 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.146  
   5.147  lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   5.148 -by(simp add:inat_defs split:inat_splits, arith?)
   5.149 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.150  
   5.151  lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
   5.152 -by(simp add:inat_defs split:inat_splits, arith?)
   5.153 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.154  
   5.155  lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
   5.156 -by(simp add:inat_defs split:inat_splits, arith?)
   5.157 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.158  
   5.159  lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
   5.160 -by(simp add:inat_defs split:inat_splits, arith?)
   5.161 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.162  
   5.163  
   5.164  (* ----------------------------------------------------------------------- *)
   5.165  
   5.166 -lemma ile_def2: "m <= n = (m < n | m = (n::inat))"
   5.167 -by(simp add:inat_defs split:inat_splits, arith?)
   5.168 +lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))"
   5.169 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.170  
   5.171 -lemma ile_refl [simp]: "n <= (n::inat)"
   5.172 -by(simp add:inat_defs split:inat_splits, arith?)
   5.173 +lemma ile_refl [simp]: "n \<le> (n::inat)"
   5.174 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.175  
   5.176 -lemma ile_trans: "i <= j ==> j <= k ==> i <= (k::inat)"
   5.177 -by(simp add:inat_defs split:inat_splits, arith?)
   5.178 +lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
   5.179 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.180  
   5.181 -lemma ile_iless_trans: "i <= j ==> j < k ==> i < (k::inat)"
   5.182 -by(simp add:inat_defs split:inat_splits, arith?)
   5.183 +lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
   5.184 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.185  
   5.186 -lemma iless_ile_trans: "i < j ==> j <= k ==> i < (k::inat)"
   5.187 -by(simp add:inat_defs split:inat_splits, arith?)
   5.188 +lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
   5.189 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.190  
   5.191 -lemma Infty_ub [simp]: "n <= \<infinity>"
   5.192 -by(simp add:inat_defs split:inat_splits, arith?)
   5.193 +lemma Infty_ub [simp]: "n \<le> \<infinity>"
   5.194 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.195  
   5.196 -lemma i0_lb [simp]: "(0::inat) <= n"
   5.197 -by(simp add:inat_defs split:inat_splits, arith?)
   5.198 +lemma i0_lb [simp]: "(0::inat) \<le> n"
   5.199 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.200  
   5.201 -lemma Infty_ileE [elim!]: "\<infinity> <= Fin m ==> R"
   5.202 -by(simp add:inat_defs split:inat_splits, arith?)
   5.203 +lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
   5.204 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.205  
   5.206 -lemma Fin_ile_mono [simp]: "(Fin n <= Fin m) = (n <= m)"
   5.207 -by(simp add:inat_defs split:inat_splits, arith?)
   5.208 +lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
   5.209 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.210  
   5.211 -lemma ilessI1: "n <= m ==> n \<noteq> m ==> n < (m::inat)"
   5.212 -by(simp add:inat_defs split:inat_splits, arith?)
   5.213 +lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
   5.214 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.215  
   5.216 -lemma ileI1: "m < n ==> iSuc m <= n"
   5.217 -by(simp add:inat_defs split:inat_splits, arith?)
   5.218 +lemma ileI1: "m < n ==> iSuc m \<le> n"
   5.219 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.220  
   5.221 -lemma Suc_ile_eq: "Fin (Suc m) <= n = (Fin m < n)"
   5.222 -by(simp add:inat_defs split:inat_splits, arith?)
   5.223 +lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)"
   5.224 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.225  
   5.226 -lemma iSuc_ile_mono [simp]: "iSuc n <= iSuc m = (n <= m)"
   5.227 -by(simp add:inat_defs split:inat_splits, arith?)
   5.228 +lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)"
   5.229 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.230  
   5.231 -lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m <= n)"
   5.232 -by(simp add:inat_defs split:inat_splits, arith?)
   5.233 +lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)"
   5.234 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.235  
   5.236 -lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n <= 0"
   5.237 -by(simp add:inat_defs split:inat_splits, arith?)
   5.238 +lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   5.239 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.240  
   5.241 -lemma ile_iSuc [simp]: "n <= iSuc n"
   5.242 -by(simp add:inat_defs split:inat_splits, arith?)
   5.243 +lemma ile_iSuc [simp]: "n \<le> iSuc n"
   5.244 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.245  
   5.246 -lemma Fin_ile: "n <= Fin m ==> \<exists>k. n = Fin k"
   5.247 -by(simp add:inat_defs split:inat_splits, arith?)
   5.248 +lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
   5.249 +  by (simp add:inat_defs split:inat_splits, arith?)
   5.250  
   5.251  lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   5.252 -apply (induct_tac "k")
   5.253 -apply  (simp (no_asm) only: Fin_0)
   5.254 -apply  (fast intro: ile_iless_trans i0_lb)
   5.255 -apply (erule exE)
   5.256 -apply (drule spec)
   5.257 -apply (erule exE)
   5.258 -apply (drule ileI1)
   5.259 -apply (rule iSuc_Fin [THEN subst])
   5.260 -apply (rule exI)
   5.261 -apply (erule (1) ile_iless_trans)
   5.262 -done
   5.263 -
   5.264 -ML {*
   5.265 -val Fin_0 = thm "Fin_0";
   5.266 -val Suc_ile_eq = thm "Suc_ile_eq";
   5.267 -val iSuc_Fin = thm "iSuc_Fin";
   5.268 -val iSuc_Infty = thm "iSuc_Infty";
   5.269 -val iSuc_mono = thm "iSuc_mono";
   5.270 -val iSuc_ile_mono = thm "iSuc_ile_mono";
   5.271 -val not_iSuc_ilei0=thm "not_iSuc_ilei0";
   5.272 -val iSuc_inject = thm "iSuc_inject";
   5.273 -val i0_iless_iSuc = thm "i0_iless_iSuc";
   5.274 -val i0_eq = thm "i0_eq";
   5.275 -val i0_lb = thm "i0_lb";
   5.276 -val ile_def = thm "ile_def";
   5.277 -val ile_refl = thm "ile_refl";
   5.278 -val Infty_ub = thm "Infty_ub";
   5.279 -val ilessI1 = thm "ilessI1";
   5.280 -val ile_iless_trans = thm "ile_iless_trans";
   5.281 -val ile_trans = thm "ile_trans";
   5.282 -val ileI1 = thm "ileI1";
   5.283 -val ile_iSuc = thm "ile_iSuc";
   5.284 -val Fin_iless_Infty = thm "Fin_iless_Infty";
   5.285 -val Fin_ile_mono = thm "Fin_ile_mono";
   5.286 -val chain_incr = thm "chain_incr";
   5.287 -val Infty_eq = thm "Infty_eq";
   5.288 -*}
   5.289 +  apply (induct_tac k)
   5.290 +   apply (simp (no_asm) only: Fin_0)
   5.291 +   apply (fast intro: ile_iless_trans i0_lb)
   5.292 +  apply (erule exE)
   5.293 +  apply (drule spec)
   5.294 +  apply (erule exE)
   5.295 +  apply (drule ileI1)
   5.296 +  apply (rule iSuc_Fin [THEN subst])
   5.297 +  apply (rule exI)
   5.298 +  apply (erule (1) ile_iless_trans)
   5.299 +  done
   5.300  
   5.301  end
   5.302 -
   5.303 -
   5.304 -
     6.1 --- a/src/HOLCF/FOCUS/Buffer.ML	Thu May 31 18:28:23 2001 +0200
     6.2 +++ b/src/HOLCF/FOCUS/Buffer.ML	Thu May 31 20:52:51 2001 +0200
     6.3 @@ -1,5 +1,5 @@
     6.4  (*  Title: 	HOLCF/FOCUS/Buffer.ML
     6.5 -    ID:         $ $
     6.6 +    ID:         $Id$
     6.7      Author: 	David von Oheimb, TU Muenchen
     6.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.9  *)
     7.1 --- a/src/HOLCF/FOCUS/Buffer.thy	Thu May 31 18:28:23 2001 +0200
     7.2 +++ b/src/HOLCF/FOCUS/Buffer.thy	Thu May 31 20:52:51 2001 +0200
     7.3 @@ -1,5 +1,5 @@
     7.4  (*  Title: 	HOLCF/FOCUS/Buffer.thy
     7.5 -    ID:         $ $
     7.6 +    ID:         $Id$
     7.7      Author: 	David von Oheimb, TU Muenchen
     7.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.9  
     8.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Thu May 31 18:28:23 2001 +0200
     8.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Thu May 31 20:52:51 2001 +0200
     8.3 @@ -1,5 +1,5 @@
     8.4  (*  Title: 	HOLCF/FOCUS/Buffer_adm.ML
     8.5 -    ID:         $ $
     8.6 +    ID:         $Id$
     8.7      Author: 	David von Oheimb, TU Muenchen
     8.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.9  *)
    8.10 @@ -8,7 +8,7 @@
    8.11  fun _ y t = by t;
    8.12  val b=9999;
    8.13  
    8.14 -Addsimps [Fin_0];
    8.15 +Addsimps [thm "Fin_0"];
    8.16  
    8.17  val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
    8.18  val BufAC_Asm_d3 = prove_forw 
    8.19 @@ -58,7 +58,7 @@
    8.20  b y rtac conjI 1;
    8.21  b y  strip_tac 2;
    8.22  b y  dtac slen_mono 2;
    8.23 -b y  datac ile_trans 1 2;
    8.24 +b y  datac (thm "ile_trans") 1 2;
    8.25  b y ALLGOALS Force_tac;
    8.26  qed "BufAC_Asm_F_stream_antiP";
    8.27  
     9.1 --- a/src/HOLCF/FOCUS/Buffer_adm.thy	Thu May 31 18:28:23 2001 +0200
     9.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.thy	Thu May 31 20:52:51 2001 +0200
     9.3 @@ -1,5 +1,5 @@
     9.4  (*  Title: 	HOLCF/FOCUS/Buffer_adm.thy
     9.5 -    ID:         $ $
     9.6 +    ID:         $Id$
     9.7      Author: 	David von Oheimb, TU Muenchen
     9.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     9.9  
    10.1 --- a/src/HOLCF/FOCUS/FOCUS.ML	Thu May 31 18:28:23 2001 +0200
    10.2 +++ b/src/HOLCF/FOCUS/FOCUS.ML	Thu May 31 20:52:51 2001 +0200
    10.3 @@ -1,5 +1,5 @@
    10.4  (*  Title: 	HOLCF/FOCUS/FOCUS.ML
    10.5 -    ID:         $ $
    10.6 +    ID:         $Id$
    10.7      Author: 	David von Oheimb, TU Muenchen
    10.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    10.9  *)
   10.10 @@ -18,5 +18,5 @@
   10.11  
   10.12  Addsimps[slen_less_1_eq, fstream_exhaust_slen_eq,
   10.13  		   slen_fscons_eq, slen_fscons_less_eq];
   10.14 -Addsimps[Suc_ile_eq];
   10.15 +Addsimps[thm "Suc_ile_eq"];
   10.16  AddEs  [strictI];
    11.1 --- a/src/HOLCF/FOCUS/FOCUS.thy	Thu May 31 18:28:23 2001 +0200
    11.2 +++ b/src/HOLCF/FOCUS/FOCUS.thy	Thu May 31 20:52:51 2001 +0200
    11.3 @@ -1,5 +1,5 @@
    11.4  (*  Title: 	HOLCF/FOCUS/FOCUS.thy
    11.5 -    ID:         $ $
    11.6 +    ID:         $Id$
    11.7      Author: 	David von Oheimb, TU Muenchen
    11.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    11.9  
    12.1 --- a/src/HOLCF/FOCUS/Fstream.ML	Thu May 31 18:28:23 2001 +0200
    12.2 +++ b/src/HOLCF/FOCUS/Fstream.ML	Thu May 31 20:52:51 2001 +0200
    12.3 @@ -1,5 +1,5 @@
    12.4  (*  Title: 	HOLCF/FOCUS/Fstream.ML
    12.5 -    ID:         $ $
    12.6 +    ID:         $Id$
    12.7      Author: 	David von Oheimb, TU Muenchen
    12.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    12.9  *)
    13.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Thu May 31 18:28:23 2001 +0200
    13.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Thu May 31 20:52:51 2001 +0200
    13.3 @@ -1,5 +1,5 @@
    13.4  (*  Title: 	HOLCF/FOCUS/Fstream.thy
    13.5 -    ID:         $ $
    13.6 +    ID:         $Id$
    13.7      Author: 	David von Oheimb, TU Muenchen
    13.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    13.9  
    14.1 --- a/src/HOLCF/FOCUS/ROOT.ML	Thu May 31 18:28:23 2001 +0200
    14.2 +++ b/src/HOLCF/FOCUS/ROOT.ML	Thu May 31 20:52:51 2001 +0200
    14.3 @@ -1,5 +1,5 @@
    14.4  (*  Title:      HOLCF/FOCUS/ROOT.ML
    14.5 -    ID:         $$
    14.6 +    ID:         $Id$
    14.7      Author: 	David von Oheimb, TU Muenchen
    14.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    14.9  
    15.1 --- a/src/HOLCF/FOCUS/Stream_adm.ML	Thu May 31 18:28:23 2001 +0200
    15.2 +++ b/src/HOLCF/FOCUS/Stream_adm.ML	Thu May 31 20:52:51 2001 +0200
    15.3 @@ -1,5 +1,5 @@
    15.4  (*  Title: 	HOLCF/ex/Stream_adm.ML
    15.5 -    ID:         $ $
    15.6 +    ID:         $Id$
    15.7      Author: 	David von Oheimb, TU Muenchen
    15.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    15.9  *)
   15.10 @@ -20,7 +20,7 @@
   15.11  by (EVERY'[eresolve_tac (premises()), atac, etac thin_rl] 1);
   15.12  by (rtac allI 1);
   15.13  by (case_tac "!j. stream_finite (Y j)" 1);
   15.14 -by ( rtac chain_incr 1);
   15.15 +by ( rtac (thm "chain_incr") 1);
   15.16  by ( rtac allI 1);
   15.17  by ( dtac spec 1);
   15.18  by ( Safe_tac);
   15.19 @@ -33,8 +33,8 @@
   15.20  by (stac slen_infinite 1);
   15.21  by (etac thin_rl 1);
   15.22  by (dtac spec 1);
   15.23 -by (fold_goals_tac [ile_def]);
   15.24 -by (etac (ile_iless_trans RS (Infty_eq RS iffD1)) 1);
   15.25 +by (fold_goals_tac [thm "ile_def"]);
   15.26 +by (etac (thm "ile_iless_trans" RS (thm "Infty_eq" RS iffD1)) 1);
   15.27  by (Simp_tac 1);
   15.28  qed "flatstream_adm_lemma";
   15.29  
   15.30 @@ -50,7 +50,7 @@
   15.31  
   15.32  (* context (theory "Nat_InFinity");*)
   15.33  Goal "Fin (i + j) <= x ==> Fin i <= x";
   15.34 -by (rtac ile_trans 1);
   15.35 +by (rtac (thm "ile_trans") 1);
   15.36  by  (atac 2);
   15.37  by (Simp_tac 1);
   15.38  qed "ile_lemma";
   15.39 @@ -67,7 +67,7 @@
   15.40  by (etac allE 1 THEN etac all_dupE 1 THEN dtac mp 1 THEN etac ile_lemma 1);
   15.41  by (dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1);
   15.42  by (etac allE 1 THEN dtac mp 1 THEN rtac ile_lemma 1);
   15.43 -by ( etac ile_trans 1);
   15.44 +by ( etac (thm "ile_trans") 1);
   15.45  by ( etac slen_mono 1);
   15.46  by (etac ssubst 1);
   15.47  by (safe_tac HOL_cs);
   15.48 @@ -93,10 +93,10 @@
   15.49  	etac exE 1,
   15.50  	etac allE 1 THEN etac exE 1,
   15.51  	etac allE 1 THEN etac allE 1 THEN dtac mp 1, (* stream_monoP *)
   15.52 -	 dtac ileI1 1,
   15.53 -	 dtac ile_trans 1,
   15.54 -	  rtac ile_iSuc 1,
   15.55 -	 dtac (iSuc_ile_mono RS iffD1) 1,
   15.56 +	 dtac (thm "ileI1") 1,
   15.57 +	 dtac (thm "ile_trans") 1,
   15.58 +	  rtac (thm "ile_iSuc") 1,
   15.59 +	 dtac (thm "iSuc_ile_mono" RS iffD1) 1,
   15.60  	 atac 1,
   15.61  	dtac mp 1,
   15.62  	 etac is_ub_thelub 1,
   15.63 @@ -117,7 +117,7 @@
   15.64  	etac conjE 1,
   15.65  	case_tac "#x < Fin ia" 1,
   15.66  	 fast_tac HOL_cs 1,
   15.67 -	fold_goals_tac [ile_def],
   15.68 +	fold_goals_tac [thm "ile_def"],
   15.69  	mp_tac 1,
   15.70  	etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1,
   15.71  	etac ssubst 1,
    16.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy	Thu May 31 18:28:23 2001 +0200
    16.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy	Thu May 31 20:52:51 2001 +0200
    16.3 @@ -1,5 +1,5 @@
    16.4  (*  Title: 	HOLCF/ex/Stream_adm.thy
    16.5 -    ID:         $ $
    16.6 +    ID:         $Id$
    16.7      Author: 	David von Oheimb, TU Muenchen
    16.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    16.9  
    17.1 --- a/src/HOLCF/ex/Stream.ML	Thu May 31 18:28:23 2001 +0200
    17.2 +++ b/src/HOLCF/ex/Stream.ML	Thu May 31 20:52:51 2001 +0200
    17.3 @@ -384,7 +384,7 @@
    17.4  by (Simp_tac 1);
    17.5  by (stac Least_equality 1);
    17.6  by    Auto_tac;
    17.7 -by (simp_tac(simpset() addsimps [Fin_0]) 1);
    17.8 +by (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
    17.9  qed "slen_empty";
   17.10  
   17.11  Goalw [slen_def] "x ~= \\<bottom> ==> #(x&&xs) = iSuc (#xs)";
   17.12 @@ -393,7 +393,7 @@
   17.13  by (rtac (split_if RS iffD2) 2);
   17.14  by  Safe_tac;
   17.15  by   (fast_tac (claset() addIs [stream_finite_lemma1]) 2);
   17.16 -by  (rtac (iSuc_Infty RS sym) 2);
   17.17 +by  (rtac (thm "iSuc_Infty" RS sym) 2);
   17.18  by (rtac (split_if RS iffD2) 1);
   17.19  by (Simp_tac 1);
   17.20  by Safe_tac;
   17.21 @@ -409,8 +409,8 @@
   17.22  
   17.23  Goal "#x < Fin 1 = (x = UU)";
   17.24  by (stream_case_tac "x" 1);
   17.25 -by (auto_tac (claset(), simpset() delsimps [iSuc_Fin] addsimps
   17.26 - [Fin_0, iSuc_Fin RS sym,i0_iless_iSuc, iSuc_mono]));
   17.27 +by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
   17.28 + [thm "Fin_0", thm "iSuc_Fin" RS sym, thm "i0_iless_iSuc", thm "iSuc_mono"]));
   17.29  qed "slen_less_1_eq";
   17.30  
   17.31  Goal "(#x = 0) = (x = \\<bottom>)";
   17.32 @@ -422,8 +422,8 @@
   17.33  
   17.34  Goal "Fin (Suc n) < #x = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
   17.35  by (stream_case_tac "x" 1);
   17.36 -by (auto_tac (claset(), simpset() delsimps [iSuc_Fin] addsimps
   17.37 -                [iSuc_Fin RS sym, iSuc_mono]));
   17.38 +by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
   17.39 +                [thm "iSuc_Fin" RS sym, thm "iSuc_mono"]));
   17.40  by  (dtac sym 1);
   17.41  by  (rotate_tac 2 2);
   17.42  by  Auto_tac;
   17.43 @@ -438,15 +438,15 @@
   17.44  
   17.45  Goal 
   17.46  "#x < Fin (Suc (Suc n)) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
   17.47 -by (stac (iSuc_Fin RS sym) 1);
   17.48 -by (stac (iSuc_Fin RS sym) 1);
   17.49 +by (stac (thm "iSuc_Fin" RS sym) 1);
   17.50 +by (stac (thm "iSuc_Fin" RS sym) 1);
   17.51  by (safe_tac HOL_cs);
   17.52  by  (rotate_tac ~1 1);
   17.53 -by  (asm_full_simp_tac (HOL_ss addsimps [slen_scons, iSuc_mono]) 1);
   17.54 +by  (asm_full_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1);
   17.55  by  (Asm_full_simp_tac 1);
   17.56  by (stream_case_tac "x" 1);
   17.57 -by ( simp_tac (HOL_ss addsimps [slen_empty, i0_iless_iSuc]) 1);
   17.58 -by (asm_simp_tac (HOL_ss addsimps [slen_scons, iSuc_mono]) 1);
   17.59 +by ( simp_tac (HOL_ss addsimps [slen_empty, thm "i0_iless_iSuc"]) 1);
   17.60 +by (asm_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1);
   17.61  by (etac allE 1);
   17.62  by (etac allE 1);
   17.63  by (safe_tac HOL_cs);
   17.64 @@ -457,7 +457,7 @@
   17.65  
   17.66  Goal "!x. Fin n < #x = (stream_take n\\<cdot>x ~= x)";
   17.67  by (nat_ind_tac "n" 1);
   17.68 -by  (simp_tac(simpset() addsimps [slen_empty_eq, Fin_0]) 1);
   17.69 +by  (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1);
   17.70  by  (Fast_tac 1);
   17.71  by (rtac allI 1);
   17.72  by (asm_simp_tac (simpset() addsimps [slen_scons_eq]) 1);
   17.73 @@ -469,7 +469,7 @@
   17.74  by Auto_tac;
   17.75  qed_spec_mp "slen_take_eq";
   17.76  
   17.77 -Goalw [ile_def] "#x <= Fin n = (stream_take n\\<cdot>x = x)";
   17.78 +Goalw [thm "ile_def"] "#x <= Fin n = (stream_take n\\<cdot>x = x)";
   17.79  by (simp_tac (simpset() addsimps [slen_take_eq]) 1);
   17.80  qed "slen_take_eq_rev";
   17.81  
   17.82 @@ -479,10 +479,10 @@
   17.83  
   17.84  Goal "!x. ~stream_finite x --> #(stream_take i\\<cdot>x) = Fin i";
   17.85  by (nat_ind_tac "i" 1);
   17.86 -by  (simp_tac(simpset() addsimps [Fin_0]) 1);
   17.87 +by  (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
   17.88  by (rtac allI 1);
   17.89  by (stream_case_tac "x" 1);
   17.90 -by  (auto_tac (claset()addSIs [stream_finite_lemma1], simpset() delsimps [iSuc_Fin] addsimps [iSuc_Fin RS sym]));
   17.91 +by  (auto_tac (claset()addSIs [stream_finite_lemma1], simpset() delsimps [thm "iSuc_Fin"] addsimps [thm "iSuc_Fin" RS sym]));
   17.92  by (force_tac (claset(), simpset() addsimps [stream.finite_def]) 1);
   17.93  qed_spec_mp "slen_take_lemma2";
   17.94  
   17.95 @@ -491,9 +491,9 @@
   17.96  by  (etac stream_finite_ind 1);
   17.97  by   (Simp_tac 1);
   17.98  by  (etac (slen_scons RS ssubst) 1);
   17.99 -by  (stac (iSuc_Infty RS sym) 1);
  17.100 +by  (stac (thm "iSuc_Infty" RS sym) 1);
  17.101  by  (etac contrapos_nn 1);
  17.102 -by  (etac (iSuc_inject RS iffD1) 1);
  17.103 +by  (etac (thm "iSuc_inject" RS iffD1) 1);
  17.104  by (case_tac "#x" 1);
  17.105  by (auto_tac (claset()addSDs [slen_take_lemma1],
  17.106          simpset() addsimps [stream.finite_def]));
  17.107 @@ -510,9 +510,9 @@
  17.108  by  (Simp_tac 1);
  17.109  by (rtac allI 1);
  17.110  by (stream_case_tac "x" 1);
  17.111 -by  (asm_simp_tac (HOL_ss addsimps [slen_empty, i0_lb]) 1);
  17.112 +by  (asm_simp_tac (HOL_ss addsimps [slen_empty, thm "i0_lb"]) 1);
  17.113  by (asm_simp_tac (HOL_ss addsimps [slen_scons]) 1);
  17.114 -by (fast_tac(claset() addSIs [iSuc_ile_mono RS iffD2] addSDs stream.inverts) 1);
  17.115 +by (fast_tac(claset() addSIs [thm "iSuc_ile_mono" RS iffD2] addSDs stream.inverts) 1);
  17.116  qed "slen_mono";
  17.117  
  17.118  Goal "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> \
  17.119 @@ -522,14 +522,14 @@
  17.120  by (strip_tac 1);
  17.121  by (stream_case_tac "x" 1);
  17.122  by  (asm_full_simp_tac (HOL_ss addsimps [slen_empty, 
  17.123 -              iSuc_Fin RS sym, not_iSuc_ilei0]) 1);
  17.124 +              thm "iSuc_Fin" RS sym, thm "not_iSuc_ilei0"]) 1);
  17.125  by (fatac stream_prefix 1 1);
  17.126  by (safe_tac (claset() addSDs [stream_flat_prefix]));
  17.127  by (Simp_tac 1);
  17.128  by (rtac cfun_arg_cong 1);
  17.129  by (rotate_tac 3 1);
  17.130 -by (asm_full_simp_tac (simpset() delsimps [iSuc_Fin] addsimps 
  17.131 -        [iSuc_Fin RS sym, iSuc_ile_mono]) 1);
  17.132 +by (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] addsimps 
  17.133 +        [thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1);
  17.134  qed_spec_mp "slen_take_lemma3";
  17.135  
  17.136  Goal "stream_finite t ==> \
  17.137 @@ -548,7 +548,7 @@
  17.138  qed "slen_strict_mono_lemma";
  17.139  
  17.140  Goal "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t";
  17.141 -by (rtac ilessI1 1);
  17.142 +by (rtac (thm "ilessI1") 1);
  17.143  by  (etac slen_mono 1);
  17.144  by (dtac slen_strict_mono_lemma 1);
  17.145  by (Fast_tac 1);
  17.146 @@ -559,12 +559,12 @@
  17.147  by  (Simp_tac 1);
  17.148  by (strip_tac 1);
  17.149  by (stream_case_tac "x" 1);
  17.150 -by  (asm_full_simp_tac (simpset() delsimps [iSuc_Fin] 
  17.151 -             addsimps [iSuc_Fin RS sym]) 1);
  17.152 +by  (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] 
  17.153 +             addsimps [thm "iSuc_Fin" RS sym]) 1);
  17.154  by (stac iterate_Suc2 1);
  17.155  by (rotate_tac 2 1);
  17.156 -by (asm_full_simp_tac  (simpset() delsimps [iSuc_Fin] 
  17.157 -    addsimps [iSuc_Fin RS sym, iSuc_ile_mono]) 1);
  17.158 +by (asm_full_simp_tac  (simpset() delsimps [thm "iSuc_Fin"] 
  17.159 +    addsimps [thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1);
  17.160  qed_spec_mp "slen_rt_mult";
  17.161  
  17.162