--- 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"
--- /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
+}
--- 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}
--- 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
--- 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
-
-
-
--- 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)
*)
--- 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)
--- 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";
--- 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)
--- 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];
--- 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)
--- 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)
*)
--- 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)
--- 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)
--- 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,
--- 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)
--- 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";