# HG changeset patch
# User wenzelm
# Date 991335171 -7200
# Node ID 778c369559d90517f6b4bf7e19dcd45f2a2ccf5e
# Parent  9b80fe19407fcbdab5058cdedf8244c920fab11f
tuned

diff -r 9b80fe19407f -r 778c369559d9 src/HOL/CTL/CTL.thy
--- a/src/HOL/CTL/CTL.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOL/CTL/CTL.thy	Thu May 31 20:52:51 2001 +0200
@@ -4,13 +4,16 @@
 section {* CTL formulae *}
 
 text {*
-  \tweakskip By using the common technique of ``shallow embedding'', a
-  CTL formula is identified with the corresponding set of states where
-  it holds.  Consequently, CTL operations such as negation,
-  conjunction, disjunction simply become complement, intersection,
-  union of sets.  We only require a separate operation for
-  implication, as point-wise inclusion is usually not encountered in
-  plain set-theory.
+  \tweakskip We formalize basic concepts of Computational Tree Logic
+  (CTL) \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
+  simply-typed set theory of HOL.
+
+  By using the common technique of ``shallow embedding'', a CTL
+  formula is identified with the corresponding set of states where it
+  holds.  Consequently, CTL operations such as negation, conjunction,
+  disjunction simply become complement, intersection, union of sets.
+  We only require a separate operation for implication, as point-wise
+  inclusion is usually not encountered in plain set-theory.
 *}
 
 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
@@ -25,16 +28,16 @@
 
 
 text {*
-  \smallskip The CTL path operators are more interesting; they are 
-  based on an arbitrary, but fixed model @{text \<M>}, which is simply 
-  a transition relation over states @{typ "'a"}. 
+  \smallskip The CTL path operators are more interesting; they are
+  based on an arbitrary, but fixed model @{text \<M>}, which is simply
+  a transition relation over states @{typ "'a"}.
 *}
 
 consts model :: "('a \<times> 'a) set"    ("\<M>")
 
 text {*
-  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken as
-  primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
+  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
+  as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
   defined as derived ones.  The formula @{text "\<EX> p"} holds in a
   state @{term s}, iff there is a successor state @{term s'} (with
   respect to the model @{term \<M>}), such that @{term p} holds in
@@ -55,8 +58,9 @@
   EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
 
 text {*
-  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined 
-  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text "\<EG>"}.
+  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
+  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
+  "\<EG>"}.
 *}
 
 constdefs
@@ -67,11 +71,11 @@
 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
 
 
-
 section {* Basic fixed point properties *}
 
 text {*
-  \tweakskip First of all, we use the de-Morgan property of fixed points
+  \tweakskip First of all, we use the de-Morgan property of fixed
+  points
 *}
 
 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
@@ -131,7 +135,6 @@
   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
 qed
 
-
 text {*
   From the greatest fixed point definition of @{term "\<AG> p"}, we
   derive as a consequence of the Knaster-Tarski theorem on the one
@@ -141,8 +144,8 @@
 
 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<AX> s)" sorry (* by rule (auto simp add: AX_def EX_def) *)
-  then show ?thesis sorry (* by (simp only: AG_gfp) (rule gfp_unfold) *)
+  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
 qed
 
 text {*
@@ -188,7 +191,8 @@
 
 lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
 lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
-lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q" by (simp only: AG_gfp, rule gfp_mono) auto 
+lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
+  by (simp only: AG_gfp, rule gfp_mono) auto 
 
 text {*
   The formula @{term "AG p"} implies @{term "AX p"} (we use
@@ -221,15 +225,14 @@
 qed
 
 text {*
-  \smallskip We now give an alternative characterization of the
-  @{text "\<AG>"} operator, which describes the @{text "\<AG>"}
-  operator in an ``operational'' way by tree induction:
-  In a state holds @{term "AG p"} iff
-  in that state holds @{term p}, and in all reachable states @{term s}
-  follows from the fact that @{term p} holds in @{term s}, that @{term
-  p} also holds in all successor states of @{term s}.  We use the
-  co-induction principle @{thm [source] AG_I} to establish this in a
-  purely algebraic manner.
+  \smallskip We now give an alternative characterization of the @{text
+  "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
+  an ``operational'' way by tree induction: In a state holds @{term
+  "AG p"} iff in that state holds @{term p}, and in all reachable
+  states @{term s} follows from the fact that @{term p} holds in
+  @{term s}, that @{term p} also holds in all successor states of
+  @{term s}.  We use the co-induction principle @{thm [source] AG_I}
+  to establish this in a purely algebraic manner.
 *}
 
 theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
diff -r 9b80fe19407f -r 778c369559d9 src/HOL/CTL/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/CTL/document/root.bib	Thu May 31 20:52:51 2001 +0200
@@ -0,0 +1,13 @@
+
+@Misc{McMillan-LectureNotes,
+  author =	 {Ken McMillan},
+  title =	 {Lecture notes on verification of digital and hybrid systems},
+  note =	 {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
+}
+
+@PhdThesis{McMillan-PhDThesis,
+  author = 	 {Ken McMillan},
+  title = 	 {Symbolic Model Checking: an approach to the state explosion problem},
+  school = 	 {Carnegie Mellon University},
+  year = 	 1992
+}
diff -r 9b80fe19407f -r 778c369559d9 src/HOL/CTL/document/root.tex
--- a/src/HOL/CTL/document/root.tex	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOL/CTL/document/root.tex	Thu May 31 20:52:51 2001 +0200
@@ -2,6 +2,9 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
+\urlstyle{rm}
+\isabellestyle{it}
+
 \newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
 \newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
 \newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
@@ -9,15 +12,13 @@
 \newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
 \newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
 
-%for best-style documents ...
-\urlstyle{rm}
-\isabellestyle{it}
 
 \begin{document}
 
-\title{A short case study on CTL}
+\title{Some properties of CTL}
 \author{Gertrud Bauer}
 \maketitle
+
 \tableofcontents
 \bigskip
 
@@ -26,7 +27,7 @@
 
 \input{session}
 
-%\bibliographystyle{plain}
-%\bibliography{root}
+\bibliographystyle{abbrv}
+\bibliography{root}
 
 \end{document}
diff -r 9b80fe19407f -r 778c369559d9 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOL/Library/Continuity.thy	Thu May 31 20:52:51 2001 +0200
@@ -1,219 +1,222 @@
 (*  Title:      HOL/Library/Continuity.thy
-    ID:         $$
-    Author: 	David von Oheimb, TU Muenchen
+    ID:         $Id$
+    Author:     David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
 *)
 
 header {*
-  \title{Continuity and interations (of set transformers)}
+  \title{Continuity and iterations (of set transformers)}
   \author{David von Oheimb}
 *}
 
-theory Continuity = Relation_Power:
-
+theory Continuity = Main:
 
 subsection "Chains"
 
 constdefs
-  up_chain      :: "(nat => 'a set) => bool"
- "up_chain F      == !i. F i <= F (Suc i)"
+  up_chain :: "(nat => 'a set) => bool"
+  "up_chain F == \<forall>i. F i \<subseteq> F (Suc i)"
 
-lemma up_chainI: "(!!i. F i <= F (Suc i)) ==> up_chain F"
-by (simp add: up_chain_def);
+lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
+  by (simp add: up_chain_def)
 
-lemma up_chainD: "up_chain F ==> F i <= F (Suc i)"
-by (simp add: up_chain_def);
+lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
+  by (simp add: up_chain_def)
 
-lemma up_chain_less_mono [rule_format]: "up_chain F ==> x < y --> F x <= F y"
-apply (induct_tac y)
-apply (blast dest: up_chainD elim: less_SucE)+
-done
+lemma up_chain_less_mono [rule_format]:
+    "up_chain F ==> x < y --> F x \<subseteq> F y"
+  apply (induct_tac y)
+  apply (blast dest: up_chainD elim: less_SucE)+
+  done
 
-lemma up_chain_mono: "up_chain F ==> x <= y ==> F x <= F y"
-apply (drule le_imp_less_or_eq)
-apply (blast dest: up_chain_less_mono)
-done
+lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
+  apply (drule le_imp_less_or_eq)
+  apply (blast dest: up_chain_less_mono)
+  done
 
 
 constdefs
-  down_chain      :: "(nat => 'a set) => bool"
- "down_chain F == !i. F (Suc i) <= F i"
+  down_chain :: "(nat => 'a set) => bool"
+  "down_chain F == \<forall>i. F (Suc i) \<subseteq> F i"
 
-lemma down_chainI: "(!!i. F (Suc i) <= F i) ==> down_chain F"
-by (simp add: down_chain_def);
+lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
+  by (simp add: down_chain_def)
 
-lemma down_chainD: "down_chain F ==> F (Suc i) <= F i"
-by (simp add: down_chain_def);
+lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
+  by (simp add: down_chain_def)
 
-lemma down_chain_less_mono[rule_format]: "down_chain F ==> x < y --> F y <= F x"
-apply (induct_tac y)
-apply (blast dest: down_chainD elim: less_SucE)+
-done
+lemma down_chain_less_mono [rule_format]:
+    "down_chain F ==> x < y --> F y \<subseteq> F x"
+  apply (induct_tac y)
+  apply (blast dest: down_chainD elim: less_SucE)+
+  done
 
-lemma down_chain_mono: "down_chain F ==> x <= y ==> F y <= F x"
-apply (drule le_imp_less_or_eq)
-apply (blast dest: down_chain_less_mono)
-done
+lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
+  apply (drule le_imp_less_or_eq)
+  apply (blast dest: down_chain_less_mono)
+  done
 
 
 subsection "Continuity"
 
 constdefs
   up_cont :: "('a set => 'a set) => bool"
- "up_cont f == !F. up_chain F --> f (Union (range F)) = Union (f`(range F))"
+  "up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)"
 
-lemma up_contI: 
- "(!!F. up_chain F ==> f (Union (range F)) = Union (f`(range F))) ==> up_cont f"
-apply (unfold up_cont_def)
-by blast
+lemma up_contI:
+    "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
+  apply (unfold up_cont_def)
+  apply blast
+  done
 
-lemma up_contD: 
-  "[| up_cont f; up_chain F |] ==> f (Union (range F)) = Union (f`(range F))"
-apply (unfold up_cont_def)
-by auto
+lemma up_contD:
+    "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
+  apply (unfold up_cont_def)
+  apply auto
+  done
 
 
 lemma up_cont_mono: "up_cont f ==> mono f"
-apply (rule monoI)
-apply (drule_tac F = "%i. if i = 0 then A else B" in up_contD)
-apply  (rule up_chainI)
-apply  simp+
-apply (drule Un_absorb1)
-apply auto
-done
+  apply (rule monoI)
+  apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
+   apply (rule up_chainI)
+   apply  simp+
+  apply (drule Un_absorb1)
+  apply auto
+  done
 
 
 constdefs
   down_cont :: "('a set => 'a set) => bool"
- "down_cont f == !F. down_chain F --> f (Inter (range F)) = Inter (f`(range F))"
+  "down_cont f ==
+    \<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)"
 
-lemma down_contI: 
- "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f`(range F))) ==> 
-  down_cont f"
-apply (unfold down_cont_def)
-by blast
+lemma down_contI:
+  "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
+    down_cont f"
+  apply (unfold down_cont_def)
+  apply blast
+  done
 
-lemma down_contD: "[| down_cont f; down_chain F |] ==> 
-  f (Inter (range F)) = Inter (f`(range F))"
-apply (unfold down_cont_def)
-by auto
+lemma down_contD: "down_cont f ==> down_chain F ==>
+    f (Inter (range F)) = Inter (f ` range F)"
+  apply (unfold down_cont_def)
+  apply auto
+  done
 
 lemma down_cont_mono: "down_cont f ==> mono f"
-apply (rule monoI)
-apply (drule_tac F = "%i. if i = 0 then B else A" in down_contD)
-apply  (rule down_chainI)
-apply  simp+
-apply (drule Int_absorb1)
-apply auto
-done
+  apply (rule monoI)
+  apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
+   apply (rule down_chainI)
+   apply simp+
+  apply (drule Int_absorb1)
+  apply auto
+  done
 
 
 subsection "Iteration"
 
 constdefs
-
   up_iterate :: "('a set => 'a set) => nat => 'a set"
- "up_iterate f n == (f^n) {}"
+  "up_iterate f n == (f^n) {}"
 
 lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
-by (simp add: up_iterate_def)
+  by (simp add: up_iterate_def)
 
-lemma up_iterate_Suc [simp]: 
-  "up_iterate f (Suc i) = f (up_iterate f i)"
-by (simp add: up_iterate_def)
+lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)"
+  by (simp add: up_iterate_def)
 
 lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
-apply (rule up_chainI)
-apply (induct_tac i)
-apply simp+
-apply (erule (1) monoD)
-done
+  apply (rule up_chainI)
+  apply (induct_tac i)
+   apply simp+
+  apply (erule (1) monoD)
+  done
 
-lemma UNION_up_iterate_is_fp: 
-"up_cont F ==> F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
-apply (frule up_cont_mono [THEN up_iterate_chain])
-apply (drule (1) up_contD)
-apply simp
-apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
-apply (case_tac "xa")
-apply auto
-done
+lemma UNION_up_iterate_is_fp:
+  "up_cont F ==>
+    F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
+  apply (frule up_cont_mono [THEN up_iterate_chain])
+  apply (drule (1) up_contD)
+  apply simp
+  apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
+  apply (case_tac xa)
+   apply auto
+  done
 
-lemma UNION_up_iterate_lowerbound: 
-"[| mono F; F P = P |] ==> UNION UNIV (up_iterate F) <= P"
-apply (subgoal_tac "(!!i. up_iterate F i <= P)")
-apply  fast
-apply (induct_tac "i")
-prefer 2 apply (drule (1) monoD)
-apply auto
-done
+lemma UNION_up_iterate_lowerbound:
+    "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P"
+  apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)")
+   apply fast
+  apply (induct_tac i)
+  prefer 2 apply (drule (1) monoD)
+   apply auto
+  done
 
-lemma UNION_up_iterate_is_lfp: 
-  "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
-apply (rule set_eq_subset [THEN iffD2])
-apply (rule conjI)
-prefer 2
-apply  (drule up_cont_mono)
-apply  (rule UNION_up_iterate_lowerbound)
-apply   assumption
-apply  (erule lfp_unfold [symmetric])
-apply (rule lfp_lowerbound)
-apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
-apply (erule UNION_up_iterate_is_fp [symmetric])
-done
+lemma UNION_up_iterate_is_lfp:
+    "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
+  apply (rule set_eq_subset [THEN iffD2])
+  apply (rule conjI)
+   prefer 2
+   apply (drule up_cont_mono)
+   apply (rule UNION_up_iterate_lowerbound)
+    apply assumption
+   apply (erule lfp_unfold [symmetric])
+  apply (rule lfp_lowerbound)
+  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
+  apply (erule UNION_up_iterate_is_fp [symmetric])
+  done
 
 
 constdefs
-
   down_iterate :: "('a set => 'a set) => nat => 'a set"
- "down_iterate f n == (f^n) UNIV"
+  "down_iterate f n == (f^n) UNIV"
 
 lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
-by (simp add: down_iterate_def)
+  by (simp add: down_iterate_def)
 
-lemma down_iterate_Suc [simp]: 
-  "down_iterate f (Suc i) = f (down_iterate f i)"
-by (simp add: down_iterate_def)
+lemma down_iterate_Suc [simp]:
+    "down_iterate f (Suc i) = f (down_iterate f i)"
+  by (simp add: down_iterate_def)
 
 lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
-apply (rule down_chainI)
-apply (induct_tac i)
-apply simp+
-apply (erule (1) monoD)
-done
+  apply (rule down_chainI)
+  apply (induct_tac i)
+   apply simp+
+  apply (erule (1) monoD)
+  done
 
-lemma INTER_down_iterate_is_fp: 
-"down_cont F ==> 
- F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
-apply (frule down_cont_mono [THEN down_iterate_chain])
-apply (drule (1) down_contD)
-apply simp
-apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
-apply (case_tac "xa")
-apply auto
-done
+lemma INTER_down_iterate_is_fp:
+  "down_cont F ==>
+    F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
+  apply (frule down_cont_mono [THEN down_iterate_chain])
+  apply (drule (1) down_contD)
+  apply simp
+  apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
+  apply (case_tac xa)
+   apply auto
+  done
 
-lemma INTER_down_iterate_upperbound: 
-"[| mono F; F P = P |] ==> P <= INTER UNIV (down_iterate F)"
-apply (subgoal_tac "(!!i. P <= down_iterate F i)")
-apply  fast
-apply (induct_tac "i")
-prefer 2 apply (drule (1) monoD)
-apply auto
-done
+lemma INTER_down_iterate_upperbound:
+    "mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)"
+  apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)")
+   apply fast
+  apply (induct_tac i)
+  prefer 2 apply (drule (1) monoD)
+   apply auto
+  done
 
-lemma INTER_down_iterate_is_gfp: 
-  "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
-apply (rule set_eq_subset [THEN iffD2])
-apply (rule conjI)
-apply  (drule down_cont_mono)
-apply  (rule INTER_down_iterate_upperbound)
-apply   assumption
-apply  (erule gfp_unfold [symmetric])
-apply (rule gfp_upperbound)
-apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
-apply (erule INTER_down_iterate_is_fp)
-done
+lemma INTER_down_iterate_is_gfp:
+    "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
+  apply (rule set_eq_subset [THEN iffD2])
+  apply (rule conjI)
+   apply (drule down_cont_mono)
+   apply (rule INTER_down_iterate_upperbound)
+    apply assumption
+   apply (erule gfp_unfold [symmetric])
+  apply (rule gfp_upperbound)
+  apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
+  apply (erule INTER_down_iterate_is_fp)
+  done
 
 end
diff -r 9b80fe19407f -r 778c369559d9 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Thu May 31 20:52:51 2001 +0200
@@ -1,8 +1,7 @@
-(*  Title: 	HOL/Library/Nat_Infinity.thy
-    ID:         $ $
-    Author: 	David von Oheimb, TU Muenchen
+(*  Title:      HOL/Library/Nat_Infinity.thy
+    ID:         $Id$
+    Author:     David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
 *)
 
 header {*
@@ -10,14 +9,14 @@
   \author{David von Oheimb}
 *}
 
-theory Nat_Infinity = Datatype:
+theory Nat_Infinity = Main:
 
 subsection "Definitions"
 
 text {*
- We extend the standard natural numbers by a special value indicating infinity.
- This includes extending the ordering relations @{term "op <"} and 
- @{term "op <="}.
+  We extend the standard natural numbers by a special value indicating
+  infinity.  This includes extending the ordering relations @{term "op
+  <"} and @{term "op \<le>"}.
 *}
 
 datatype inat = Fin nat | Infty
@@ -26,191 +25,159 @@
 instance inat :: zero ..
 
 consts
-
-  iSuc	:: "inat => inat"
+  iSuc :: "inat => inat"
 
 syntax (xsymbols)
-
-  Infty		:: inat					("\<infinity>")
+  Infty :: inat    ("\<infinity>")
 
 defs
-
-  iZero_def:	"0      == Fin 0"
-  iSuc_def:	"iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
-  iless_def:	"m < n  == case m of Fin m1 => (case n of Fin n1 => m1 < n1 
-						             | \<infinity> => True)
-				   | \<infinity>  => False "
-  ile_def:	"(m::inat) <= n == \<not>(n<m)"
+  iZero_def: "0 == Fin 0"
+  iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
+  iless_def: "m < n ==
+    case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
+    | \<infinity>  => False"
+  ile_def: "(m::inat) \<le> n == \<not> (n < m)"
 
 lemmas inat_defs = iZero_def iSuc_def iless_def ile_def
 lemmas inat_splits = inat.split inat.split_asm
 
-
-text {* Below is a not quite complete set of theorems. Use
-@{text "apply(simp add:inat_defs split:inat_splits, arith?)"}
-to prove new theorems or solve arithmetic subgoals involving @{typ inat} 
-on the fly.
+text {*
+  Below is a not quite complete set of theorems.  Use method @{text
+  "(simp add: inat_defs split:inat_splits, arith?)"} to prove new
+  theorems or solve arithmetic subgoals involving @{typ inat} on the
+  fly.
 *}
 
 subsection "Constructors"
 
 lemma Fin_0: "Fin 0 = 0"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 
 subsection "Ordering relations"
 
 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma iless_linear: "m < n | m = n | n < (m::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma i0_iless_iSuc [simp]: "0 < iSuc n"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
-by(simp add:inat_defs split:inat_splits, arith?)
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 
 (* ----------------------------------------------------------------------- *)
 
-lemma ile_def2: "m <= n = (m < n | m = (n::inat))"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma ile_refl [simp]: "n <= (n::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma ile_refl [simp]: "n \<le> (n::inat)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma ile_trans: "i <= j ==> j <= k ==> i <= (k::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma ile_iless_trans: "i <= j ==> j < k ==> i < (k::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma iless_ile_trans: "i < j ==> j <= k ==> i < (k::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma Infty_ub [simp]: "n <= \<infinity>"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma Infty_ub [simp]: "n \<le> \<infinity>"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma i0_lb [simp]: "(0::inat) <= n"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma i0_lb [simp]: "(0::inat) \<le> n"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma Infty_ileE [elim!]: "\<infinity> <= Fin m ==> R"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma Fin_ile_mono [simp]: "(Fin n <= Fin m) = (n <= m)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma ilessI1: "n <= m ==> n \<noteq> m ==> n < (m::inat)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma ileI1: "m < n ==> iSuc m <= n"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma ileI1: "m < n ==> iSuc m \<le> n"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma Suc_ile_eq: "Fin (Suc m) <= n = (Fin m < n)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma iSuc_ile_mono [simp]: "iSuc n <= iSuc m = (n <= m)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m <= n)"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n <= 0"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma ile_iSuc [simp]: "n <= iSuc n"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma ile_iSuc [simp]: "n \<le> iSuc n"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
-lemma Fin_ile: "n <= Fin m ==> \<exists>k. n = Fin k"
-by(simp add:inat_defs split:inat_splits, arith?)
+lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
+  by (simp add:inat_defs split:inat_splits, arith?)
 
 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
-apply (induct_tac "k")
-apply  (simp (no_asm) only: Fin_0)
-apply  (fast intro: ile_iless_trans i0_lb)
-apply (erule exE)
-apply (drule spec)
-apply (erule exE)
-apply (drule ileI1)
-apply (rule iSuc_Fin [THEN subst])
-apply (rule exI)
-apply (erule (1) ile_iless_trans)
-done
-
-ML {*
-val Fin_0 = thm "Fin_0";
-val Suc_ile_eq = thm "Suc_ile_eq";
-val iSuc_Fin = thm "iSuc_Fin";
-val iSuc_Infty = thm "iSuc_Infty";
-val iSuc_mono = thm "iSuc_mono";
-val iSuc_ile_mono = thm "iSuc_ile_mono";
-val not_iSuc_ilei0=thm "not_iSuc_ilei0";
-val iSuc_inject = thm "iSuc_inject";
-val i0_iless_iSuc = thm "i0_iless_iSuc";
-val i0_eq = thm "i0_eq";
-val i0_lb = thm "i0_lb";
-val ile_def = thm "ile_def";
-val ile_refl = thm "ile_refl";
-val Infty_ub = thm "Infty_ub";
-val ilessI1 = thm "ilessI1";
-val ile_iless_trans = thm "ile_iless_trans";
-val ile_trans = thm "ile_trans";
-val ileI1 = thm "ileI1";
-val ile_iSuc = thm "ile_iSuc";
-val Fin_iless_Infty = thm "Fin_iless_Infty";
-val Fin_ile_mono = thm "Fin_ile_mono";
-val chain_incr = thm "chain_incr";
-val Infty_eq = thm "Infty_eq";
-*}
+  apply (induct_tac k)
+   apply (simp (no_asm) only: Fin_0)
+   apply (fast intro: ile_iless_trans i0_lb)
+  apply (erule exE)
+  apply (drule spec)
+  apply (erule exE)
+  apply (drule ileI1)
+  apply (rule iSuc_Fin [THEN subst])
+  apply (rule exI)
+  apply (erule (1) ile_iless_trans)
+  done
 
 end
-
-
-
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Buffer.ML
--- a/src/HOLCF/FOCUS/Buffer.ML	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer.ML	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/Buffer.ML
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Buffer.thy
--- a/src/HOLCF/FOCUS/Buffer.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/Buffer.thy
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/Buffer_adm.ML
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
@@ -8,7 +8,7 @@
 fun _ y t = by t;
 val b=9999;
 
-Addsimps [Fin_0];
+Addsimps [thm "Fin_0"];
 
 val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
 val BufAC_Asm_d3 = prove_forw 
@@ -58,7 +58,7 @@
 b y rtac conjI 1;
 b y  strip_tac 2;
 b y  dtac slen_mono 2;
-b y  datac ile_trans 1 2;
+b y  datac (thm "ile_trans") 1 2;
 b y ALLGOALS Force_tac;
 qed "BufAC_Asm_F_stream_antiP";
 
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOLCF/FOCUS/Buffer_adm.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/Buffer_adm.thy
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/FOCUS.ML
--- a/src/HOLCF/FOCUS/FOCUS.ML	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.ML	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/FOCUS.ML
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
@@ -18,5 +18,5 @@
 
 Addsimps[slen_less_1_eq, fstream_exhaust_slen_eq,
 		   slen_fscons_eq, slen_fscons_less_eq];
-Addsimps[Suc_ile_eq];
+Addsimps[thm "Suc_ile_eq"];
 AddEs  [strictI];
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/FOCUS.thy
--- a/src/HOLCF/FOCUS/FOCUS.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.thy	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/FOCUS.thy
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Fstream.ML
--- a/src/HOLCF/FOCUS/Fstream.ML	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Fstream.ML	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/Fstream.ML
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/FOCUS/Fstream.thy
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/ROOT.ML
--- a/src/HOLCF/FOCUS/ROOT.ML	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/ROOT.ML	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/FOCUS/ROOT.ML
-    ID:         $$
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Stream_adm.ML
--- a/src/HOLCF/FOCUS/Stream_adm.ML	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.ML	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/ex/Stream_adm.ML
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
@@ -20,7 +20,7 @@
 by (EVERY'[eresolve_tac (premises()), atac, etac thin_rl] 1);
 by (rtac allI 1);
 by (case_tac "!j. stream_finite (Y j)" 1);
-by ( rtac chain_incr 1);
+by ( rtac (thm "chain_incr") 1);
 by ( rtac allI 1);
 by ( dtac spec 1);
 by ( Safe_tac);
@@ -33,8 +33,8 @@
 by (stac slen_infinite 1);
 by (etac thin_rl 1);
 by (dtac spec 1);
-by (fold_goals_tac [ile_def]);
-by (etac (ile_iless_trans RS (Infty_eq RS iffD1)) 1);
+by (fold_goals_tac [thm "ile_def"]);
+by (etac (thm "ile_iless_trans" RS (thm "Infty_eq" RS iffD1)) 1);
 by (Simp_tac 1);
 qed "flatstream_adm_lemma";
 
@@ -50,7 +50,7 @@
 
 (* context (theory "Nat_InFinity");*)
 Goal "Fin (i + j) <= x ==> Fin i <= x";
-by (rtac ile_trans 1);
+by (rtac (thm "ile_trans") 1);
 by  (atac 2);
 by (Simp_tac 1);
 qed "ile_lemma";
@@ -67,7 +67,7 @@
 by (etac allE 1 THEN etac all_dupE 1 THEN dtac mp 1 THEN etac ile_lemma 1);
 by (dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1);
 by (etac allE 1 THEN dtac mp 1 THEN rtac ile_lemma 1);
-by ( etac ile_trans 1);
+by ( etac (thm "ile_trans") 1);
 by ( etac slen_mono 1);
 by (etac ssubst 1);
 by (safe_tac HOL_cs);
@@ -93,10 +93,10 @@
 	etac exE 1,
 	etac allE 1 THEN etac exE 1,
 	etac allE 1 THEN etac allE 1 THEN dtac mp 1, (* stream_monoP *)
-	 dtac ileI1 1,
-	 dtac ile_trans 1,
-	  rtac ile_iSuc 1,
-	 dtac (iSuc_ile_mono RS iffD1) 1,
+	 dtac (thm "ileI1") 1,
+	 dtac (thm "ile_trans") 1,
+	  rtac (thm "ile_iSuc") 1,
+	 dtac (thm "iSuc_ile_mono" RS iffD1) 1,
 	 atac 1,
 	dtac mp 1,
 	 etac is_ub_thelub 1,
@@ -117,7 +117,7 @@
 	etac conjE 1,
 	case_tac "#x < Fin ia" 1,
 	 fast_tac HOL_cs 1,
-	fold_goals_tac [ile_def],
+	fold_goals_tac [thm "ile_def"],
 	mp_tac 1,
 	etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1,
 	etac ssubst 1,
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Thu May 31 20:52:51 2001 +0200
@@ -1,5 +1,5 @@
 (*  Title: 	HOLCF/ex/Stream_adm.thy
-    ID:         $ $
+    ID:         $Id$
     Author: 	David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
diff -r 9b80fe19407f -r 778c369559d9 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Thu May 31 18:28:23 2001 +0200
+++ b/src/HOLCF/ex/Stream.ML	Thu May 31 20:52:51 2001 +0200
@@ -384,7 +384,7 @@
 by (Simp_tac 1);
 by (stac Least_equality 1);
 by    Auto_tac;
-by (simp_tac(simpset() addsimps [Fin_0]) 1);
+by (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
 qed "slen_empty";
 
 Goalw [slen_def] "x ~= \\<bottom> ==> #(x&&xs) = iSuc (#xs)";
@@ -393,7 +393,7 @@
 by (rtac (split_if RS iffD2) 2);
 by  Safe_tac;
 by   (fast_tac (claset() addIs [stream_finite_lemma1]) 2);
-by  (rtac (iSuc_Infty RS sym) 2);
+by  (rtac (thm "iSuc_Infty" RS sym) 2);
 by (rtac (split_if RS iffD2) 1);
 by (Simp_tac 1);
 by Safe_tac;
@@ -409,8 +409,8 @@
 
 Goal "#x < Fin 1 = (x = UU)";
 by (stream_case_tac "x" 1);
-by (auto_tac (claset(), simpset() delsimps [iSuc_Fin] addsimps
- [Fin_0, iSuc_Fin RS sym,i0_iless_iSuc, iSuc_mono]));
+by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
+ [thm "Fin_0", thm "iSuc_Fin" RS sym, thm "i0_iless_iSuc", thm "iSuc_mono"]));
 qed "slen_less_1_eq";
 
 Goal "(#x = 0) = (x = \\<bottom>)";
@@ -422,8 +422,8 @@
 
 Goal "Fin (Suc n) < #x = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
 by (stream_case_tac "x" 1);
-by (auto_tac (claset(), simpset() delsimps [iSuc_Fin] addsimps
-                [iSuc_Fin RS sym, iSuc_mono]));
+by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
+                [thm "iSuc_Fin" RS sym, thm "iSuc_mono"]));
 by  (dtac sym 1);
 by  (rotate_tac 2 2);
 by  Auto_tac;
@@ -438,15 +438,15 @@
 
 Goal 
 "#x < Fin (Suc (Suc n)) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
-by (stac (iSuc_Fin RS sym) 1);
-by (stac (iSuc_Fin RS sym) 1);
+by (stac (thm "iSuc_Fin" RS sym) 1);
+by (stac (thm "iSuc_Fin" RS sym) 1);
 by (safe_tac HOL_cs);
 by  (rotate_tac ~1 1);
-by  (asm_full_simp_tac (HOL_ss addsimps [slen_scons, iSuc_mono]) 1);
+by  (asm_full_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1);
 by  (Asm_full_simp_tac 1);
 by (stream_case_tac "x" 1);
-by ( simp_tac (HOL_ss addsimps [slen_empty, i0_iless_iSuc]) 1);
-by (asm_simp_tac (HOL_ss addsimps [slen_scons, iSuc_mono]) 1);
+by ( simp_tac (HOL_ss addsimps [slen_empty, thm "i0_iless_iSuc"]) 1);
+by (asm_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1);
 by (etac allE 1);
 by (etac allE 1);
 by (safe_tac HOL_cs);
@@ -457,7 +457,7 @@
 
 Goal "!x. Fin n < #x = (stream_take n\\<cdot>x ~= x)";
 by (nat_ind_tac "n" 1);
-by  (simp_tac(simpset() addsimps [slen_empty_eq, Fin_0]) 1);
+by  (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1);
 by  (Fast_tac 1);
 by (rtac allI 1);
 by (asm_simp_tac (simpset() addsimps [slen_scons_eq]) 1);
@@ -469,7 +469,7 @@
 by Auto_tac;
 qed_spec_mp "slen_take_eq";
 
-Goalw [ile_def] "#x <= Fin n = (stream_take n\\<cdot>x = x)";
+Goalw [thm "ile_def"] "#x <= Fin n = (stream_take n\\<cdot>x = x)";
 by (simp_tac (simpset() addsimps [slen_take_eq]) 1);
 qed "slen_take_eq_rev";
 
@@ -479,10 +479,10 @@
 
 Goal "!x. ~stream_finite x --> #(stream_take i\\<cdot>x) = Fin i";
 by (nat_ind_tac "i" 1);
-by  (simp_tac(simpset() addsimps [Fin_0]) 1);
+by  (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
 by (rtac allI 1);
 by (stream_case_tac "x" 1);
-by  (auto_tac (claset()addSIs [stream_finite_lemma1], simpset() delsimps [iSuc_Fin] addsimps [iSuc_Fin RS sym]));
+by  (auto_tac (claset()addSIs [stream_finite_lemma1], simpset() delsimps [thm "iSuc_Fin"] addsimps [thm "iSuc_Fin" RS sym]));
 by (force_tac (claset(), simpset() addsimps [stream.finite_def]) 1);
 qed_spec_mp "slen_take_lemma2";
 
@@ -491,9 +491,9 @@
 by  (etac stream_finite_ind 1);
 by   (Simp_tac 1);
 by  (etac (slen_scons RS ssubst) 1);
-by  (stac (iSuc_Infty RS sym) 1);
+by  (stac (thm "iSuc_Infty" RS sym) 1);
 by  (etac contrapos_nn 1);
-by  (etac (iSuc_inject RS iffD1) 1);
+by  (etac (thm "iSuc_inject" RS iffD1) 1);
 by (case_tac "#x" 1);
 by (auto_tac (claset()addSDs [slen_take_lemma1],
         simpset() addsimps [stream.finite_def]));
@@ -510,9 +510,9 @@
 by  (Simp_tac 1);
 by (rtac allI 1);
 by (stream_case_tac "x" 1);
-by  (asm_simp_tac (HOL_ss addsimps [slen_empty, i0_lb]) 1);
+by  (asm_simp_tac (HOL_ss addsimps [slen_empty, thm "i0_lb"]) 1);
 by (asm_simp_tac (HOL_ss addsimps [slen_scons]) 1);
-by (fast_tac(claset() addSIs [iSuc_ile_mono RS iffD2] addSDs stream.inverts) 1);
+by (fast_tac(claset() addSIs [thm "iSuc_ile_mono" RS iffD2] addSDs stream.inverts) 1);
 qed "slen_mono";
 
 Goal "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> \
@@ -522,14 +522,14 @@
 by (strip_tac 1);
 by (stream_case_tac "x" 1);
 by  (asm_full_simp_tac (HOL_ss addsimps [slen_empty, 
-              iSuc_Fin RS sym, not_iSuc_ilei0]) 1);
+              thm "iSuc_Fin" RS sym, thm "not_iSuc_ilei0"]) 1);
 by (fatac stream_prefix 1 1);
 by (safe_tac (claset() addSDs [stream_flat_prefix]));
 by (Simp_tac 1);
 by (rtac cfun_arg_cong 1);
 by (rotate_tac 3 1);
-by (asm_full_simp_tac (simpset() delsimps [iSuc_Fin] addsimps 
-        [iSuc_Fin RS sym, iSuc_ile_mono]) 1);
+by (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] addsimps 
+        [thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1);
 qed_spec_mp "slen_take_lemma3";
 
 Goal "stream_finite t ==> \
@@ -548,7 +548,7 @@
 qed "slen_strict_mono_lemma";
 
 Goal "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t";
-by (rtac ilessI1 1);
+by (rtac (thm "ilessI1") 1);
 by  (etac slen_mono 1);
 by (dtac slen_strict_mono_lemma 1);
 by (Fast_tac 1);
@@ -559,12 +559,12 @@
 by  (Simp_tac 1);
 by (strip_tac 1);
 by (stream_case_tac "x" 1);
-by  (asm_full_simp_tac (simpset() delsimps [iSuc_Fin] 
-             addsimps [iSuc_Fin RS sym]) 1);
+by  (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] 
+             addsimps [thm "iSuc_Fin" RS sym]) 1);
 by (stac iterate_Suc2 1);
 by (rotate_tac 2 1);
-by (asm_full_simp_tac  (simpset() delsimps [iSuc_Fin] 
-    addsimps [iSuc_Fin RS sym, iSuc_ile_mono]) 1);
+by (asm_full_simp_tac  (simpset() delsimps [thm "iSuc_Fin"] 
+    addsimps [thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1);
 qed_spec_mp "slen_rt_mult";