--- a/TFL/rules.sml Thu Oct 12 18:09:06 2000 +0200
+++ b/TFL/rules.sml Thu Oct 12 18:38:23 2000 +0200
@@ -482,7 +482,7 @@
let val {prop, ...} = rep_thm thm
in case prop
of (Const("==>",_)$(Const("Trueprop",_)$ _) $
- (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
| _ => true
end;
@@ -685,7 +685,7 @@
end;
fun restricted t = is_some (S.find_term
- (fn (Const("WF.cut",_)) =>true | _ => false)
+ (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
--- a/TFL/thms.sml Thu Oct 12 18:09:06 2000 +0200
+++ b/TFL/thms.sml Thu Oct 12 18:38:23 2000 +0200
@@ -17,9 +17,9 @@
structure Thms: Thms_sig =
struct
- val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
- val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
- val CUT_DEF = get_thm WF.thy "cut_def";
+ val WFREC_COROLLARY = get_thm Wellfounded_Recursion.thy "tfl_wfrec";
+ val WF_INDUCTION_THM = get_thm Wellfounded_Recursion.thy "tfl_wf_induct";
+ val CUT_DEF = get_thm Wellfounded_Recursion.thy "cut_def";
val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
(fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
--- a/TFL/usyntax.sml Thu Oct 12 18:09:06 2000 +0200
+++ b/TFL/usyntax.sml Thu Oct 12 18:38:23 2000 +0200
@@ -407,7 +407,7 @@
mesg="unexpected term structure"} (* FIXME do not handle _ !!! *)
else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
-fun is_WFR (Const("WF.wf",_)$_) = true
+fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
--- a/doc-src/TutorialI/CTL/CTL.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Thu Oct 12 18:38:23 2000 +0200
@@ -2,7 +2,7 @@
subsection{*Computation tree logic---CTL*};
-text{*
+text{*\label{sec:CTL}
The semantics of PDL only needs transitive reflexive closure.
Let us now be a bit more adventurous and introduce a new temporal operator
that goes beyond transitive reflexive closure. We extend the datatype
@@ -266,16 +266,20 @@
apply(fast intro:someI2_ex);
txt{*\noindent
-What is worth noting here is that we have used @{text fast} rather than @{text blast}.
-The reason is that @{text blast} would fail because it cannot cope with @{thm[source]someI2_ex}:
-unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
-variables. For efficiency reasons @{text blast} does not even attempt such unifications.
-Although @{text fast} can in principle cope with complicated unification problems, in practice
-the number of unifiers arising is often prohibitive and the offending rule may need to be applied
-explicitly rather than automatically.
+What is worth noting here is that we have used @{text fast} rather than
+@{text blast}. The reason is that @{text blast} would fail because it cannot
+cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
+subgoal is nontrivial because of the nested schematic variables. For
+efficiency reasons @{text blast} does not even attempt such unifications.
+Although @{text fast} can in principle cope with complicated unification
+problems, in practice the number of unifiers arising is often prohibitive and
+the offending rule may need to be applied explicitly rather than
+automatically. This is what happens in the step case.
-The induction step is similar, but more involved, because now we face nested occurrences of
-@{text SOME}. We merely show the proof commands but do not describe th details:
+The induction step is similar, but more involved, because now we face nested
+occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
+solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely
+show the proof commands but do not describe the details:
*};
apply(simp);
@@ -397,53 +401,4 @@
a fixpoint is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.
*}
-
-(*<*)
-(*
-Second proof of opposite direction, directly by wellfounded induction
-on the initial segment of M that avoids A.
-
-Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path
-*)
-
-consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
-inductive "Avoid s A"
-intros "s \<in> Avoid s A"
- "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
-
-(* For any infinite A-avoiding path (f) in Avoid s A,
- there is some infinite A-avoiding path (p) in Avoid s A that starts with s.
-*)
-lemma ex_infinite_path[rule_format]:
-"t \<in> Avoid s A \<Longrightarrow>
- \<forall>f. t = f 0 \<longrightarrow> (\<forall>i. (f i, f (Suc i)) \<in> M \<and> f i \<in> Avoid s A \<and> f i \<notin> A)
- \<longrightarrow> (\<exists> p\<in>Paths s. \<forall>i. p i \<notin> A)";
-apply(simp add:Paths_def);
-apply(erule Avoid.induct);
- apply(blast);
-apply(rule allI);
-apply(erule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in allE);
-by(force split:nat.split);
-
-lemma Avoid_in_lfp[rule_format(no_asm)]:
-"\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
-apply(subgoal_tac "wf{(y,x). (x,y)\<in>M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}");
- apply(erule_tac a = t in wf_induct);
- apply(clarsimp);
- apply(rule ssubst [OF lfp_unfold[OF mono_af]]);
- apply(unfold af_def);
- apply(blast intro:Avoid.intros);
-apply(erule contrapos2);
-apply(simp add:wf_iff_no_infinite_down_chain);
-apply(erule exE);
-apply(rule ex_infinite_path);
-by(auto);
-
-theorem AF_lemma2:
-"{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
-apply(rule subsetI);
-apply(simp);
-apply(erule Avoid_in_lfp);
-by(rule Avoid.intros);
-
-end(*>*)
+(*<*)end(*>*)
--- a/doc-src/TutorialI/CTL/PDL.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy Thu Oct 12 18:38:23 2000 +0200
@@ -118,11 +118,10 @@
\ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
\end{isabelle}
-which is proved by @{text blast} with the help of a few lemmas about
-@{text"^*"}:
+which is proved by @{text blast} with the help of transitivity of @{text"^*"}:
*}
- apply(blast intro: r_into_rtrancl rtrancl_trans);
+ apply(blast intro: rtrancl_trans);
txt{*
We now return to the second set containment subgoal, which is again proved
--- a/doc-src/TutorialI/CTL/ROOT.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/ROOT.ML Thu Oct 12 18:38:23 2000 +0200
@@ -1,3 +1,4 @@
use "../settings.ML";
use_thy "PDL";
use_thy "CTL";
+use_thy "CTLind";
--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Oct 12 18:38:23 2000 +0200
@@ -197,16 +197,20 @@
\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-What is worth noting here is that we have used \isa{fast} rather than \isa{blast}.
-The reason is that \isa{blast} would fail because it cannot cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
-unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
-variables. For efficiency reasons \isa{blast} does not even attempt such unifications.
-Although \isa{fast} can in principle cope with complicated unification problems, in practice
-the number of unifiers arising is often prohibitive and the offending rule may need to be applied
-explicitly rather than automatically.
+What is worth noting here is that we have used \isa{fast} rather than
+\isa{blast}. The reason is that \isa{blast} would fail because it cannot
+cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
+subgoal is nontrivial because of the nested schematic variables. For
+efficiency reasons \isa{blast} does not even attempt such unifications.
+Although \isa{fast} can in principle cope with complicated unification
+problems, in practice the number of unifiers arising is often prohibitive and
+the offending rule may need to be applied explicitly rather than
+automatically. This is what happens in the step case.
-The induction step is similar, but more involved, because now we face nested occurrences of
-\isa{SOME}. We merely show the proof commands but do not describe th details:%
+The induction step is similar, but more involved, because now we face nested
+occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to
+solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand. We merely
+show the proof commands but do not describe the details:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/CTL/document/PDL.tex Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Thu Oct 12 18:38:23 2000 +0200
@@ -113,10 +113,9 @@
\ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
\end{isabelle}
-which is proved by \isa{blast} with the help of a few lemmas about
-\isa{{\isacharcircum}{\isacharasterisk}}:%
+which is proved by \isa{blast} with the help of transitivity of \isa{{\isacharcircum}{\isacharasterisk}}:%
\end{isamarkuptxt}%
-\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ r{\isacharunderscore}into{\isacharunderscore}rtrancl\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
+\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
\begin{isamarkuptxt}%
We now return to the second set containment subgoal, which is again proved
pointwise:%
--- a/doc-src/TutorialI/IsaMakefile Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile Thu Oct 12 18:38:23 2000 +0200
@@ -106,7 +106,7 @@
HOL-CTL: HOL $(LOG)/HOL-CTL.gz
-$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
+$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
@rm -f tutorial.dvi
@@ -126,4 +126,4 @@
## clean
clean:
- @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz
+ @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz
--- a/doc-src/TutorialI/Recdef/Nested2.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Thu Oct 12 18:38:23 2000 +0200
@@ -66,10 +66,9 @@
@{thm[display,margin=50]"map_cong"[no_vars]}
Its second premise expresses (indirectly) that the second argument of
@{term"map"} is only applied to elements of its third argument. Congruence
-rules for other higher-order functions on lists would look very similar but
-have not been proved yet because they were never needed. If you get into a
-situation where you need to supply \isacommand{recdef} with new congruence
-rules, you can either append a hint locally
+rules for other higher-order functions on lists look very similar. If you get
+into a situation where you need to supply \isacommand{recdef} with new
+congruence rules, you can either append a hint locally
to the specific occurrence of \isacommand{recdef}
*}
(*<*)
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Oct 12 18:38:23 2000 +0200
@@ -66,10 +66,9 @@
\end{isabelle}
Its second premise expresses (indirectly) that the second argument of
\isa{map} is only applied to elements of its third argument. Congruence
-rules for other higher-order functions on lists would look very similar but
-have not been proved yet because they were never needed. If you get into a
-situation where you need to supply \isacommand{recdef} with new congruence
-rules, you can either append a hint locally
+rules for other higher-order functions on lists look very similar. If you get
+into a situation where you need to supply \isacommand{recdef} with new
+congruence rules, you can either append a hint locally
to the specific occurrence of \isacommand{recdef}%
\end{isamarkuptext}%
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
--- a/doc-src/TutorialI/todo.tobias Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias Thu Oct 12 18:38:23 2000 +0200
@@ -15,8 +15,6 @@
swap in classical.ML has ugly name Pa in it. Rename.
-list of ^*/^+ intro rules. Incl transitivity?
-
Induction rules for int: int_le/ge_induct?
Needed for ifak example. But is that example worth it?
--- a/doc-src/TutorialI/tutorial.tex Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex Thu Oct 12 18:38:23 2000 +0200
@@ -67,7 +67,7 @@
\input{fp}
\chapter{The Rules of the Game}
\input{sets}
-\chapter{Inductively Defined Sets}
+\input{Inductive/inductive}
\input{Advanced/advanced}
\chapter{More about Types}
\chapter{Theory Presentation}
--- a/src/HOL/Datatype.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Datatype.thy Thu Oct 12 18:38:23 2000 +0200
@@ -4,7 +4,7 @@
Copyright 1998 TU Muenchen
*)
-Datatype = Univ +
+Datatype = Datatype_Universe +
rep_datatype bool
distinct True_not_False, False_not_True
--- a/src/HOL/Divides.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Divides.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
The division operators div, mod and the divides relation "dvd"
*)
-Divides = Arith +
+Divides = Arithmetic +
(*We use the same class for div and mod;
moreover, dvd is defined whenever multiplication is*)
--- a/src/HOL/Fun.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Fun.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
Notions about functions.
*)
-Fun = Vimage + equalities +
+Fun = Inverse_Image + equalities +
instance set :: (term) order
(subset_refl,subset_trans,subset_antisym,psubset_eq)
--- a/src/HOL/IOA/Asig.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/IOA/Asig.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
Action signatures
*)
-Asig = Prod +
+Asig = Product_Type +
types
--- a/src/HOL/Induct/Comb.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Induct/Comb.ML Thu Oct 12 18:38:23 2000 +0200
@@ -65,12 +65,12 @@
Goal "x ---> y ==> x#z ---> y#z";
by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
+by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
qed "Ap_reduce1";
Goal "x ---> y ==> z#x ---> z#y";
by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
+by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
qed "Ap_reduce2";
(** Counterexample to the diamond property for -1-> **)
--- a/src/HOL/Induct/LList.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Induct/LList.ML Thu Oct 12 18:38:23 2000 +0200
@@ -782,7 +782,7 @@
by (ALLGOALS Asm_simp_tac);
qed "fun_power_Suc";
-val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
+val Pair_cong = read_instantiate_sg (sign_of Product_Type.thy)
[("f","Pair")] (standard(refl RS cong RS cong));
(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
--- a/src/HOL/Induct/Sexp.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Induct/Sexp.thy Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
structures by hand.
*)
-Sexp = Univ + Inductive +
+Sexp = Datatype_Universe + Inductive +
consts
sexp :: 'a item set
--- a/src/HOL/Inductive.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Inductive.thy Thu Oct 12 18:38:23 2000 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-theory Inductive = Gfp + Prod + Sum + NatDef
+theory Inductive = Gfp + Sum_Type + NatDef
files
"Tools/induct_method.ML"
"Tools/inductive_package.ML"
--- a/src/HOL/Integ/IntDef.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Integ/IntDef.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
The integers as equivalence classes over nat*nat.
*)
-IntDef = Equiv + Arith +
+IntDef = Equiv + Arithmetic +
constdefs
intrel :: "((nat * nat) * (nat * nat)) set"
"intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
--- a/src/HOL/IsaMakefile Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/IsaMakefile Thu Oct 12 18:38:23 2000 +0200
@@ -69,7 +69,7 @@
$(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
$(SRC)/TFL/rules.sml $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml \
$(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml \
- Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML \
+ Arithmetic.ML Arithmetic.thy Calculation.thy Datatype.thy Divides.ML \
Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
@@ -80,17 +80,17 @@
Integ/int_arith2.ML Integ/nat_simprocs.ML Lfp.ML Lfp.thy List.ML \
List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
- Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy \
- RelPow.ML RelPow.thy Relation.ML Relation.thy Set.ML Set.thy \
+ Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+ Relation_Power.ML Relation_Power.thy Relation.ML Relation.thy Set.ML Set.thy \
SetInterval.ML SetInterval.thy String.thy SVC_Oracle.ML \
- SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
+ SVC_Oracle.thy Sum_Type.ML Sum_Type.thy Tools/datatype_aux.ML \
Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
Tools/induct_method.ML Tools/inductive_package.ML Tools/meson.ML \
Tools/numeral_syntax.ML Tools/primrec_package.ML \
Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
- Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
- Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy While.ML \
+ Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy Datatype_Universe.ML Datatype_Universe.thy \
+ Inverse_Image.ML Inverse_Image.thy Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML Wellfounded_Relations.thy While.ML \
While.thy arith_data.ML blastdata.ML cladata.ML equalities.ML \
equalities.thy hologic.ML meson_lemmas.ML mono.ML mono.thy simpdata.ML \
subset.ML subset.thy thy_syntax.ML
--- a/src/HOL/Lambda/Commutation.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Lambda/Commutation.thy Thu Oct 12 18:38:23 2000 +0200
@@ -132,7 +132,7 @@
rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
apply (erule rtrancl_induct)
apply blast
- apply (blast del: rtrancl_refl intro: rtranclIs)
+ apply (blast del: rtrancl_refl intro: rtrancl_trans)
done
end
--- a/src/HOL/Lfp.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Lfp.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
The Knaster-Tarski Theorem
*)
-Lfp = mono + Prod +
+Lfp = mono + Product_Type +
constdefs
lfp :: ['a set=>'a set] => 'a set
--- a/src/HOL/MicroJava/J/JBasis.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.ML Thu Oct 12 18:38:23 2000 +0200
@@ -13,19 +13,19 @@
fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
-val select_split = prove_goalw Prod.thy [split_def]
+val select_split = prove_goalw Product_Type.thy [split_def]
"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
-val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
+val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
-val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
+val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
(fn _ => [Auto_tac]);
-val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
+val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
rtac (split_beta RS subst) 1,
rtac (hd prems) 1]);
-val splitE2' = prove_goal Prod.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
+val splitE2' = prove_goal Product_Type.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
res_inst_tac [("P1","P")] (split_beta RS subst) 1,
rtac (hd prems) 1]);
@@ -131,11 +131,11 @@
by(simp_tac (simpset() addsimps image_def::premises()) 1);
qed "image_cong";
-val split_Pair_eq = prove_goal Prod.thy
+val split_Pair_eq = prove_goal Product_Type.thy
"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
etac imageE 1,
split_all_tac 1,
- auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
+ auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]);
(* More about Maps *)
--- a/src/HOL/Modelcheck/MuckeSyn.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Thu Oct 12 18:38:23 2000 +0200
@@ -147,7 +147,7 @@
(* first simplification, then model checking *)
-goalw Prod.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
+goalw Product_Type.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
by (rtac ext 1);
by (stac (surjective_pairing RS sym) 1);
by (rtac refl 1);
--- a/src/HOL/NatDef.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/NatDef.thy Thu Oct 12 18:38:23 2000 +0200
@@ -8,7 +8,7 @@
Type nat is defined as a set Nat over type ind.
*)
-NatDef = WF +
+NatDef = Wellfounded_Recursion +
(** type ind **)
--- a/src/HOL/PreList.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/PreList.thy Thu Oct 12 18:38:23 2000 +0200
@@ -8,8 +8,8 @@
*)
theory PreList =
- Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation +
- SVC_Oracle + While:
+ Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
+ Relation_Power + Calculation + SVC_Oracle + While:
theorems [cases type: bool] = case_split
--- a/src/HOL/Real/Hyperreal/Series.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Series.ML Thu Oct 12 18:38:23 2000 +0200
@@ -94,9 +94,9 @@
[real_minus_add_distrib]));
qed "sumr_minus";
-context Arith.thy;
+context Arithmetic.thy;
-goal Arith.thy "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
+Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
by (auto_tac (claset() addSDs [not_leE],simpset()));
qed "lemma_not_Suc_add";
--- a/src/HOL/Recdef.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Recdef.thy Thu Oct 12 18:38:23 2000 +0200
@@ -5,7 +5,7 @@
TFL: recursive function definitions.
*)
-theory Recdef = WF_Rel + Datatype
+theory Recdef = Wellfounded_Relations + Datatype
files
"../TFL/utils.sml"
"../TFL/usyntax.sml"
--- a/src/HOL/Relation.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Relation.thy Thu Oct 12 18:38:23 2000 +0200
@@ -4,7 +4,7 @@
Copyright 1996 University of Cambridge
*)
-Relation = Prod +
+Relation = Product_Type +
constdefs
converse :: "('a*'b) set => ('b*'a) set" ("(_^-1)" [1000] 999)
--- a/src/HOL/SetInterval.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/SetInterval.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
lessThan, greaterThan, atLeast, atMost
*)
-SetInterval = equalities + Arith +
+SetInterval = equalities + Arithmetic +
constdefs
lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")
--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 12 18:38:23 2000 +0200
@@ -417,7 +417,7 @@
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
- val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
val size_names = replicate (length (hd descr)) size_name @
map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
(map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
--- a/src/HOL/Tools/datatype_package.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML Thu Oct 12 18:38:23 2000 +0200
@@ -715,7 +715,7 @@
val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
[descr] sorts thy7;
val (thy9, size_thms) =
- if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
+ if exists (equal "Arithmetic") (Sign.stamp_names_of (Theory.sign_of thy8)) then
DatatypeAbsProofs.prove_size_thms false new_type_names
[descr] sorts reccomb_names rec_thms thy8
else (thy8, []);
--- a/src/HOL/Tools/datatype_prop.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Thu Oct 12 18:38:23 2000 +0200
@@ -398,7 +398,7 @@
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
- val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
val size_names = replicate (length (hd descr)) size_name @
map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
(map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
--- a/src/HOL/Tools/inductive_package.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Oct 12 18:38:23 2000 +0200
@@ -185,7 +185,7 @@
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
-val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "vimage";
+val vimage_name = Sign.intern_const (Theory.sign_of Inverse_Image.thy) "vimage";
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
(* make injections needed in mutually recursive definitions *)
--- a/src/HOL/UNITY/Reach.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/UNITY/Reach.ML Thu Oct 12 18:38:23 2000 +0200
@@ -31,7 +31,7 @@
Goal "Rprg : Always reach_invariant";
by (always_tac 1);
-by (blast_tac (claset() addIs rtranclIs) 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
qed "reach_invariant";
@@ -42,7 +42,7 @@
"fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
by (rtac equalityI 1);
by (auto_tac (claset() addSIs [ext], simpset()));
-by (blast_tac (claset() addIs rtranclIs) 2);
+by (blast_tac (claset() addIs [rtrancl_trans]) 2);
by (etac rtrancl_induct 1);
by Auto_tac;
qed "fixedpoint_invariant_correct";
--- a/src/HOL/ex/PiSets.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/PiSets.thy Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
Also the nice -> operator for function space
*)
-PiSets = Univ + Finite +
+PiSets = Datatype_Universe + Finite +
syntax
"->" :: "['a set, 'b set] => ('a => 'b) set" (infixr 60)
--- a/src/HOL/ex/cla.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/cla.ML Thu Oct 12 18:38:23 2000 +0200
@@ -462,7 +462,7 @@
(*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
Fast_tac indeed copes!*)
-goal Prod.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
+goal Product_Type.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \
\ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) & J(x))";
by (Fast_tac 1);
@@ -470,7 +470,7 @@
(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
It does seem obvious!*)
-goal Prod.thy
+goal Product_Type.thy
"(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \
\ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))";
@@ -488,7 +488,7 @@
by (Blast_tac 1);
result();
-goal Prod.thy
+goal Product_Type.thy
"(ALL x y. R(x,y) | R(y,x)) & \
\ (ALL x y. S(x,y) & S(y,x) --> x=y) & \
\ (ALL x y. R(x,y) --> S(x,y)) --> (ALL x y. S(x,y) --> R(x,y))";
--- a/src/HOL/ex/mesontest2.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/mesontest2.ML Thu Oct 12 18:38:23 2000 +0200
@@ -11,9 +11,9 @@
(*All but the fastest are ignored to reduce build time*)
val even_hard_ones = false;
-(*Prod.thy instead of HOL.thy regards arguments as tuples.
+(*Product_Type.thy instead of HOL.thy regards arguments as tuples.
But Main.thy would allow clashes with many other constants*)
-fun prove (s,tac) = prove_goal Prod.thy s (fn [] => [tac]);
+fun prove (s,tac) = prove_goal Product_Type.thy s (fn [] => [tac]);
fun prove_hard arg = if even_hard_ones then prove arg else TrueI;
--- a/src/HOLCF/Cprod1.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/Cprod1.ML Thu Oct 12 18:38:23 2000 +0200
@@ -3,7 +3,7 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Partial ordering for cartesian product of HOL theory Prod.thy
+Partial ordering for cartesian product of HOL theory Product_Type.thy
*)
@@ -15,7 +15,7 @@
by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
by (rotate_tac ~1 1);
by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
-by (asm_simp_tac (simpset_of Prod.thy) 1);
+by (asm_simp_tac (simpset_of Product_Type.thy) 1);
qed "Sel_injective_cprod";
Goalw [less_cprod_def] "(p::'a*'b) << p";
--- a/src/HOLCF/IOA/ABP/Lemmas.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,4 +6,4 @@
Arithmetic lemmas
*)
-Lemmas = Arith
+Lemmas = Arithmetic
--- a/src/HOLCF/IOA/ABP/Packet.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/ABP/Packet.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
Packets
*)
-Packet = Arith +
+Packet = Arithmetic +
types
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Thu Oct 12 18:38:23 2000 +0200
@@ -35,7 +35,7 @@
(* Arithmetic *)
-goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
+goal Arithmetic.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
qed "pred_suc";
--- a/src/HOLCF/IOA/NTP/Lemmas.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,4 +6,4 @@
Arithmetic lemmas
*)
-Lemmas = Arith
+Lemmas = Arithmetic
--- a/src/HOLCF/IOA/NTP/Multiset.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
Should be done as a subtype and moved to a global place.
*)
-Multiset = Arith + Lemmas +
+Multiset = Lemmas +
types
--- a/src/HOLCF/IOA/NTP/Packet.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Packet.thy Thu Oct 12 18:38:23 2000 +0200
@@ -6,7 +6,7 @@
Packets
*)
-Packet = Arith + Multiset +
+Packet = Multiset +
types
--- a/src/HOLCF/Up1.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOLCF/Up1.thy Thu Oct 12 18:38:23 2000 +0200
@@ -8,7 +8,7 @@
*)
-Up1 = Cfun3 + Sum + Datatype +
+Up1 = Cfun3 + Sum_Type + Datatype +
(* new type for lifting *)