--- a/src/CCL/CCL.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/CCL.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ccl
+(* Title: CCL/ccl
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For ccl.thy.
@@ -89,7 +89,7 @@
| arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
val sg = sign_of thy;
val T = case Sign.const_type sg sy of
- None => error(sy^" not declared") | Some(T) => T;
+ None => error(sy^" not declared") | Some(T) => T;
val arity = length (fst (strip_type T));
in sy ^ (arg_str arity name "") end;
--- a/src/CCL/Fix.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Fix.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/fix
+(* Title: CCL/fix
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For fix.thy.
--- a/src/CCL/Gfp.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Gfp.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,9 +1,9 @@
-(* Title: CCL/gfp
+(* Title: CCL/gfp
ID: $Id$
Modified version of
- Title: HOL/gfp
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Title: HOL/gfp
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For gfp.thy. The Knaster-Tarski Theorem for greatest fixed points.
@@ -28,12 +28,12 @@
val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
- rtac (mono RS monoD), rtac gfp_upperbound, atac]);
+ rtac (mono RS monoD), rtac gfp_upperbound, atac]);
qed "gfp_lemma2";
val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD),
- rtac gfp_lemma2, rtac mono]);
+ rtac gfp_lemma2, rtac mono]);
qed "gfp_lemma3";
val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
--- a/src/CCL/Hered.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Hered.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/hered
+(* Title: CCL/hered
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For hered.thy.
--- a/src/CCL/Lfp.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Lfp.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,9 +1,9 @@
-(* Title: CCL/lfp
+(* Title: CCL/lfp
ID: $Id$
Modified version of
- Title: HOL/lfp.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Title: HOL/lfp.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
For lfp.thy. The Knaster-Tarski Theorem
@@ -28,12 +28,12 @@
val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
- rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
+ rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
qed "lfp_lemma2";
val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD),
- rtac lfp_lemma2, rtac mono]);
+ rtac lfp_lemma2, rtac mono]);
qed "lfp_lemma3";
val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
@@ -44,15 +44,15 @@
(*** General induction rule for least fixed points ***)
val [lfp,mono,indhyp] = goal Lfp.thy
- "[| a: lfp(f); mono(f); \
-\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \
+ "[| a: lfp(f); mono(f); \
+\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
by (EVERY1 [rtac Int_greatest, rtac subset_trans,
- rtac (Int_lower1 RS (mono RS monoD)),
- rtac (mono RS lfp_lemma2),
- rtac (CollectI RS subsetI), rtac indhyp, atac]);
+ rtac (Int_lower1 RS (mono RS monoD)),
+ rtac (mono RS lfp_lemma2),
+ rtac (CollectI RS subsetI), rtac indhyp, atac]);
qed "induct";
(** Definition forms of lfp_Tarski and induct, to control unfolding **)
@@ -63,11 +63,11 @@
qed "def_lfp_Tarski";
val rew::prems = goal Lfp.thy
- "[| A == lfp(f); a:A; mono(f); \
-\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \
+ "[| A == lfp(f); a:A; mono(f); \
+\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
-by (EVERY1 [rtac induct, (*backtracking to force correct induction*)
- REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
+by (EVERY1 [rtac induct, (*backtracking to force correct induction*)
+ REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
qed "def_induct";
(*Monotonicity of lfp!*)
--- a/src/CCL/Set.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Set.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,11 +1,11 @@
-(* Title: set/set
+(* Title: set/set
ID: $Id$
For set.thy.
Modified version of
- Title: HOL/set
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Title: HOL/set
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
For set.thy. Set theory for higher-order logic. A set is simply a predicate.
@@ -282,7 +282,7 @@
\ (UN x:A. C(x)) = (UN x:B. D(x))";
by (REPEAT (etac UN_E 1
ORELSE ares_tac ([UN_I,equalityI,subsetI] @
- (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
+ (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
qed "UN_cong";
(*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *)
--- a/src/CCL/Term.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Term.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/terms
+(* Title: CCL/terms
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For terms.thy.
@@ -57,12 +57,12 @@
fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
(fn _ => [rtac (letrecB RS ssubst) 1,
- simp_tac (CCL_ss addsimps rawBs) 1]);
+ simp_tac (CCL_ss addsimps rawBs) 1]);
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
(fn _ => [simp_tac (CCL_ss addsimps rawBs
- setloop (rtac (letrecB RS ssubst))) 1]);
+ setloop (rtac (letrecB RS ssubst))) 1]);
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
val ifBtrue = mk_beta_rl "if true then t else u = t";
@@ -116,7 +116,7 @@
(*** Constructors are injective ***)
val term_injs = map (mk_inj_rl Term.thy
- [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
+ [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
--- a/src/CCL/Trancl.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Trancl.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,11 +1,11 @@
-(* Title: CCL/trancl
+(* Title: CCL/trancl
ID: $Id$
For trancl.thy.
Modified version of
- Title: HOL/trancl.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Title: HOL/trancl.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
@@ -66,8 +66,8 @@
qed "compEpair";
val comp_cs = set_cs addIs [compI,idI]
- addEs [compE,idE]
- addSEs [pair_inject];
+ addEs [compE,idE]
+ addSEs [pair_inject];
val prems = goal Trancl.thy
"[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
@@ -120,7 +120,7 @@
val major::prems = goal Trancl.thy
"[| <a,b> : r^*; \
\ P(a); \
-\ !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) |] \
+\ !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) |] \
\ ==> P(b)";
(*by induction on this formula*)
by (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)" 1);
@@ -142,7 +142,7 @@
(*elimination of rtrancl -- by induction on a special formula*)
val major::prems = goal Trancl.thy
"[| <a,b> : r^*; (a = b) ==> P; \
-\ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
+\ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
\ ==> P";
by (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r)" 1);
by (rtac (major RS rtrancl_induct) 2);
@@ -188,7 +188,7 @@
val major::prems = goal Trancl.thy
"[| <a,b> : r^+; \
\ <a,b> : r ==> P; \
-\ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \
+\ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \
\ |] ==> P";
by (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r)" 1);
by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
--- a/src/CCL/Type.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Type.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/types
+(* Title: CCL/types
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
For types.thy.
--- a/src/CCL/Wfd.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/Wfd.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,11 +1,11 @@
-(* Title: CCL/wfd.ML
+(* Title: CCL/wfd.ML
ID: $Id$
For wfd.thy.
Based on
- Titles: ZF/wf.ML and HOL/ex/lex-prod
- Authors: Lawrence C Paulson and Tobias Nipkow
+ Titles: ZF/wf.ML and HOL/ex/lex-prod
+ Authors: Lawrence C Paulson and Tobias Nipkow
Copyright 1992 University of Cambridge
*)
--- a/src/CCL/coinduction.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/coinduction.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: 92/CCL/coinduction
+(* Title: 92/CCL/coinduction
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Lemmas and tactics for using the rule coinduct3 on [= and =.
--- a/src/CCL/equalities.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/equalities.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,9 +1,9 @@
-(* Title: CCL/equalities
+(* Title: CCL/equalities
ID: $Id$
Modified version of
- Title: HOL/equalities
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Title: HOL/equalities
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Equalities involving union, intersection, inclusion, etc.
--- a/src/CCL/eval.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/eval.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: 92/CCL/eval
+(* Title: 92/CCL/eval
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/CCL/ex/Flag.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/ex/Flag.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/flag
+(* Title: CCL/ex/flag
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For flag.thy.
@@ -35,8 +35,8 @@
"flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)";
by (typechk_tac [redT,whiteT,blueT,ccaseT] 1);
by clean_ccs_tac;
-be (ListPRI RS (ListPR_wf RS wfI)) 1;
-ba 1;
+by (etac (ListPRI RS (ListPR_wf RS wfI)) 1);
+by (assume_tac 1);
result();
--- a/src/CCL/ex/List.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/ex/List.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/list
+(* Title: CCL/ex/list
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For list.thy.
@@ -32,12 +32,12 @@
(****)
val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
-br (prem RS Nat_ind) 1;
+by (rtac (prem RS Nat_ind) 1);
by (ALLGOALS (asm_simp_tac list_ss));
qed "nmapBnil";
val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
-br (prem RS Nat_ind) 1;
+by (rtac (prem RS Nat_ind) 1);
by (ALLGOALS (asm_simp_tac list_ss));
qed "nmapBcons";
@@ -85,8 +85,8 @@
"[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)";
by (typechk_tac prems 1);
by clean_ccs_tac;
-br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2;
-br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1;
+by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2);
+by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1);
by (REPEAT (atac 1));
qed "partitionT";
--- a/src/CCL/ex/Nat.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/ex/Nat.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/nat
+(* Title: CCL/ex/nat
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For nat.thy.
@@ -25,7 +25,7 @@
(*** Lemma for napply ***)
val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
-br (prem RS Nat_ind) 1;
+by (rtac (prem RS Nat_ind) 1);
by (ALLGOALS (asm_simp_tac nat_ss));
qed "napply_f";
@@ -43,13 +43,13 @@
val prems = goalw Nat.thy [sub_def] "[| a:Nat; b:Nat |] ==> a #- b : Nat";
by (typechk_tac (prems) 1);
by clean_ccs_tac;
-be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
+by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1);
qed "subT";
val prems = goalw Nat.thy [le_def] "[| a:Nat; b:Nat |] ==> a #<= b : Bool";
by (typechk_tac (prems) 1);
by clean_ccs_tac;
-be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
+by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1);
qed "leT";
val prems = goalw Nat.thy [not_def,lt_def] "[| a:Nat; b:Nat |] ==> a #< b : Bool";
--- a/src/CCL/ex/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/ex/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -6,7 +6,7 @@
Executes all examples for Classical Computational Logic
*)
-CCL_build_completed; (*Cause examples to fail if CCL did*)
+CCL_build_completed; (*Cause examples to fail if CCL did*)
writeln"Root file for CCL examples";
proof_timing := true;
--- a/src/CCL/ex/Stream.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/ex/Stream.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/stream
+(* Title: CCL/ex/stream
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
For stream.thy.
@@ -19,7 +19,7 @@
"{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
-be (XH_to_E ListsXH) 1;
+by (etac (XH_to_E ListsXH) 1);
by (EQgen_tac list_ss [] 1);
by (simp_tac list_ss 1);
by (fast_tac ccl_cs 1);
@@ -32,7 +32,7 @@
"{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(%x.x,l) & y=l)}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
-be (XH_to_E ListsXH) 1;
+by (etac (XH_to_E ListsXH) 1);
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 1);
qed "map_id";
@@ -45,9 +45,9 @@
\ x=map(f,l@m) & y=map(f,l) @ map(f,m))}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
-be (XH_to_E ListsXH) 1;
+by (etac (XH_to_E ListsXH) 1);
by (EQgen_tac list_ss [] 1);
-be (XH_to_E ListsXH) 1;
+by (etac (XH_to_E ListsXH) 1);
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 1);
qed "map_append";
@@ -61,7 +61,7 @@
\ x=k @ l @ m & y=(k @ l) @ m)}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac type_cs);
-be (XH_to_E ListsXH) 1;
+by (etac (XH_to_E ListsXH) 1);
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 2);
by (DEPTH_SOLVE (etac (XH_to_E ListsXH) 1 THEN EQgen_tac list_ss [] 1));
@@ -74,7 +74,7 @@
"{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1);
by (fast_tac (ccl_cs addSIs prems) 1);
by (safe_tac set_cs);
-be (XH_to_E IListsXH) 1;
+by (etac (XH_to_E IListsXH) 1);
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 1);
qed "ilist_append";
@@ -85,13 +85,13 @@
(* fun iter2(f,a) = a$map(f,iter2(f,a)) *)
goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
-br (letrecB RS trans) 1;
+by (rtac (letrecB RS trans) 1);
by (simp_tac term_ss 1);
qed "iter1B";
goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
-br (letrecB RS trans) 1;
-br refl 1;
+by (rtac (letrecB RS trans) 1);
+by (rtac refl 1);
qed "iter2B";
val [prem] =goal Stream.thy
@@ -106,7 +106,7 @@
"{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
1);
by (fast_tac (type_cs addSIs [napplyBzero RS sym,
- napplyBzero RS sym RS arg_cong]) 1);
+ napplyBzero RS sym RS arg_cong]) 1);
by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
by (rtac (napply_f RS ssubst) 1 THEN atac 1);
by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
--- a/src/CCL/genrec.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/genrec.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: 92/CCL/genrec
+(* Title: 92/CCL/genrec
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
--- a/src/CCL/mono.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/mono.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,9 +1,9 @@
-(* Title: CCL/mono
+(* Title: CCL/mono
ID: $Id$
Modified version of
- Title: HOL/mono
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Title: HOL/mono
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Monotonicity of various operations
--- a/src/CCL/subset.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/subset.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,9 +1,9 @@
-(* Title: CCL/subset
+(* Title: CCL/subset
ID: $Id$
Modified version of
- Title: HOL/subset
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Title: HOL/subset
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Derived rules involving subsets
@@ -99,10 +99,10 @@
val set_cs = FOL_cs
addSIs [ballI, subsetI, InterI, INT_I, CollectI,
- ComplI, IntI, UnCI, singletonI]
+ ComplI, IntI, UnCI, singletonI]
addIs [bexI, UnionI, UN_I]
addSEs [bexE, UnionE, UN_E,
- CollectE, ComplE, IntE, UnE, emptyE, singletonE]
+ CollectE, ComplE, IntE, UnE, emptyE, singletonE]
addEs [ballE, InterD, InterE, INT_D, INT_E, subsetD, subsetCE];
fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
--- a/src/CCL/typecheck.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CCL/typecheck.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/typecheck
+(* Title: CCL/typecheck
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
--- a/src/CTT/Arith.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/Arith.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/arith
+(* Title: CTT/arith
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Theorems for arith.thy (Arithmetic operators)
@@ -120,14 +120,14 @@
structure Arith_simp_data: TSIMP_DATA =
struct
- val refl = refl_elem
- val sym = sym_elem
- val trans = trans_elem
- val refl_red = refl_red
- val trans_red = trans_red
- val red_if_equal = red_if_equal
- val default_rls = arithC_rls @ comp_rls
- val routine_tac = routine_tac (arith_typing_rls @ routine_rls)
+ val refl = refl_elem
+ val sym = sym_elem
+ val trans = trans_elem
+ val refl_red = refl_red
+ val trans_red = trans_red
+ val red_if_equal = red_if_equal
+ val default_rls = arithC_rls @ comp_rls
+ val routine_tac = routine_tac (arith_typing_rls @ routine_rls)
end;
structure Arith_simp = TSimpFun (Arith_simp_data);
@@ -159,7 +159,7 @@
[ (NE_tac "a" 1),
(hyp_arith_rew_tac prems),
(NE_tac "b" 2),
- (resolve_tac [sym_elem] 1),
+ (rtac sym_elem 1),
(NE_tac "b" 1),
(hyp_arith_rew_tac prems) ]);
@@ -175,7 +175,7 @@
[ (NE_tac "a" 1),
(hyp_arith_rew_tac prems),
(NE_tac "b" 2),
- (resolve_tac [sym_elem] 1),
+ (rtac sym_elem 1),
(NE_tac "b" 1),
(hyp_arith_rew_tac prems) ]); NEEDS COMMUTATIVE MATCHING
***************)
@@ -198,7 +198,7 @@
(REPEAT (assume_tac 1 ORELSE
resolve_tac
(prems@[add_commute,mult_typingL,add_typingL]@
- intrL_rls@[refl_elem]) 1)) ]);
+ intrL_rls@[refl_elem]) 1)) ]);
(*Commutative law for multiplication*)
qed_goal "mult_commute" Arith.thy
@@ -254,8 +254,8 @@
(succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
by (NE_tac "x" 4 THEN assume_tac 4);
(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
-by (resolve_tac [replace_type] 5);
-by (resolve_tac [replace_type] 4);
+by (rtac replace_type 5);
+by (rtac replace_type 4);
by (arith_rew_tac prems);
(*Solves first 0 goal, simplifies others. Two sugbgoals remain.
Both follow by rewriting, (2) using quantified induction hyp*)
@@ -271,7 +271,7 @@
the use of RS below instantiates Vars in ProdE automatically. *)
val prems =
goal Arith.thy "[| a:N; b:N; b-a = 0 : N |] ==> b #+ (a-b) = a : N";
-by (resolve_tac [EqE] 1);
+by (rtac EqE 1);
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
by (REPEAT (resolve_tac (prems@[EqI]) 1));
qed "add_diff_inverse";
@@ -310,7 +310,7 @@
(*Note how easy using commutative laws can be? ...not always... *)
val prems = goalw Arith.thy [absdiff_def]
"[| a:N; b:N |] ==> a |-| b = b |-| a : N";
-by (resolve_tac [add_commute] 1);
+by (rtac add_commute 1);
by (typechk_tac ([diff_typing]@prems));
qed "absdiff_commute";
@@ -318,7 +318,7 @@
val prems =
goal Arith.thy "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)";
by (NE_tac "a" 1);
-by (resolve_tac [replace_type] 3);
+by (rtac replace_type 3);
by (arith_rew_tac prems);
by (intr_tac[]); (*strips remaining PRODs*)
by (resolve_tac [ zero_ne_succ RS FE ] 2);
@@ -330,9 +330,9 @@
Again, resolution instantiates variables in ProdE *)
val prems =
goal Arith.thy "[| a:N; b:N; a #+ b = 0 : N |] ==> a = 0 : N";
-by (resolve_tac [EqE] 1);
+by (rtac EqE 1);
by (resolve_tac [add_eq0_lemma RS ProdE] 1);
-by (resolve_tac [EqI] 3);
+by (rtac EqI 3);
by (ALLGOALS (resolve_tac prems));
qed "add_eq0";
@@ -342,8 +342,8 @@
\ ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
by (intr_tac[]);
by eqintr_tac;
-by (resolve_tac [add_eq0] 2);
-by (resolve_tac [add_eq0] 1);
+by (rtac add_eq0 2);
+by (rtac add_eq0 1);
by (resolve_tac [add_commute RS trans_elem] 6);
by (typechk_tac (diff_typing::prems));
qed "absdiff_eq0_lem";
@@ -352,12 +352,12 @@
proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
val prems =
goal Arith.thy "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N";
-by (resolve_tac [EqE] 1);
+by (rtac EqE 1);
by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
by (TRYALL (resolve_tac prems));
by eqintr_tac;
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
-by (resolve_tac [EqE] 3 THEN assume_tac 3);
+by (rtac EqE 3 THEN assume_tac 3);
by (hyp_arith_rew_tac (prems@[add_0_right]));
qed "absdiff_eq0";
@@ -430,11 +430,11 @@
(*for case analysis on whether a number is 0 or a successor*)
qed_goal "iszero_decidable" Arith.thy
"a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
-\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
+\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
(fn prems=>
[ (NE_tac "a" 1),
- (resolve_tac [PlusI_inr] 3),
- (resolve_tac [PlusI_inl] 2),
+ (rtac PlusI_inr 3),
+ (rtac PlusI_inl 2),
eqintr_tac,
(equal_tac prems) ]);
@@ -443,17 +443,17 @@
goal Arith.thy "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N";
by (NE_tac "a" 1);
by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2]));
-by (resolve_tac [EqE] 1);
+by (rtac EqE 1);
(*case analysis on succ(u mod b)|-|b *)
by (res_inst_tac [("a1", "succ(u mod b) |-| b")]
(iszero_decidable RS PlusE) 1);
by (etac SumE 3);
by (hyp_arith_rew_tac (prems @ div_typing_rls @
- [modC0,modC_succ, divC0, divC_succ2]));
+ [modC0,modC_succ, divC0, divC_succ2]));
(*Replace one occurence of b by succ(u mod b). Clumsy!*)
by (resolve_tac [ add_typingL RS trans_elem ] 1);
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
-by (resolve_tac [refl_elem] 3);
+by (rtac refl_elem 3);
by (hyp_arith_rew_tac (prems @ div_typing_rls));
qed "mod_div_equality";
--- a/src/CTT/Bool.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/Bool.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/bool
+(* Title: CTT/bool
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Theorems for bool.thy (booleans and conditionals)
@@ -40,7 +40,7 @@
"!!C. [| p = q : Bool; a = c : C(true); b = d : C(false) |] ==> \
\ cond(p,a,b) = cond(q,c,d) : C(p)"
(fn _ =>
- [ (resolve_tac [PlusEL] 1),
+ [ (rtac PlusEL 1),
(REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]);
(*computation rules for true, false*)
--- a/src/CTT/CTT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/CTT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/ctt.ML
+(* Title: CTT/ctt.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Tactics and lemmas for ctt.thy (Constructive Type Theory)
@@ -38,9 +38,9 @@
qed_goal "SumIL2" CTT.thy
"[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
(fn prems=>
- [ (resolve_tac [sym_elem] 1),
- (resolve_tac [SumIL] 1),
- (ALLGOALS (resolve_tac [sym_elem])),
+ [ (rtac sym_elem 1),
+ (rtac SumIL 1),
+ (ALLGOALS (rtac sym_elem )),
(ALLGOALS (resolve_tac prems)) ]);
val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
@@ -103,16 +103,16 @@
qed_goal "replace_type" CTT.thy
"[| B = A; a : A |] ==> a : B"
(fn prems=>
- [ (resolve_tac [equal_types] 1),
- (resolve_tac [sym_type] 2),
+ [ (rtac equal_types 1),
+ (rtac sym_type 2),
(ALLGOALS (resolve_tac prems)) ]);
(*Simplify the parameter of a unary type operator.*)
qed_goal "subst_eqtyparg" CTT.thy
"a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
(fn prems=>
- [ (resolve_tac [subst_typeL] 1),
- (resolve_tac [refl_type] 2),
+ [ (rtac subst_typeL 1),
+ (rtac refl_type 2),
(ALLGOALS (resolve_tac prems)),
(assume_tac 1) ]);
@@ -129,25 +129,25 @@
(** Tactics that instantiate CTT-rules.
Vars in the given terms will be incremented!
- The (resolve_tac [EqE] i) lets them apply to equality judgements. **)
+ The (rtac EqE i) lets them apply to equality judgements. **)
fun NE_tac (sp: string) i =
- TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] NE i;
+ TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
fun SumE_tac (sp: string) i =
- TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] SumE i;
+ TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
fun PlusE_tac (sp: string) i =
- TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
+ TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
fun add_mp_tac i =
- resolve_tac [subst_prodE] i THEN assume_tac i THEN assume_tac i;
+ rtac subst_prodE i THEN assume_tac i THEN assume_tac i;
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = eresolve_tac [subst_prodE] i THEN assume_tac i;
+fun mp_tac i = etac subst_prodE i THEN assume_tac i;
(*"safe" when regarded as predicate calculus rules*)
val safe_brls = sort lessb
--- a/src/CTT/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/ROOT
+(* Title: CTT/ROOT
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Adds Constructive Type Theory to a database containing pure Isabelle.
@@ -23,4 +23,4 @@
use "../Pure/install_pp.ML";
print_depth 8;
-val CTT_build_completed = (); (*indicate successful build*)
+val CTT_build_completed = (); (*indicate successful build*)
--- a/src/CTT/ex/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/ex/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/ex/ROOT
+(* Title: CTT/ex/ROOT
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Executes all examples for Constructive Type Theory.
--- a/src/CTT/ex/equal.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/ex/equal.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/ex/equal
+(* Title: CTT/ex/equal
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Equality reasoning by rewriting.
--- a/src/CTT/ex/synth.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/ex/synth.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/ex/synth
+(* Title: CTT/ex/synth
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
@@ -9,8 +9,8 @@
writeln"discovery of predecessor function";
goal CTT.thy
- "?a : SUM pred:?A . Eq(N, pred`0, 0) \
-\ * (PROD n:N. Eq(N, pred ` succ(n), n))";
+ "?a : SUM pred:?A . Eq(N, pred`0, 0) \
+\ * (PROD n:N. Eq(N, pred ` succ(n), n))";
by (intr_tac[]);
by eqintr_tac;
by (resolve_tac reduction_rls 3);
@@ -36,7 +36,7 @@
See following example.*)
goal CTT.thy
"?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) \
-\ * Eq(?A, ?b(inr(i)), <succ(0), i>)";
+\ * Eq(?A, ?b(inr(i)), <succ(0), i>)";
by (intr_tac[]);
by eqintr_tac;
by (resolve_tac comp_rls 1);
@@ -49,13 +49,13 @@
Simpler still: make ?A into a constant type N*N.*)
goal CTT.thy
"?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) \
-\ * Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
+\ * Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
writeln"A tricky combination of when and split";
(*Now handled easily, but caused great problems once*)
goal CTT.thy
"?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i) \
-\ * Eq(?A, ?b(inr(<i,j>)), j)";
+\ * Eq(?A, ?b(inr(<i,j>)), j)";
by (intr_tac[]);
by eqintr_tac;
by (resolve_tac [ PlusC_inl RS trans_elem ] 1);
@@ -69,18 +69,18 @@
(*similar but allows the type to depend on i and j*)
goal CTT.thy
"?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
-\ * Eq(?A(i,j), ?b(inr(<i,j>)), j)";
+\ * Eq(?A(i,j), ?b(inr(<i,j>)), j)";
(*similar but specifying the type N simplifies the unification problems*)
goal CTT.thy
- "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i) \
-\ * Eq(N, ?b(inr(<i,j>)), j)";
+ "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i) \
+\ * Eq(N, ?b(inr(<i,j>)), j)";
writeln"Deriving the addition operator";
goal Arith.thy
"?c : PROD n:N. Eq(N, ?f(0,n), n) \
-\ * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
+\ * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
by (intr_tac[]);
by eqintr_tac;
by (resolve_tac comp_rls 1);
@@ -91,8 +91,8 @@
writeln"The addition function -- using explicit lambdas";
goal Arith.thy
"?c : SUM plus : ?A . \
-\ PROD x:N. Eq(N, plus`0`x, x) \
-\ * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
+\ PROD x:N. Eq(N, plus`0`x, x) \
+\ * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
by (intr_tac[]);
by eqintr_tac;
by (resolve_tac [TSimp.split_eqn] 3);
--- a/src/CTT/ex/typechk.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/ex/typechk.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/ex/typechk
+(* Title: CTT/ex/typechk
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Easy examples: type checking and type deduction
--- a/src/CTT/rew.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/rew.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/rew
+(* Title: CTT/rew
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Simplifier for CTT, using Typedsimp
@@ -17,14 +17,14 @@
structure TSimp_data: TSIMP_DATA =
struct
- val refl = refl_elem
- val sym = sym_elem
- val trans = trans_elem
- val refl_red = refl_red
- val trans_red = trans_red
- val red_if_equal = red_if_equal
- val default_rls = comp_rls
- val routine_tac = routine_tac routine_rls
+ val refl = refl_elem
+ val sym = sym_elem
+ val trans = trans_elem
+ val refl_red = refl_red
+ val trans_red = trans_red
+ val red_if_equal = red_if_equal
+ val default_rls = comp_rls
+ val routine_tac = routine_tac routine_rls
end;
structure TSimp = TSimpFun (TSimp_data);
--- a/src/Cube/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/Cube/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Cube/ROOT
+(* Title: Cube/ROOT
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1992 University of Cambridge
The Lambda-Cube a la Barendregt
@@ -17,4 +17,4 @@
use "../Pure/install_pp.ML";
print_depth 8;
-val Cube_build_completed = (); (*indicate successful build*)
+val Cube_build_completed = (); (*indicate successful build*)
--- a/src/Cube/ex.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/Cube/ex.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
(* Examples taken from
- H. Barendregt. Introduction to Generalised Type Systems.
- J. Functional Programming.
+ H. Barendregt. Introduction to Generalised Type Systems.
+ J. Functional Programming.
*)
Cube_build_completed; (*Cause examples to fail if Cube did*)
@@ -11,11 +11,11 @@
REPEAT(resolve_tac[strip_b,strip_s]i THEN DEPTH_SOLVE_1(ares_tac thms i));
val imp_elim = prove_goal thy "[| f:A->B; a:A; f^a:B ==> PROP P |] ==> PROP P"
- (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
+ (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
val pi_elim = prove_goal thy
- "[| F:Prod(A,B); a:A; F^a:B(a) ==> PROP P |] ==> PROP P"
- (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
+ "[| F:Prod(A,B); a:A; F^a:B(a) ==> PROP P |] ==> PROP P"
+ (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
(* SIMPLE TYPES *)
@@ -114,7 +114,7 @@
uresult();
goal LP_thy "A:* P:A->* Q:* a0:A |- \
-\ Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T";
+\ Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
@@ -157,13 +157,13 @@
uresult();
goal LP2_thy "A:* P:A->A->* |- \
-\ (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P : ?T";
+\ (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P : ?T";
by (DEPTH_SOLVE (ares_tac LP2 1));
uresult();
(* Antisymmetry implies irreflexivity: *)
goal LP2_thy "A:* P:A->A->* |- \
-\ ?p: (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P";
+\ ?p: (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P";
by (strip_asms_tac LP2 1);
by (rtac lam_ss 1);
by (DEPTH_SOLVE_1(ares_tac LP2 1));
@@ -208,12 +208,12 @@
(* Some random examples *)
goal LP2_thy "A:* c:A f:A->A |- \
-\ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
+\ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
by (DEPTH_SOLVE(ares_tac LP2 1));
uresult();
goal CC_thy "Lam A:*.Lam c:A.Lam f:A->A. \
-\ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
+\ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
by (DEPTH_SOLVE(ares_tac CC 1));
uresult();
--- a/src/FOL/FOL.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/FOL.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/FOL.ML
+(* Title: FOL/FOL.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Tactics and lemmas for FOL.thy (classical First-Order Logic)
@@ -14,7 +14,7 @@
qed_goal "disjCI" FOL.thy
"(~Q ==> P) ==> P|Q"
(fn prems=>
- [ (resolve_tac [classical] 1),
+ [ (rtac classical 1),
(REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
(REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
@@ -22,17 +22,17 @@
qed_goal "ex_classical" FOL.thy
"( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
(fn prems=>
- [ (resolve_tac [classical] 1),
+ [ (rtac classical 1),
(eresolve_tac (prems RL [exI]) 1) ]);
(*version of above, simplifying ~EX to ALL~ *)
qed_goal "exCI" FOL.thy
"(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
(fn [prem]=>
- [ (resolve_tac [ex_classical] 1),
+ [ (rtac ex_classical 1),
(resolve_tac [notI RS allI RS prem] 1),
- (eresolve_tac [notE] 1),
- (eresolve_tac [exI] 1) ]);
+ (etac notE 1),
+ (etac exI 1) ]);
qed_goal "excluded_middle" FOL.thy "~P | P"
(fn _=> [ rtac disjCI 1, assume_tac 1 ]);
@@ -54,7 +54,7 @@
(*Double negation law*)
qed_goal "notnotD" FOL.thy "~~P ==> P"
(fn [major]=>
- [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
+ [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
(*** Tactics for implication and contradiction ***)
@@ -64,6 +64,6 @@
qed_goalw "iffCE" FOL.thy [iff_def]
"[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R"
(fn prems =>
- [ (resolve_tac [conjE] 1),
+ [ (rtac conjE 1),
(REPEAT (DEPTH_SOLVE_1
- (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]);
+ (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]);
--- a/src/FOL/IFOL.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/IFOL.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/IFOL.ML
+(* Title: FOL/IFOL.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Tactics and lemmas for IFOL.thy (intuitionistic first-order logic)
@@ -85,7 +85,7 @@
(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
qed_goalw "iffE" IFOL.thy [iff_def]
"[| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R"
- (fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]);
+ (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
(* Destruct rules for <-> similar to Modus Ponens *)
@@ -125,7 +125,7 @@
qed_goal "ex_ex1I" IFOL.thy
"[| EX x.P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
(fn [ex,eq] => [ (rtac (ex RS exE) 1),
- (REPEAT (ares_tac [ex1I,eq] 1)) ]);
+ (REPEAT (ares_tac [ex1I,eq] 1)) ]);
qed_goalw "ex1E" IFOL.thy [ex1_def]
"[| EX! x.P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R"
@@ -171,14 +171,14 @@
(fn prems =>
[ (cut_facts_tac prems 1),
(REPEAT (ares_tac [iffI,impI] 1
- ORELSE eresolve_tac [iffE] 1
+ ORELSE etac iffE 1
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]);
qed_goal "iff_cong" IFOL.thy
"[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
- (REPEAT (eresolve_tac [iffE] 1
+ (REPEAT (etac iffE 1
ORELSE ares_tac [iffI] 1
ORELSE mp_tac 1)) ]);
@@ -195,12 +195,12 @@
(fn prems =>
[ (REPEAT (ares_tac [iffI,allI] 1
ORELSE mp_tac 1
- ORELSE eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]);
+ ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]);
qed_goal "ex_cong" IFOL.thy
"(!!x.P(x) <-> Q(x)) ==> (EX x.P(x)) <-> (EX x.Q(x))"
(fn prems =>
- [ (REPEAT (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1
+ [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1
ORELSE mp_tac 1
ORELSE iff_tac prems 1)) ]);
@@ -241,7 +241,7 @@
"[| a=b |] ==> t(a)=t(b)"
(fn prems=>
[ (resolve_tac (prems RL [ssubst]) 1),
- (resolve_tac [refl] 1) ]);
+ (rtac refl 1) ]);
qed_goal "subst_context2" IFOL.thy
"[| a=b; c=d |] ==> t(a,c)=t(b,d)"
@@ -254,23 +254,23 @@
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
(*Useful with eresolve_tac for proving equalties from known equalities.
- a = b
- | |
- c = d *)
+ a = b
+ | |
+ c = d *)
qed_goal "box_equals" IFOL.thy
"[| a=b; a=c; b=d |] ==> c=d"
(fn prems=>
- [ (resolve_tac [trans] 1),
- (resolve_tac [trans] 1),
- (resolve_tac [sym] 1),
+ [ (rtac trans 1),
+ (rtac trans 1),
+ (rtac sym 1),
(REPEAT (resolve_tac prems 1)) ]);
(*Dual of box_equals: for proving equalities backwards*)
qed_goal "simp_equals" IFOL.thy
"[| a=c; b=d; c=d |] ==> a=b"
(fn prems=>
- [ (resolve_tac [trans] 1),
- (resolve_tac [trans] 1),
+ [ (rtac trans 1),
+ (rtac trans 1),
(REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);
(** Congruence rules for predicate letters **)
@@ -300,9 +300,9 @@
val pred_congs =
flat (map (fn c =>
- map (fn th => read_instantiate [("P",c)] th)
- [pred1_cong,pred2_cong,pred3_cong])
- (explode"PQRS"));
+ map (fn th => read_instantiate [("P",c)] th)
+ [pred1_cong,pred2_cong,pred3_cong])
+ (explode"PQRS"));
(*special case for the equality predicate!*)
val eq_cong = read_instantiate [("P","op =")] pred2_cong;
@@ -360,6 +360,6 @@
(*Courtesy Krzysztof Grabczewski*)
val major::prems = goal IFOL.thy "[| P|Q; P==>R; Q==>S |] ==> R|S";
-br (major RS disjE) 1;
+by (rtac (major RS disjE) 1);
by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
qed "disj_imp_disj";
--- a/src/FOL/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ROOT
+(* Title: FOL/ROOT
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Adds First-Order Logic to a database containing pure Isabelle.
@@ -43,10 +43,10 @@
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
- val sizef = size_of_thm
- val mp = mp
- val not_elim = notE
- val classical = classical
+ val sizef = size_of_thm
+ val mp = mp
+ val not_elim = notE
+ val classical = classical
val hyp_subst_tacs=[hyp_subst_tac]
end;
@@ -72,4 +72,4 @@
use "../Pure/install_pp.ML";
print_depth 8;
-val FOL_build_completed = (); (*indicate successful build*)
+val FOL_build_completed = (); (*indicate successful build*)
--- a/src/FOL/ex/If.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/If.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/if
+(* Title: FOL/ex/if
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
For ex/if.thy. First-Order Logic: the 'if' example
@@ -23,11 +23,11 @@
goal If.thy
"if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
-by (resolve_tac [iffI] 1);
-by (eresolve_tac [ifE] 1);
-by (eresolve_tac [ifE] 1);
-by (resolve_tac [ifI] 1);
-by (resolve_tac [ifI] 1);
+by (rtac iffI 1);
+by (etac ifE 1);
+by (etac ifE 1);
+by (rtac ifI 1);
+by (rtac ifI 1);
choplev 0;
val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
@@ -40,7 +40,7 @@
qed "nested_ifs";
choplev 0;
-by (rewrite_goals_tac [if_def]);
+by (rewtac if_def);
by (fast_tac FOL_cs 1);
result();
@@ -53,7 +53,7 @@
by (REPEAT (step_tac if_cs 1));
choplev 0;
-by (rewrite_goals_tac [if_def]);
+by (rewtac if_def);
by (fast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
--- a/src/FOL/ex/List.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/List.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/list
+(* Title: FOL/ex/list
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1991 University of Cambridge
For ex/list.thy. Examples of simplification and induction on lists
@@ -14,8 +14,8 @@
qed "list_exh";
val list_rew_thms = [list_distinct1,list_distinct2,app_nil,app_cons,
- hd_eq,tl_eq,forall_nil,forall_cons,list_free,
- len_nil,len_cons,at_0,at_succ];
+ hd_eq,tl_eq,forall_nil,forall_cons,list_free,
+ len_nil,len_cons,at_0,at_succ];
val list_ss = nat_ss addsimps list_rew_thms;
--- a/src/FOL/ex/Nat.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/Nat.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/nat.ML
+(* Title: FOL/ex/nat.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Examples for the manual "Introduction to Isabelle"
@@ -17,17 +17,17 @@
goal Nat.thy "Suc(k) ~= k";
by (res_inst_tac [("n","k")] induct 1);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [Suc_neq_0] 1);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [notE] 1);
-by (eresolve_tac [Suc_inject] 1);
+by (rtac notI 1);
+by (etac Suc_neq_0 1);
+by (rtac notI 1);
+by (etac notE 1);
+by (etac Suc_inject 1);
qed "Suc_n_not_n";
goal Nat.thy "(k+m)+n = k+(m+n)";
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
-by (resolve_tac [induct] 1);
+by (rtac induct 1);
back();
back();
back();
@@ -36,11 +36,11 @@
back();
goalw Nat.thy [add_def] "0+n = n";
-by (resolve_tac [rec_0] 1);
+by (rtac rec_0 1);
qed "add_0";
goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
-by (resolve_tac [rec_Suc] 1);
+by (rtac rec_Suc 1);
qed "add_Suc";
val add_ss = FOL_ss addsimps [add_0, add_Suc];
--- a/src/FOL/ex/Nat2.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/Nat2.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/nat2.ML
+(* Title: FOL/ex/nat2.ML
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1991 University of Cambridge
For ex/nat.thy.
@@ -10,9 +10,9 @@
open Nat2;
val nat_rews = [pred_0, pred_succ, plus_0, plus_succ,
- nat_distinct1, nat_distinct2, succ_inject,
- leq_0,leq_succ_succ,leq_succ_0,
- lt_0_succ,lt_succ_succ,lt_0];
+ nat_distinct1, nat_distinct2, succ_inject,
+ leq_0,leq_succ_succ,leq_succ_0,
+ lt_0_succ,lt_succ_succ,lt_0];
val nat_ss = FOL_ss addsimps nat_rews;
--- a/src/FOL/ex/NatClass.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/NatClass.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/NatClass.ML
+(* Title: FOL/ex/NatClass.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
This is Nat.ML trivially modified to make it work with NatClass.thy.
@@ -10,17 +10,17 @@
goal NatClass.thy "Suc(k) ~= (k::'a::nat)";
by (res_inst_tac [("n","k")] induct 1);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [Suc_neq_0] 1);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [notE] 1);
-by (eresolve_tac [Suc_inject] 1);
+by (rtac notI 1);
+by (etac Suc_neq_0 1);
+by (rtac notI 1);
+by (etac notE 1);
+by (etac Suc_inject 1);
qed "Suc_n_not_n";
goal NatClass.thy "(k+m)+n = k+(m+n)";
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
-by (resolve_tac [induct] 1);
+by (rtac induct 1);
back();
back();
back();
@@ -29,11 +29,11 @@
back();
goalw NatClass.thy [add_def] "0+n = n";
-by (resolve_tac [rec_0] 1);
+by (rtac rec_0 1);
qed "add_0";
goalw NatClass.thy [add_def] "Suc(m)+n = Suc(m+n)";
-by (resolve_tac [rec_Suc] 1);
+by (rtac rec_Suc 1);
qed "add_Suc";
val add_ss = FOL_ss addsimps [add_0, add_Suc];
--- a/src/FOL/ex/Prolog.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/Prolog.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/prolog.ML
+(* Title: FOL/ex/prolog.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
For ex/prolog.thy. First-Order Logic: PROLOG examples
--- a/src/FOL/ex/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/ROOT
+(* Title: FOL/ex/ROOT
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Executes all examples for First-Order Logic.
@@ -8,7 +8,7 @@
writeln"Root file for FOL examples";
-FOL_build_completed; (*Cause examples to fail if FOL did*)
+FOL_build_completed; (*Cause examples to fail if FOL did*)
proof_timing := true;
--- a/src/FOL/ex/cla.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/cla.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/cla
+(* Title: FOL/ex/cla
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Classical First-Order Logic
@@ -222,8 +222,8 @@
result();
writeln"Problem 26";
-goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) & \
-\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
+goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) & \
+\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
by (fast_tac FOL_cs 1);
result();
@@ -283,9 +283,9 @@
writeln"Problem 34 AMENDED (TWICE!!)";
(*Andrews's challenge*)
-goal FOL.thy "((EX x. ALL y. p(x) <-> p(y)) <-> \
-\ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \
-\ ((EX x. ALL y. q(x) <-> q(y)) <-> \
+goal FOL.thy "((EX x. ALL y. p(x) <-> p(y)) <-> \
+\ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \
+\ ((EX x. ALL y. q(x) <-> q(y)) <-> \
\ ((EX x. p(x)) <-> (ALL y. q(y))))";
by (deepen_tac FOL_cs 0 1);
result();
@@ -318,10 +318,10 @@
writeln"Problem 38";
goal FOL.thy
- "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \
-\ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \
-\ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \
-\ (~p(a) | ~(EX y. p(y) & r(x,y)) | \
+ "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \
+\ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \
+\ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \
+\ (~p(a) | ~(EX y. p(y) & r(x,y)) | \
\ (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
by (fast_tac FOL_cs 1);
result();
@@ -338,7 +338,7 @@
result();
writeln"Problem 41";
-goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \
+goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \
\ --> ~ (EX z. ALL x. f(x,z))";
by (fast_tac FOL_cs 1);
result();
@@ -349,29 +349,29 @@
result();
writeln"Problem 43";
-goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
+goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
\ --> (ALL x. ALL y. q(x,y) <-> q(y,x))";
by (mini_tac 1);
by (deepen_tac FOL_cs 5 1);
(*Faster alternative proof!
- by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1);
+ by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1);
*)
result();
writeln"Problem 44";
-goal FOL.thy "(ALL x. f(x) --> \
-\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
-\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
+goal FOL.thy "(ALL x. f(x) --> \
+\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
+\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
\ --> (EX x. j(x) & ~f(x))";
by (fast_tac FOL_cs 1);
result();
writeln"Problem 45";
-goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \
-\ --> (ALL y. g(y) & h(x,y) --> k(y))) & \
-\ ~ (EX y. l(y) & k(y)) & \
-\ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \
-\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \
+goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \
+\ --> (ALL y. g(y) & h(x,y) --> k(y))) & \
+\ ~ (EX y. l(y) & k(y)) & \
+\ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \
+\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \
\ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
by (best_tac FOL_cs 1);
result();
@@ -388,12 +388,12 @@
(*Hard because it involves substitution for Vars;
the type constraint ensures that x,y,z have the same type as a,b,u. *)
goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
-\ --> (ALL u::'a.P(u))";
+\ --> (ALL u::'a.P(u))";
by (safe_tac FOL_cs);
by (res_inst_tac [("x","a")] allE 1);
-ba 1;
+by (assume_tac 1);
by (res_inst_tac [("x","b")] allE 1);
-ba 1;
+by (assume_tac 1);
by (fast_tac FOL_cs 1);
result();
@@ -437,8 +437,8 @@
\ killed(?who,agatha)";
by (safe_tac FOL_cs);
by (dres_inst_tac [("x1","x")] (spec RS mp) 1);
-ba 1;
-be (spec RS exE) 1;
+by (assume_tac 1);
+by (etac (spec RS exE) 1);
by (REPEAT (etac allE 1));
by (fast_tac FOL_cs 1);
result();
@@ -490,8 +490,8 @@
writeln"Problem 62 as corrected in AAR newletter #31";
goal FOL.thy
- "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \
-\ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \
+ "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \
+\ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \
\ (~p(a) | ~p(f(x)) | p(f(f(x)))))";
by (fast_tac FOL_cs 1);
result();
--- a/src/FOL/ex/foundn.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/foundn.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/foundn
+(* Title: FOL/ex/foundn
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
@@ -9,11 +9,11 @@
writeln"File FOL/ex/foundn.";
goal IFOL.thy "A&B --> (C-->A&C)";
-by (resolve_tac [impI] 1);
-by (resolve_tac [impI] 1);
-by (resolve_tac [conjI] 1);
+by (rtac impI 1);
+by (rtac impI 1);
+by (rtac conjI 1);
by (assume_tac 2);
-by (resolve_tac [conjunct1] 1);
+by (rtac conjunct1 1);
by (assume_tac 1);
result();
@@ -21,9 +21,9 @@
val prems =
goal IFOL.thy "A&B ==> ([| A; B |] ==> C) ==> C";
by (resolve_tac prems 1);
-by (resolve_tac [conjunct1] 1);
+by (rtac conjunct1 1);
by (resolve_tac prems 1);
-by (resolve_tac [conjunct2] 1);
+by (rtac conjunct2 1);
by (resolve_tac prems 1);
result();
@@ -31,17 +31,17 @@
val prems =
goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B";
by (resolve_tac prems 1);
-by (resolve_tac [notI] 1);
+by (rtac notI 1);
by (res_inst_tac [ ("P", "~B") ] notE 1);
-by (resolve_tac [notI] 2);
+by (rtac notI 2);
by (res_inst_tac [ ("P", "B | ~B") ] notE 2);
by (assume_tac 2);
-by (resolve_tac [disjI1] 2);
+by (rtac disjI1 2);
by (assume_tac 2);
-by (resolve_tac [notI] 1);
+by (rtac notI 1);
by (res_inst_tac [ ("P", "B | ~B") ] notE 1);
by (assume_tac 1);
-by (resolve_tac [disjI2] 1);
+by (rtac disjI2 1);
by (assume_tac 1);
result();
@@ -49,23 +49,23 @@
val prems =
goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B";
by (resolve_tac prems 1);
-by (resolve_tac [notI] 1);
-by (resolve_tac [notE] 1);
-by (resolve_tac [notI] 2);
-by (eresolve_tac [notE] 2);
-by (eresolve_tac [disjI1] 2);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [notE] 1);
-by (eresolve_tac [disjI2] 1);
+by (rtac notI 1);
+by (rtac notE 1);
+by (rtac notI 2);
+by (etac notE 2);
+by (etac disjI1 2);
+by (rtac notI 1);
+by (etac notE 1);
+by (etac disjI2 1);
result();
val prems =
goal IFOL.thy "[| A | ~A; ~ ~A |] ==> A";
-by (resolve_tac [disjE] 1);
+by (rtac disjE 1);
by (resolve_tac prems 1);
by (assume_tac 1);
-by (resolve_tac [FalseE] 1);
+by (rtac FalseE 1);
by (res_inst_tac [ ("P", "~A") ] notE 1);
by (resolve_tac prems 1);
by (assume_tac 1);
@@ -76,25 +76,25 @@
val prems =
goal IFOL.thy "ALL z. G(z) ==> ALL z. G(z)|H(z)";
-by (resolve_tac [allI] 1);
-by (resolve_tac [disjI1] 1);
+by (rtac allI 1);
+by (rtac disjI1 1);
by (resolve_tac (prems RL [spec]) 1);
(*can use instead
- by (resolve_tac [spec] 1); by (resolve_tac prems 1); *)
+ by (rtac spec 1); by (resolve_tac prems 1); *)
result();
goal IFOL.thy "ALL x. EX y. x=y";
-by (resolve_tac [allI] 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [refl] 1);
+by (rtac allI 1);
+by (rtac exI 1);
+by (rtac refl 1);
result();
goal IFOL.thy "EX y. ALL x. x=y";
-by (resolve_tac [exI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [refl] 1) handle ERROR => writeln"Failed, as expected";
+by (rtac exI 1);
+by (rtac allI 1);
+by (rtac refl 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
@@ -109,12 +109,12 @@
val prems =
goal IFOL.thy "(EX z.F(z)) & B ==> (EX z. F(z) & B)";
-by (resolve_tac [conjE] 1);
+by (rtac conjE 1);
by (resolve_tac prems 1);
-by (resolve_tac [exE] 1);
+by (rtac exE 1);
by (assume_tac 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [conjI] 1);
+by (rtac exI 1);
+by (rtac conjI 1);
by (assume_tac 1);
by (assume_tac 1);
result();
@@ -122,11 +122,11 @@
(*A bigger demonstration of quantifiers -- not in the paper*)
goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
-by (resolve_tac [impI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [exE] 1 THEN assume_tac 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [allE] 1 THEN assume_tac 1);
+by (rtac impI 1);
+by (rtac allI 1);
+by (rtac exE 1 THEN assume_tac 1);
+by (rtac exI 1);
+by (rtac allE 1 THEN assume_tac 1);
by (assume_tac 1);
result();
--- a/src/FOL/ex/int.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/int.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/int
+(* Title: FOL/ex/int
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Intuitionistic First-Order Logic
@@ -289,8 +289,8 @@
result();
writeln"Problem ~~26";
-goal IFOL.thy "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) & \
-\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
+goal IFOL.thy "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) & \
+\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
(*NOT PROVED*)
@@ -378,9 +378,9 @@
result();
writeln"Problem 44";
-goal IFOL.thy "(ALL x. f(x) --> \
-\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
-\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
+goal IFOL.thy "(ALL x. f(x) --> \
+\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
+\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
\ --> (EX x. j(x) & ~f(x))";
by (Int.fast_tac 1);
result();
--- a/src/FOL/ex/intro.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/intro.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/intro
+(* Title: FOL/ex/intro
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Examples for the manual "Introduction to Isabelle"
@@ -15,29 +15,29 @@
(**** Some simple backward proofs ****)
goal FOL.thy "P|P --> P";
-by (resolve_tac [impI] 1);
-by (resolve_tac [disjE] 1);
+by (rtac impI 1);
+by (rtac disjE 1);
by (assume_tac 3);
by (assume_tac 2);
by (assume_tac 1);
qed "mythm";
goal FOL.thy "(P & Q) | R --> (P | R)";
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disjE] 1);
-by (dresolve_tac [conjunct1] 1);
-by (resolve_tac [disjI1] 1);
-by (resolve_tac [disjI2] 2);
+by (rtac impI 1);
+by (etac disjE 1);
+by (dtac conjunct1 1);
+by (rtac disjI1 1);
+by (rtac disjI2 2);
by (REPEAT (assume_tac 1));
result();
(*Correct version, delaying use of "spec" until last*)
goal FOL.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
-by (resolve_tac [impI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [allI] 1);
-by (dresolve_tac [spec] 1);
-by (dresolve_tac [spec] 1);
+by (rtac impI 1);
+by (rtac allI 1);
+by (rtac allI 1);
+by (dtac spec 1);
+by (dtac spec 1);
by (assume_tac 1);
result();
@@ -58,7 +58,7 @@
(**** Derivation of conjunction elimination rule ****)
val [major,minor] = goal FOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R";
-by (resolve_tac [minor] 1);
+by (rtac minor 1);
by (resolve_tac [major RS conjunct1] 1);
by (resolve_tac [major RS conjunct2] 1);
prth (topthm());
@@ -70,17 +70,17 @@
(** Derivation of negation introduction **)
val prems = goal FOL.thy "(P ==> False) ==> ~P";
-by (rewrite_goals_tac [not_def]);
-by (resolve_tac [impI] 1);
+by (rewtac not_def);
+by (rtac impI 1);
by (resolve_tac prems 1);
by (assume_tac 1);
result();
val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R";
-by (resolve_tac [FalseE] 1);
-by (resolve_tac [mp] 1);
+by (rtac FalseE 1);
+by (rtac mp 1);
by (resolve_tac [rewrite_rule [not_def] major] 1);
-by (resolve_tac [minor] 1);
+by (rtac minor 1);
result();
(*Alternative proof of above result*)
--- a/src/FOL/ex/mini.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/mini.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/mini
+(* Title: FOL/ex/mini
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Classical First-Order Logic
@@ -20,52 +20,52 @@
(writeln s;
prove_goal FOL.thy s
(fn prems => [ (cut_facts_tac prems 1),
- (Cla.fast_tac FOL_cs 1) ]));
+ (Cla.fast_tac FOL_cs 1) ]));
val demorgans = map prove_fun
- ["~(P&Q) <-> ~P | ~Q",
- "~(P|Q) <-> ~P & ~Q",
- "~~P <-> P",
- "~(ALL x.P(x)) <-> (EX x. ~P(x))",
- "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
+ ["~(P&Q) <-> ~P | ~Q",
+ "~(P|Q) <-> ~P & ~Q",
+ "~~P <-> P",
+ "~(ALL x.P(x)) <-> (EX x. ~P(x))",
+ "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
(*** Removal of --> and <-> (positive and negative occurrences) ***)
(*Last one is important for computing a compact CNF*)
val nnf_rews = map prove_fun
- ["(P-->Q) <-> (~P | Q)",
- "~(P-->Q) <-> (P & ~Q)",
- "(P<->Q) <-> (~P | Q) & (~Q | P)",
- "~(P<->Q) <-> (P | Q) & (~P | ~Q)"];
+ ["(P-->Q) <-> (~P | Q)",
+ "~(P-->Q) <-> (P & ~Q)",
+ "(P<->Q) <-> (~P | Q) & (~Q | P)",
+ "~(P<->Q) <-> (P | Q) & (~P | ~Q)"];
(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
(*** Pushing in the existential quantifiers ***)
val ex_rews = map prove_fun
- ["(EX x. P) <-> P",
- "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
- "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
- "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
- "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
- "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
+ ["(EX x. P) <-> P",
+ "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
+ "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
+ "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
+ "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
+ "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
(*** Pushing in the universal quantifiers ***)
val all_rews = map prove_fun
- ["(ALL x. P) <-> P",
- "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
- "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
- "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
- "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
- "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
+ ["(ALL x. P) <-> P",
+ "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
+ "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
+ "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
+ "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
+ "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
val mini_ss =
empty_ss
setmksimps (map mk_meta_eq o atomize o gen_all)
setsolver (fn prems => resolve_tac (triv_rls@prems)
- ORELSE' assume_tac
- ORELSE' etac FalseE)
+ ORELSE' assume_tac
+ ORELSE' etac FalseE)
setsubgoaler asm_simp_tac
addsimps (demorgans @ nnf_rews @ ex_rews @ all_rews);
--- a/src/FOL/ex/prop.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/prop.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/prop
+(* Title: FOL/ex/prop
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
First-Order Logic: propositional examples (intuitionistic and classical)
@@ -107,13 +107,13 @@
(* stab-to-peirce *)
goal thy "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
-\ --> ((P --> Q) --> P) --> P";
+\ --> ((P --> Q) --> P) --> P";
by tac;
result();
(* peirce-imp1 *)
goal thy "(((Q --> R) --> Q) --> Q) \
-\ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
+\ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
by tac;
result();
@@ -134,10 +134,10 @@
(* tatsuta *)
goal thy "(((P7 --> P1) --> P10) --> P4 --> P5) \
-\ --> (((P8 --> P2) --> P9) --> P3 --> P10) \
-\ --> (P1 --> P8) --> P6 --> P7 \
-\ --> (((P3 --> P2) --> P9) --> P4) \
-\ --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
+\ --> (((P8 --> P2) --> P9) --> P3 --> P10) \
+\ --> (P1 --> P8) --> P6 --> P7 \
+\ --> (((P3 --> P2) --> P9) --> P4) \
+\ --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
by tac;
result();
--- a/src/FOL/ex/quant.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/ex/quant.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/quant
+(* Title: FOL/ex/quant
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
First-Order Logic: quantifier examples (intuitionistic and classical)
--- a/src/FOL/intprover.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/intprover.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/int-prover
+(* Title: FOL/int-prover
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
A naive prover for intuitionistic logic
@@ -56,10 +56,10 @@
(*Attack subgoals using safe inferences -- matching, not resolution*)
val safe_step_tac = FIRST' [eq_assume_tac,
- eq_mp_tac,
- bimatch_tac safe0_brls,
- hyp_subst_tac,
- bimatch_tac safep_brls] ;
+ eq_mp_tac,
+ bimatch_tac safe0_brls,
+ hyp_subst_tac,
+ bimatch_tac safep_brls] ;
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
--- a/src/FOL/simpdata.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/simpdata.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/simpdata
+(* Title: FOL/simpdata
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Simplification data for FOL
@@ -12,37 +12,37 @@
(writeln s;
prove_goal IFOL.thy s
(fn prems => [ (cut_facts_tac prems 1),
- (Int.fast_tac 1) ]));
+ (Int.fast_tac 1) ]));
val conj_rews = map int_prove_fun
- ["P & True <-> P", "True & P <-> P",
+ ["P & True <-> P", "True & P <-> P",
"P & False <-> False", "False & P <-> False",
"P & P <-> P",
- "P & ~P <-> False", "~P & P <-> False",
+ "P & ~P <-> False", "~P & P <-> False",
"(P & Q) & R <-> P & (Q & R)"];
val disj_rews = map int_prove_fun
- ["P | True <-> True", "True | P <-> True",
- "P | False <-> P", "False | P <-> P",
+ ["P | True <-> True", "True | P <-> True",
+ "P | False <-> P", "False | P <-> P",
"P | P <-> P",
"(P | Q) | R <-> P | (Q | R)"];
val not_rews = map int_prove_fun
["~(P|Q) <-> ~P & ~Q",
- "~ False <-> True", "~ True <-> False"];
+ "~ False <-> True", "~ True <-> False"];
val imp_rews = map int_prove_fun
- ["(P --> False) <-> ~P", "(P --> True) <-> True",
- "(False --> P) <-> True", "(True --> P) <-> P",
- "(P --> P) <-> True", "(P --> ~P) <-> ~P"];
+ ["(P --> False) <-> ~P", "(P --> True) <-> True",
+ "(False --> P) <-> True", "(True --> P) <-> P",
+ "(P --> P) <-> True", "(P --> ~P) <-> ~P"];
val iff_rews = map int_prove_fun
- ["(True <-> P) <-> P", "(P <-> True) <-> P",
+ ["(True <-> P) <-> P", "(P <-> True) <-> P",
"(P <-> P) <-> True",
- "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
+ "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
val quant_rews = map int_prove_fun
- ["(ALL x.P) <-> P", "(EX x.P) <-> P"];
+ ["(ALL x.P) <-> P", "(EX x.P) <-> P"];
(*These are NOT supplied by default!*)
val distrib_rews = map int_prove_fun
@@ -62,12 +62,12 @@
case concl_of r of
Const("Trueprop",_) $ p =>
(case p of
- Const("op -->",_)$_$_ => atomize(r RS mp)
+ Const("op -->",_)$_$_ => atomize(r RS mp)
| Const("op &",_)$_$_ => atomize(r RS conjunct1) @
- atomize(r RS conjunct2)
+ atomize(r RS conjunct2)
| Const("All",_)$_ => atomize(r RS spec)
- | Const("True",_) => [] (*True is DELETED*)
- | Const("False",_) => [] (*should False do something?*)
+ | Const("True",_) => [] (*True is DELETED*)
+ | Const("False",_) => [] (*should False do something?*)
| _ => [r])
| _ => [r];
@@ -111,8 +111,8 @@
empty_ss
setmksimps (map mk_meta_eq o atomize o gen_all)
setsolver (fn prems => resolve_tac (triv_rls@prems)
- ORELSE' assume_tac
- ORELSE' etac FalseE)
+ ORELSE' assume_tac
+ ORELSE' etac FalseE)
setsubgoaler asm_simp_tac
addsimps IFOL_rews
addcongs [imp_cong];
@@ -122,12 +122,12 @@
(writeln s;
prove_goal FOL.thy s
(fn prems => [ (cut_facts_tac prems 1),
- (Cla.fast_tac FOL_cs 1) ]));
+ (Cla.fast_tac FOL_cs 1) ]));
val cla_rews = map prove_fun
["~(P&Q) <-> ~P | ~Q",
- "P | ~P", "~P | P",
- "~ ~ P <-> P", "(~P --> P) <-> P"];
+ "P | ~P", "~P | P",
+ "~ ~ P <-> P", "(~P --> P) <-> P"];
val FOL_ss = IFOL_ss addsimps cla_rews;
--- a/src/FOLP/FOLP.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/FOLP.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/FOLP.ML
+(* Title: FOLP/FOLP.ML
ID: $Id$
- Author: Martin D Coen, Cambridge University Computer Laboratory
+ Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
@@ -29,7 +29,7 @@
val disjCI = prove_goal FOLP.thy
"(!!x.x:~Q ==> f(x):P) ==> ?p : P|Q"
(fn prems=>
- [ (resolve_tac [classical] 1),
+ [ (rtac classical 1),
(REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
(REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
@@ -37,17 +37,17 @@
val ex_classical = prove_goal FOLP.thy
"( !!u.u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
(fn prems=>
- [ (resolve_tac [classical] 1),
+ [ (rtac classical 1),
(eresolve_tac (prems RL [exI]) 1) ]);
(*version of above, simplifying ~EX to ALL~ *)
val exCI = prove_goal FOLP.thy
"(!!u.u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
(fn [prem]=>
- [ (resolve_tac [ex_classical] 1),
+ [ (rtac ex_classical 1),
(resolve_tac [notI RS allI RS prem] 1),
- (eresolve_tac [notE] 1),
- (eresolve_tac [exI] 1) ]);
+ (etac notE 1),
+ (etac exI 1) ]);
val excluded_middle = prove_goal FOLP.thy "?p : ~P | P"
(fn _=> [ rtac disjCI 1, assume_tac 1 ]);
@@ -66,7 +66,7 @@
(*Double negation law*)
val notnotD = prove_goal FOLP.thy "p:~~P ==> ?p : P"
(fn [major]=>
- [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
+ [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
(*** Tactics for implication and contradiction ***)
@@ -77,16 +77,16 @@
"[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R; \
\ !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R"
(fn prems =>
- [ (resolve_tac [conjE] 1),
+ [ (rtac conjE 1),
(REPEAT (DEPTH_SOLVE_1
- (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]);
+ (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]);
(*Should be used as swap since ~P becomes redundant*)
val swap = prove_goal FOLP.thy
"p:~P ==> (!!x.x:~Q ==> f(x):P) ==> ?p : Q"
(fn major::prems=>
- [ (resolve_tac [classical] 1),
+ [ (rtac classical 1),
(rtac (major RS notE) 1),
(REPEAT (ares_tac prems 1)) ]);
--- a/src/FOLP/IFOLP.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/IFOLP.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/IFOLP.ML
+(* Title: FOLP/IFOLP.ML
ID: $Id$
- Author: Martin D Coen, Cambridge University Computer Laboratory
+ Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
@@ -140,9 +140,9 @@
let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
and concl = discard_proof (Logic.strip_assums_concl prem)
in
- if exists (fn hyp => hyp aconv concl) hyps
- then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of
- [_] => assume_tac i
+ if exists (fn hyp => hyp aconv concl) hyps
+ then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of
+ [_] => assume_tac i
| _ => no_tac
else no_tac
end);
@@ -168,7 +168,7 @@
(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
val iffE = prove_goalw IFOLP.thy [iff_def]
"[| p:P <-> Q; !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R"
- (fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]);
+ (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
(* Destruct rules for <-> similar to Modus Ponens *)
@@ -241,14 +241,14 @@
(fn prems =>
[ (cut_facts_tac prems 1),
(REPEAT (ares_tac [iffI,impI] 1
- ORELSE eresolve_tac [iffE] 1
+ ORELSE etac iffE 1
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]);
val iff_cong = prove_goal IFOLP.thy
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
- (REPEAT (eresolve_tac [iffE] 1
+ (REPEAT (etac iffE 1
ORELSE ares_tac [iffI] 1
ORELSE mp_tac 1)) ]);
@@ -265,12 +265,12 @@
(fn prems =>
[ (REPEAT (ares_tac [iffI,allI] 1
ORELSE mp_tac 1
- ORELSE eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]);
+ ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]);
val ex_cong = prove_goal IFOLP.thy
"(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))"
(fn prems =>
- [ (REPEAT (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1
+ [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1
ORELSE mp_tac 1
ORELSE iff_tac prems 1)) ]);
@@ -320,7 +320,7 @@
"[| p:a=b |] ==> ?d:t(a)=t(b)"
(fn prems=>
[ (resolve_tac (prems RL [ssubst]) 1),
- (resolve_tac [refl] 1) ]);
+ (rtac refl 1) ]);
val subst_context2 = prove_goal IFOLP.thy
"[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)"
@@ -333,23 +333,23 @@
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
(*Useful with eresolve_tac for proving equalties from known equalities.
- a = b
- | |
- c = d *)
+ a = b
+ | |
+ c = d *)
val box_equals = prove_goal IFOLP.thy
"[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d"
(fn prems=>
- [ (resolve_tac [trans] 1),
- (resolve_tac [trans] 1),
- (resolve_tac [sym] 1),
+ [ (rtac trans 1),
+ (rtac trans 1),
+ (rtac sym 1),
(REPEAT (resolve_tac prems 1)) ]);
(*Dual of box_equals: for proving equalities backwards*)
val simp_equals = prove_goal IFOLP.thy
"[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b"
(fn prems=>
- [ (resolve_tac [trans] 1),
- (resolve_tac [trans] 1),
+ [ (rtac trans 1),
+ (rtac trans 1),
(REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);
(** Congruence rules for predicate letters **)
@@ -379,9 +379,9 @@
val pred_congs =
flat (map (fn c =>
- map (fn th => read_instantiate [("P",c)] th)
- [pred1_cong,pred2_cong,pred3_cong])
- (explode"PQRS"));
+ map (fn th => read_instantiate [("P",c)] th)
+ [pred1_cong,pred2_cong,pred3_cong])
+ (explode"PQRS"));
(*special case for the equality predicate!*)
val eq_cong = read_instantiate [("P","op =")] pred2_cong;
--- a/src/FOLP/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/ROOT
+(* Title: FOLP/ROOT
ID: $Id$
- Author: martin Coen, Cambridge University Computer Laboratory
+ Author: martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Modifed version of Lawrence Paulson's FOL that contains proof terms.
@@ -20,7 +20,7 @@
use "hypsubst.ML";
use "classical.ML"; (* Patched 'cos matching won't instantiate proof *)
-use "simp.ML"; (* Patched 'cos matching won't instantiate proof *)
+use "simp.ML"; (* Patched 'cos matching won't instantiate proof *)
(*** Applying HypsubstFun to generate hyp_subst_tac ***)
@@ -34,7 +34,7 @@
(*etac rev_cut_eq moves an equality to be the last premise. *)
val rev_cut_eq = prove_goal IFOLP.thy
- "[| p:a=b; !!x.x:a=b ==> f(x):R |] ==> ?p:R"
+ "[| p:a=b; !!x.x:a=b ==> f(x):R |] ==> ?p:R"
(fn prems => [ REPEAT(resolve_tac prems 1) ]);
val rev_mp = rev_mp
@@ -78,4 +78,4 @@
use "../Pure/install_pp.ML";
print_depth 8;
-val FOLP_build_completed = (); (*indicate successful build*)
+val FOLP_build_completed = (); (*indicate successful build*)
--- a/src/FOLP/classical.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/classical.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/classical
+(* Title: FOLP/classical
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Like Provers/classical but modified because match_tac is unsuitable for
@@ -19,10 +19,10 @@
signature CLASSICAL_DATA =
sig
- val mp: thm (* [| P-->Q; P |] ==> Q *)
- val not_elim: thm (* [| ~P; P |] ==> R *)
- val swap: thm (* ~P ==> (~Q ==> P) ==> Q *)
- val sizef : thm -> int (* size function for BEST_FIRST *)
+ val mp: thm (* [| P-->Q; P |] ==> Q *)
+ val not_elim: thm (* [| ~P; P |] ==> R *)
+ val swap: thm (* ~P ==> (~Q ==> P) ==> Q *)
+ val sizef : thm -> int (* size function for BEST_FIRST *)
val hyp_subst_tacs: (int -> tactic) list
end;
@@ -71,7 +71,7 @@
val imp_elim = make_elim mp;
(*Solve goal that assumes both P and ~P. *)
-val contr_tac = eresolve_tac [not_elim] THEN' assume_tac;
+val contr_tac = etac not_elim THEN' assume_tac;
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac i;
@@ -94,13 +94,13 @@
datatype claset =
CS of {safeIs: thm list,
- safeEs: thm list,
- hazIs: thm list,
- hazEs: thm list,
- (*the following are computed from the above*)
- safe0_brls: (bool*thm)list,
- safep_brls: (bool*thm)list,
- haz_brls: (bool*thm)list};
+ safeEs: thm list,
+ hazIs: thm list,
+ hazEs: thm list,
+ (*the following are computed from the above*)
+ safe0_brls: (bool*thm)list,
+ safep_brls: (bool*thm)list,
+ haz_brls: (bool*thm)list};
fun rep_claset (CS x) = x;
@@ -115,8 +115,8 @@
partition (apl(0,op=) o subgoals_of_brl)
(sort lessb (joinrules(safeIs, safeEs)))
in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
- safe0_brls=safe0_brls, safep_brls=safep_brls,
- haz_brls = sort lessb (joinrules(hazIs, hazEs))}
+ safe0_brls=safe0_brls, safep_brls=safep_brls,
+ haz_brls = sort lessb (joinrules(hazIs, hazEs))}
end;
(*** Manipulation of clasets ***)
@@ -151,10 +151,10 @@
(*Attack subgoals using safe inferences*)
fun safe_step_tac (CS{safe0_brls,safep_brls,...}) =
FIRST' [uniq_assume_tac,
- uniq_mp_tac,
- biresolve_tac safe0_brls,
- FIRST' hyp_subst_tacs,
- biresolve_tac safep_brls] ;
+ uniq_mp_tac,
+ biresolve_tac safe0_brls,
+ FIRST' hyp_subst_tacs,
+ biresolve_tac safep_brls] ;
(*Repeatedly attack subgoals using safe inferences*)
fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));
--- a/src/FOLP/ex/If.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/If.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/ex/if
+(* Title: FOLP/ex/if
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
For ex/if.thy. First-Order Logic: the 'if' example
@@ -24,11 +24,11 @@
goal If.thy
"?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
-by (resolve_tac [iffI] 1);
-by (eresolve_tac [ifE] 1);
-by (eresolve_tac [ifE] 1);
-by (resolve_tac [ifI] 1);
-by (resolve_tac [ifI] 1);
+by (rtac iffI 1);
+by (etac ifE 1);
+by (etac ifE 1);
+by (rtac ifI 1);
+by (rtac ifI 1);
choplev 0;
val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE];
--- a/src/FOLP/ex/Nat.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/Nat.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/ex/nat.ML
+(* Title: FOLP/ex/nat.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Examples for the manual "Introduction to Isabelle"
@@ -59,7 +59,7 @@
val add_ss = FOLP_ss addcongs nat_congs
- addrews [add_0, add_Suc];
+ addrews [add_0, add_Suc];
goal Nat.thy "?p : (k+m)+n = k+(m+n)";
by (res_inst_tac [("n","k")] induct 1);
--- a/src/FOLP/ex/Prolog.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/Prolog.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/prolog.ML
+(* Title: FOL/ex/prolog.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
For ex/prolog.thy. First-Order Logic: PROLOG examples
--- a/src/FOLP/ex/ROOT.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/ROOT.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/ex/ROOT
+(* Title: FOLP/ex/ROOT
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Executes all examples for First-Order Logic.
@@ -8,7 +8,7 @@
writeln"Root file for FOLP examples";
-FOLP_build_completed; (*Cause examples to fail if FOLP did*)
+FOLP_build_completed; (*Cause examples to fail if FOLP did*)
proof_timing := true;
--- a/src/FOLP/ex/cla.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/cla.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/ex/cla
+(* Title: FOLP/ex/cla
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Classical First-Order Logic
@@ -207,8 +207,8 @@
result();
writeln"Problem 26";
-goal FOLP.thy "?u : ((EX x. p(x)) <-> (EX x. q(x))) & \
-\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
+goal FOLP.thy "?u : ((EX x. p(x)) <-> (EX x. q(x))) & \
+\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
by (fast_tac FOLP_cs 1);
result();
@@ -301,15 +301,15 @@
result();
writeln"Problem 41";
-goal FOLP.thy "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \
+goal FOLP.thy "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \
\ --> ~ (EX z. ALL x. f(x,z))";
by (best_tac FOLP_cs 1);
result();
writeln"Problem 44";
-goal FOLP.thy "?p : (ALL x. f(x) --> \
-\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
-\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
+goal FOLP.thy "?p : (ALL x. f(x) --> \
+\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
+\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
\ --> (EX x. j(x) & ~f(x))";
by (fast_tac FOLP_cs 1);
result();
--- a/src/FOLP/ex/foundn.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/foundn.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/foundn
+(* Title: FOL/ex/foundn
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
@@ -9,11 +9,11 @@
writeln"File FOL/ex/foundn.";
goal IFOLP.thy "?p : A&B --> (C-->A&C)";
-by (resolve_tac [impI] 1);
-by (resolve_tac [impI] 1);
-by (resolve_tac [conjI] 1);
+by (rtac impI 1);
+by (rtac impI 1);
+by (rtac conjI 1);
by (assume_tac 2);
-by (resolve_tac [conjunct1] 1);
+by (rtac conjunct1 1);
by (assume_tac 1);
result();
@@ -21,9 +21,9 @@
val prems =
goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A; y:B |] ==> f(x,y):C) ==> ?p:C";
by (resolve_tac prems 1);
-by (resolve_tac [conjunct1] 1);
+by (rtac conjunct1 1);
by (resolve_tac prems 1);
-by (resolve_tac [conjunct2] 1);
+by (rtac conjunct2 1);
by (resolve_tac prems 1);
result();
@@ -31,17 +31,17 @@
val prems =
goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
-by (resolve_tac [notI] 1);
+by (rtac notI 1);
by (res_inst_tac [ ("P", "~B") ] notE 1);
-by (resolve_tac [notI] 2);
+by (rtac notI 2);
by (res_inst_tac [ ("P", "B | ~B") ] notE 2);
by (assume_tac 2);
-by (resolve_tac [disjI1] 2);
+by (rtac disjI1 2);
by (assume_tac 2);
-by (resolve_tac [notI] 1);
+by (rtac notI 1);
by (res_inst_tac [ ("P", "B | ~B") ] notE 1);
by (assume_tac 1);
-by (resolve_tac [disjI2] 1);
+by (rtac disjI2 1);
by (assume_tac 1);
result();
@@ -49,23 +49,23 @@
val prems =
goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
-by (resolve_tac [notI] 1);
-by (resolve_tac [notE] 1);
-by (resolve_tac [notI] 2);
-by (eresolve_tac [notE] 2);
-by (eresolve_tac [disjI1] 2);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [notE] 1);
-by (eresolve_tac [disjI2] 1);
+by (rtac notI 1);
+by (rtac notE 1);
+by (rtac notI 2);
+by (etac notE 2);
+by (etac disjI1 2);
+by (rtac notI 1);
+by (etac notE 1);
+by (etac disjI2 1);
result();
val prems =
goal IFOLP.thy "[| p:A | ~A; q:~ ~A |] ==> ?p:A";
-by (resolve_tac [disjE] 1);
+by (rtac disjE 1);
by (resolve_tac prems 1);
by (assume_tac 1);
-by (resolve_tac [FalseE] 1);
+by (rtac FalseE 1);
by (res_inst_tac [ ("P", "~A") ] notE 1);
by (resolve_tac prems 1);
by (assume_tac 1);
@@ -76,25 +76,25 @@
val prems =
goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
-by (resolve_tac [allI] 1);
-by (resolve_tac [disjI1] 1);
+by (rtac allI 1);
+by (rtac disjI1 1);
by (resolve_tac (prems RL [spec]) 1);
(*can use instead
- by (resolve_tac [spec] 1); by (resolve_tac prems 1); *)
+ by (rtac spec 1); by (resolve_tac prems 1); *)
result();
goal IFOLP.thy "?p : ALL x. EX y. x=y";
-by (resolve_tac [allI] 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [refl] 1);
+by (rtac allI 1);
+by (rtac exI 1);
+by (rtac refl 1);
result();
goal IFOLP.thy "?p : EX y. ALL x. x=y";
-by (resolve_tac [exI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [refl] 1) handle ERROR => writeln"Failed, as expected";
+by (rtac exI 1);
+by (rtac allI 1);
+by (rtac refl 1) handle ERROR => writeln"Failed, as expected";
getgoal 1;
@@ -109,12 +109,12 @@
val prems =
goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";
-by (resolve_tac [conjE] 1);
+by (rtac conjE 1);
by (resolve_tac prems 1);
-by (resolve_tac [exE] 1);
+by (rtac exE 1);
by (assume_tac 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [conjI] 1);
+by (rtac exI 1);
+by (rtac conjI 1);
by (assume_tac 1);
by (assume_tac 1);
result();
@@ -122,11 +122,11 @@
(*A bigger demonstration of quantifiers -- not in the paper*)
goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
-by (resolve_tac [impI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [exE] 1 THEN assume_tac 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [allE] 1 THEN assume_tac 1);
+by (rtac impI 1);
+by (rtac allI 1);
+by (rtac exE 1 THEN assume_tac 1);
+by (rtac exI 1);
+by (rtac allE 1 THEN assume_tac 1);
by (assume_tac 1);
result();
--- a/src/FOLP/ex/int.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/int.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/int
+(* Title: FOL/ex/int
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Intuitionistic First-Order Logic
@@ -320,9 +320,9 @@
result();
writeln"Problem 44";
-goal IFOLP.thy "?p : (ALL x. f(x) --> \
-\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
-\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
+goal IFOLP.thy "?p : (ALL x. f(x) --> \
+\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
+\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
\ --> (EX x. j(x) & ~f(x))";
by (Int.fast_tac 1);
result();
--- a/src/FOLP/ex/prop.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/prop.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/prop
+(* Title: FOL/ex/prop
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
First-Order Logic: propositional examples (intuitionistic and classical)
@@ -107,13 +107,13 @@
(* stab-to-peirce *)
goal thy "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
-\ --> ((P --> Q) --> P) --> P";
+\ --> ((P --> Q) --> P) --> P";
by tac;
result();
(* peirce-imp1 *)
goal thy "?p : (((Q --> R) --> Q) --> Q) \
-\ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
+\ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
by tac;
result();
@@ -134,10 +134,10 @@
(* tatsuta *)
goal thy "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \
-\ --> (((P8 --> P2) --> P9) --> P3 --> P10) \
-\ --> (P1 --> P8) --> P6 --> P7 \
-\ --> (((P3 --> P2) --> P9) --> P4) \
-\ --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
+\ --> (((P8 --> P2) --> P9) --> P3 --> P10) \
+\ --> (P1 --> P8) --> P6 --> P7 \
+\ --> (((P3 --> P2) --> P9) --> P4) \
+\ --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
by tac;
result();
--- a/src/FOLP/ex/quant.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ex/quant.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/quant
+(* Title: FOL/ex/quant
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
First-Order Logic: quantifier examples (intuitionistic and classical)
--- a/src/FOLP/hypsubst.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/hypsubst.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOLP/hypsubst
+(* Title: FOLP/hypsubst
ID: $Id$
- Author: Martin D Coen, Cambridge University Computer Laboratory
+ Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Original version of Provers/hypsubst. Cannot use new version because it
@@ -11,11 +11,11 @@
signature HYPSUBST_DATA =
sig
- val dest_eq : term -> term*term
- val imp_intr : thm (* (P ==> Q) ==> P-->Q *)
- val rev_mp : thm (* [| P; P-->Q |] ==> Q *)
- val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
- val sym : thm (* a=b ==> b=a *)
+ val dest_eq : term -> term*term
+ val imp_intr : thm (* (P ==> Q) ==> P-->Q *)
+ val rev_mp : thm (* [| P; P-->Q |] ==> Q *)
+ val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
+ val sym : thm (* a=b ==> b=a *)
end;
signature HYPSUBST =
@@ -44,13 +44,13 @@
fun inspect_pair bnd (t,u) =
case (Pattern.eta_contract t, Pattern.eta_contract u) of
(Bound i, _) => if loose(i,u) then raise Match
- else sym (*eliminates t*)
+ else sym (*eliminates t*)
| (_, Bound i) => if loose(i,t) then raise Match
- else asm_rl (*eliminates u*)
+ else asm_rl (*eliminates u*)
| (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match
- else sym (*eliminates t*)
+ else sym (*eliminates t*)
| (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match
- else asm_rl (*eliminates u*)
+ else asm_rl (*eliminates u*)
| _ => raise Match;
(*Locates a substitutable variable on the left (resp. right) of an equality
@@ -58,25 +58,25 @@
the rule asm_rl (resp. sym). *)
fun eq_var bnd =
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
- | eq_var_aux k (Const("==>",_) $ A $ B) =
- ((k, inspect_pair bnd (dest_eq A))
- (*Exception Match comes from inspect_pair or dest_eq*)
- handle Match => eq_var_aux (k+1) B)
- | eq_var_aux k _ = raise EQ_VAR
+ | eq_var_aux k (Const("==>",_) $ A $ B) =
+ ((k, inspect_pair bnd (dest_eq A))
+ (*Exception Match comes from inspect_pair or dest_eq*)
+ handle Match => eq_var_aux (k+1) B)
+ | eq_var_aux k _ = raise EQ_VAR
in eq_var_aux 0 end;
(*Select a suitable equality assumption and substitute throughout the subgoal
Replaces only Bound variables if bnd is true*)
fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
let val (_,_,Bi,_) = dest_state(state,i)
- val n = length(Logic.strip_assums_hyp Bi) - 1
- val (k,symopt) = eq_var bnd Bi
+ val n = length(Logic.strip_assums_hyp Bi) - 1
+ val (k,symopt) = eq_var bnd Bi
in
- EVERY [REPEAT_DETERM_N k (etac rev_mp i),
- etac revcut_rl i,
- REPEAT_DETERM_N (n-k) (etac rev_mp i),
- etac (symopt RS subst) i,
- REPEAT_DETERM_N n (rtac imp_intr i)]
+ EVERY [REPEAT_DETERM_N k (etac rev_mp i),
+ etac revcut_rl i,
+ REPEAT_DETERM_N (n-k) (etac rev_mp i),
+ etac (symopt RS subst) i,
+ REPEAT_DETERM_N n (rtac imp_intr i)]
end
handle THM _ => no_tac | EQ_VAR => no_tac));
--- a/src/FOLP/intprover.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/intprover.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/int-prover
+(* Title: FOL/int-prover
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
A naive prover for intuitionistic logic
@@ -54,10 +54,10 @@
(*Attack subgoals using safe inferences*)
val safe_step_tac = FIRST' [uniq_assume_tac,
- IFOLP_Lemmas.uniq_mp_tac,
- biresolve_tac safe0_brls,
- hyp_subst_tac,
- biresolve_tac safep_brls] ;
+ IFOLP_Lemmas.uniq_mp_tac,
+ biresolve_tac safe0_brls,
+ hyp_subst_tac,
+ biresolve_tac safep_brls] ;
(*Repeatedly attack subgoals using safe inferences*)
val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
--- a/src/FOLP/simp.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/simp.ML Mon Jan 29 13:58:15 1996 +0100
@@ -76,13 +76,13 @@
rewrite rules are not ordered.*)
fun net_tac net =
SUBGOAL(fn (prem,i) =>
- resolve_tac (Net.unify_term net (strip_assums_concl prem)) i);
+ resolve_tac (Net.unify_term net (strip_assums_concl prem)) i);
(*match subgoal i against possible theorems indexed by lhs in the net*)
fun lhs_net_tac net =
SUBGOAL(fn (prem,i) =>
- biresolve_tac (Net.unify_term net
- (lhs_of (strip_assums_concl prem))) i);
+ biresolve_tac (Net.unify_term net
+ (lhs_of (strip_assums_concl prem))) i);
fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
@@ -113,12 +113,12 @@
val norms =
let fun norm thm =
case lhs_of(concl_of thm) of
- Const(n,_)$_ => n
- | _ => (prths normE_thms; error"No constant in lhs of a norm_thm")
+ Const(n,_)$_ => n
+ | _ => (prths normE_thms; error"No constant in lhs of a norm_thm")
in map norm normE_thms end;
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
- Const(s,_)$_ => s mem norms | _ => false;
+ Const(s,_)$_ => s mem norms | _ => false;
val refl_tac = resolve_tac refl_thms;
@@ -136,7 +136,7 @@
(*Applies tactic and returns the first resulting state, FAILS if none!*)
fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
- Some(thm',_) => thm'
+ Some(thm',_) => thm'
| None => raise THM("Simplifier: could not continue", 0, [thm]);
fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm);
@@ -147,8 +147,8 @@
(*get name of the constant from conclusion of a congruence rule*)
fun cong_const cong =
case head_of (lhs_of (concl_of cong)) of
- Const(c,_) => c
- | _ => "" (*a placeholder distinct from const names*);
+ Const(c,_) => c
+ | _ => "" (*a placeholder distinct from const names*);
(*true if the term is an atomic proposition (no ==> signs) *)
val atomic = null o strip_assums_hyp;
@@ -156,34 +156,34 @@
(*ccs contains the names of the constants possessing congruence rules*)
fun add_hidden_vars ccs =
let fun add_hvars(tm,hvars) = case tm of
- Abs(_,_,body) => add_term_vars(body,hvars)
- | _$_ => let val (f,args) = strip_comb tm
- in case f of
- Const(c,T) =>
- if c mem ccs
- then foldr add_hvars (args,hvars)
- else add_term_vars(tm,hvars)
- | _ => add_term_vars(tm,hvars)
- end
- | _ => hvars;
+ Abs(_,_,body) => add_term_vars(body,hvars)
+ | _$_ => let val (f,args) = strip_comb tm
+ in case f of
+ Const(c,T) =>
+ if c mem ccs
+ then foldr add_hvars (args,hvars)
+ else add_term_vars(tm,hvars)
+ | _ => add_term_vars(tm,hvars)
+ end
+ | _ => hvars;
in add_hvars end;
fun add_new_asm_vars new_asms =
let fun itf((tm,at),vars) =
- if at then vars else add_term_vars(tm,vars)
- fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
- in if length(tml)=length(al)
- then foldr itf (tml~~al,vars)
- else vars
- end
- fun add_vars (tm,vars) = case tm of
- Abs (_,_,body) => add_vars(body,vars)
- | r$s => (case head_of tm of
- Const(c,T) => (case assoc(new_asms,c) of
- None => add_vars(r,add_vars(s,vars))
- | Some(al) => add_list(tm,al,vars))
- | _ => add_vars(r,add_vars(s,vars)))
- | _ => vars
+ if at then vars else add_term_vars(tm,vars)
+ fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
+ in if length(tml)=length(al)
+ then foldr itf (tml~~al,vars)
+ else vars
+ end
+ fun add_vars (tm,vars) = case tm of
+ Abs (_,_,body) => add_vars(body,vars)
+ | r$s => (case head_of tm of
+ Const(c,T) => (case assoc(new_asms,c) of
+ None => add_vars(r,add_vars(s,vars))
+ | Some(al) => add_list(tm,al,vars))
+ | _ => add_vars(r,add_vars(s,vars)))
+ | _ => vars
in add_vars end;
@@ -197,27 +197,27 @@
val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
val hvars = add_new_asm_vars new_asms (rhs,hvars)
fun it_asms (asm,hvars) =
- if atomic asm then add_new_asm_vars new_asms (asm,hvars)
- else add_term_frees(asm,hvars)
+ if atomic asm then add_new_asm_vars new_asms (asm,hvars)
+ else add_term_frees(asm,hvars)
val hvars = foldr it_asms (asms,hvars)
val hvs = map (#1 o dest_Var) hvars
val refl1_tac = refl_tac 1
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)
- (STATE(fn thm =>
- case head_of(rhs_of_eq 1 thm) of
- Var(ixn,_) => if ixn mem hvs then refl1_tac
- else resolve_tac normI_thms 1 ORELSE refl1_tac
- | Const _ => resolve_tac normI_thms 1 ORELSE
- resolve_tac congs 1 ORELSE refl1_tac
- | Free _ => resolve_tac congs 1 ORELSE refl1_tac
- | _ => refl1_tac))
+ (STATE(fn thm =>
+ case head_of(rhs_of_eq 1 thm) of
+ Var(ixn,_) => if ixn mem hvs then refl1_tac
+ else resolve_tac normI_thms 1 ORELSE refl1_tac
+ | Const _ => resolve_tac normI_thms 1 ORELSE
+ resolve_tac congs 1 ORELSE refl1_tac
+ | Free _ => resolve_tac congs 1 ORELSE refl1_tac
+ | _ => refl1_tac))
val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
in thm'' end;
fun add_norm_tags congs =
let val ccs = map cong_const congs
- val new_asms = filter (exists not o #2)
- (ccs ~~ (map (map atomic o prems_of) congs));
+ val new_asms = filter (exists not o #2)
+ (ccs ~~ (map (map atomic o prems_of) congs));
in add_norms(congs,ccs,new_asms) end;
fun normed_rews congs =
@@ -225,7 +225,7 @@
in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))
end;
-fun NORM norm_lhs_tac = EVERY'[resolve_tac [red2], norm_lhs_tac, refl_tac];
+fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
val trans_norms = map mk_trans normE_thms;
@@ -233,15 +233,15 @@
(* SIMPSET *)
datatype simpset =
- SS of {auto_tac: int -> tactic,
- congs: thm list,
- cong_net: thm Net.net,
- mk_simps: thm -> thm list,
- simps: (thm * thm list) list,
- simp_net: thm Net.net}
+ SS of {auto_tac: int -> tactic,
+ congs: thm list,
+ cong_net: thm Net.net,
+ mk_simps: thm -> thm list,
+ simps: (thm * thm list) list,
+ simp_net: thm Net.net}
val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty,
- mk_simps=normed_rews[], simps=[], simp_net=Net.empty};
+ mk_simps=normed_rews[], simps=[], simp_net=Net.empty};
(** Insertion of congruences and rewrites **)
@@ -289,10 +289,10 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let fun find((p as (th,ths))::ps',ps) =
- if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
+ if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
| find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
- print_thm thm;
- ([],simps'))
+ print_thm thm;
+ ([],simps'))
val (thms,simps') = find(simps,[])
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
simps = simps', simp_net = delete_thms(thms,simp_net)}
@@ -311,8 +311,8 @@
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
fun print_ss(SS{congs,simps,...}) =
- (writeln"Congruences:"; prths congs;
- writeln"Rewrite Rules:"; prths (map #1 simps); ());
+ (writeln"Congruences:"; prths congs;
+ writeln"Rewrite Rules:"; prths (map #1 simps); ());
(* Rewriting with conditionals *)
@@ -322,32 +322,32 @@
fun if_rewritable ifc i thm =
let val tm = goal_concl i thm
- fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1)
- | nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k)
- | nobound(Bound n,j,k) = n < k orelse k+j <= n
- | nobound(_) = true;
- fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al
- fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1)
- | find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in
- case f of Const(c,_) => if c=ifc then check_args(al,j)
- else find_if(s,j) orelse find_if(t,j)
- | _ => find_if(s,j) orelse find_if(t,j) end
- | find_if(_) = false;
+ fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1)
+ | nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k)
+ | nobound(Bound n,j,k) = n < k orelse k+j <= n
+ | nobound(_) = true;
+ fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al
+ fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1)
+ | find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in
+ case f of Const(c,_) => if c=ifc then check_args(al,j)
+ else find_if(s,j) orelse find_if(t,j)
+ | _ => find_if(s,j) orelse find_if(t,j) end
+ | find_if(_) = false;
in find_if(tm,0) end;
fun IF1_TAC cong_tac i =
let fun seq_try (ifth::ifths,ifc::ifcs) thm = tapply(
- COND (if_rewritable ifc i) (DETERM(resolve_tac[ifth]i))
- (Tactic(seq_try(ifths,ifcs))), thm)
- | seq_try([],_) thm = tapply(no_tac,thm)
- and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts))
- ORELSE Tactic one_subt, thm)
- and one_subt thm =
- let val test = has_fewer_prems (nprems_of thm + 1)
- fun loop thm = tapply(COND test no_tac
- ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
- ORELSE (refl_tac i THEN Tactic loop)), thm)
- in tapply(cong_tac THEN Tactic loop, thm) end
+ COND (if_rewritable ifc i) (DETERM(rtac ifth i))
+ (Tactic(seq_try(ifths,ifcs))), thm)
+ | seq_try([],_) thm = tapply(no_tac,thm)
+ and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts))
+ ORELSE Tactic one_subt, thm)
+ and one_subt thm =
+ let val test = has_fewer_prems (nprems_of thm + 1)
+ fun loop thm = tapply(COND test no_tac
+ ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
+ ORELSE (refl_tac i THEN Tactic loop)), thm)
+ in tapply(cong_tac THEN Tactic loop, thm) end
in COND (may_match(case_consts,i)) (Tactic try_rew) no_tac end;
fun CASE_TAC (SS{cong_net,...}) i =
@@ -357,7 +357,7 @@
(* Rewriting Automaton *)
datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE
- | PROVE | POP_CS | POP_ARTR | IF;
+ | PROVE | POP_CS | POP_ARTR | IF;
(*
fun pr_cntrl c = case c of STOP => prs("STOP") | MK_EQ => prs("MK_EQ") |
ASMS i => print_int i | POP_ARTR => prs("POP_ARTR") |
@@ -367,7 +367,7 @@
*)
fun simp_refl([],_,ss) = ss
| simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)
- else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);
+ else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);
(** Tracing **)
@@ -381,13 +381,13 @@
(*Select subgoal i from proof state; substitute parameters, for printing*)
fun prepare_goal i st =
let val subgi = nth_subgoal i st
- val params = rev(strip_params subgi)
+ val params = rev(strip_params subgi)
in variants_abs (params, strip_assums_concl subgi) end;
(*print lhs of conclusion of subgoal i*)
fun pr_goal_lhs i st =
writeln (Sign.string_of_term (#sign(rep_thm st))
- (lhs_of (prepare_goal i st)));
+ (lhs_of (prepare_goal i st)));
(*print conclusion of subgoal i*)
fun pr_goal_concl i st =
@@ -404,17 +404,17 @@
if !tracing
then (if not_asms then () else writeln"Assumption used in";
pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm';
- if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
+ if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
else ();
writeln"" )
else ();
(* Skip the first n hyps of a goal, and return the rest in generalized form *)
fun strip_varify(Const("==>", _) $ H $ B, n, vs) =
- if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
- else strip_varify(B,n-1,vs)
+ if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
+ else strip_varify(B,n-1,vs)
| strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =
- strip_varify(t,n,Var(("?",length vs),T)::vs)
+ strip_varify(t,n,Var(("?",length vs),T)::vs)
| strip_varify _ = [];
fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let
@@ -423,73 +423,73 @@
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
else case Sequence.pull(tapply(cong_tac i,thm)) of
- Some(thm',_) =>
- let val ps = prems_of thm and ps' = prems_of thm';
- val n = length(ps')-length(ps);
- val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
- val l = map (fn p => length(strip_assums_hyp(p)))
- (take(n,drop(i-1,ps')));
- in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
- | None => (REW::ss,thm,anet,ats,cs);
+ Some(thm',_) =>
+ let val ps = prems_of thm and ps' = prems_of thm';
+ val n = length(ps')-length(ps);
+ val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
+ val l = map (fn p => length(strip_assums_hyp(p)))
+ (take(n,drop(i-1,ps')));
+ in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
+ | None => (REW::ss,thm,anet,ats,cs);
(*NB: the "Adding rewrites:" trace will look strange because assumptions
are represented by rules, generalized over their parameters*)
fun add_asms(ss,thm,a,anet,ats,cs) =
let val As = strip_varify(nth_subgoal i thm, a, []);
- val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
- val new_rws = flat(map mk_rew_rules thms);
- val rwrls = map mk_trans (flat(map mk_rew_rules thms));
- val anet' = foldr lhs_insert_thm (rwrls,anet)
+ val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
+ val new_rws = flat(map mk_rew_rules thms);
+ val rwrls = map mk_trans (flat(map mk_rew_rules thms));
+ val anet' = foldr lhs_insert_thm (rwrls,anet)
in if !tracing andalso not(null new_rws)
- then (writeln"Adding rewrites:"; prths new_rws; ())
- else ();
- (ss,thm,anet',anet::ats,cs)
+ then (writeln"Adding rewrites:"; prths new_rws; ())
+ else ();
+ (ss,thm,anet',anet::ats,cs)
end;
fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
Some(thm',seq') =>
- let val n = (nprems_of thm') - (nprems_of thm)
- in pr_rew(i,n,thm,thm',more);
- if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
- else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
- thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
- end
+ let val n = (nprems_of thm') - (nprems_of thm)
+ in pr_rew(i,n,thm,thm',more);
+ if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
+ else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
+ thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
+ end
| None => if more
- then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
- thm,ss,anet,ats,cs,false)
- else (ss,thm,anet,ats,cs);
+ then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
+ thm,ss,anet,ats,cs,false)
+ else (ss,thm,anet,ats,cs);
fun try_true(thm,ss,anet,ats,cs) =
case Sequence.pull(tapply(auto_tac i,thm)) of
Some(thm',_) => (ss,thm',anet,ats,cs)
| None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
- in if !tracing
- then (writeln"*** Failed to prove precondition. Normal form:";
- pr_goal_concl i thm; writeln"")
- else ();
- rew(seq,thm0,ss0,anet0,ats0,cs0,more)
- end;
+ in if !tracing
+ then (writeln"*** Failed to prove precondition. Normal form:";
+ pr_goal_concl i thm; writeln"")
+ else ();
+ rew(seq,thm0,ss0,anet0,ats0,cs0,more)
+ end;
fun if_exp(thm,ss,anet,ats,cs) =
- case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of
- Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
- | None => (ss,thm,anet,ats,cs);
+ case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of
+ Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
+ | None => (ss,thm,anet,ats,cs);
fun step(s::ss, thm, anet, ats, cs) = case s of
- MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
- | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
- | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
- | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
- | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
- | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
- | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
- else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs)
- | POP_ARTR => (ss,thm,hd ats,tl ats,cs)
- | POP_CS => (ss,thm,anet,ats,tl cs)
- | IF => if_exp(thm,ss,anet,ats,cs);
+ MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
+ | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
+ | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
+ | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
+ | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
+ | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
+ | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
+ else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs)
+ | POP_ARTR => (ss,thm,hd ats,tl ats,cs)
+ | POP_CS => (ss,thm,anet,ats,tl cs)
+ | IF => if_exp(thm,ss,anet,ats,cs);
fun exec(state as (s::ss, thm, _, _, _)) =
- if s=STOP then thm else exec(step(state));
+ if s=STOP then thm else exec(step(state));
in exec(ss, thm, Net.empty, [], []) end;
@@ -497,9 +497,9 @@
fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
let val cong_tac = net_tac cong_net
in fn i => Tactic(fn thm =>
- if i <= 0 orelse nprems_of thm < i then Sequence.null
- else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
- THEN TRY(auto_tac i)
+ if i <= 0 orelse nprems_of thm < i then Sequence.null
+ else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
+ THEN TRY(auto_tac i)
end;
val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);
@@ -513,7 +513,7 @@
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
let val cong_tac = net_tac cong_net
in fn thm => let val state = thm RSN (2,red1)
- in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end
+ in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end
end;
val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
@@ -529,7 +529,7 @@
| exp_app(i,t) = exp_app(i-1,t $ Bound (i-1));
fun exp_abs(Type("fun",[T1,T2]),t,i) =
- Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1))
+ Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1))
| exp_abs(T,t,i) = exp_app(i,t);
fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0);
@@ -537,20 +537,20 @@
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
let fun xn_list(x,n) =
- let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
- in map eta_Var (ixs ~~ (take(n+1,Ts))) end
+ let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
+ in map eta_Var (ixs ~~ (take(n+1,Ts))) end
val lhs = list_comb(f,xn_list("X",k-1))
val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
fun find_subst tsig T =
let fun find (thm::thms) =
- let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
- val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
- val eqT::_ = binder_types cT
+ let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
+ val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
+ val eqT::_ = binder_types cT
in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
- else find thms
- end
+ else find thms
+ end
| find [] = None
in find subst_thms end;
@@ -558,20 +558,20 @@
let val tsig = #tsig(Sign.rep_sg sg);
val k = length aTs;
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
- let val ca = cterm_of sg va
- and cx = cterm_of sg (eta_Var(("X"^si,0),T))
- val cb = cterm_of sg vb
- and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
- val cP = cterm_of sg P
- and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
- in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
+ let val ca = cterm_of sg va
+ and cx = cterm_of sg (eta_Var(("X"^si,0),T))
+ val cb = cterm_of sg vb
+ and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
+ val cP = cterm_of sg P
+ and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
+ in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
fun mk(c,T::Ts,i,yik) =
- let val si = radixstring(26,"a",i)
- in case find_subst tsig T of
- None => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
- | Some s => let val c' = c RSN (2,ri(s,i,si,T,yik))
- in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end
- end
+ let val si = radixstring(26,"a",i)
+ in case find_subst tsig T of
+ None => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
+ | Some s => let val c' = c RSN (2,ri(s,i,si,T,yik))
+ in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end
+ end
| mk(c,[],_,_) = c;
in mk(refl,rev aTs,k-1,[]) end;
@@ -579,10 +579,10 @@
let val (aTs,rT) = strip_type T;
val tsig = #tsig(Sign.rep_sg sg);
fun find_refl(r::rs) =
- let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
- in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
- then Some(r,(eq,body_type eqT)) else find_refl rs
- end
+ let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
+ in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
+ then Some(r,(eq,body_type eqT)) else find_refl rs
+ end
| find_refl([]) = None;
in case find_refl refl_thms of
None => [] | Some(refl) => [mk_cong sg (f,aTs,rT) refl]
@@ -591,7 +591,7 @@
fun mk_cong_thy thy f =
let val sg = sign_of thy;
val T = case Sign.const_type sg f of
- None => error(f^" not declared") | Some(T) => T;
+ None => error(f^" not declared") | Some(T) => T;
val T' = incr_tvar 9 T;
in mk_cong_type sg (Const(f,T'),T') end;
@@ -601,10 +601,10 @@
let val sg = sign_of thy;
val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
fun readfT(f,s) =
- let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
- val t = case Sign.const_type sg f of
- Some(_) => Const(f,T) | None => Free(f,T)
- in (t,T) end
+ let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
+ val t = case Sign.const_type sg f of
+ Some(_) => Const(f,T) | None => Free(f,T)
+ in (t,T) end
in flat o map (mk_cong_type sg o readfT) end;
end (* local *)
--- a/src/FOLP/simpdata.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/simpdata.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/simpdata
+(* Title: FOL/simpdata
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Simplification data for FOL
@@ -15,33 +15,33 @@
fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
val conj_rews = map int_prove_fun
- ["P & True <-> P", "True & P <-> P",
+ ["P & True <-> P", "True & P <-> P",
"P & False <-> False", "False & P <-> False",
"P & P <-> P",
- "P & ~P <-> False", "~P & P <-> False",
+ "P & ~P <-> False", "~P & P <-> False",
"(P & Q) & R <-> P & (Q & R)"];
val disj_rews = map int_prove_fun
- ["P | True <-> True", "True | P <-> True",
- "P | False <-> P", "False | P <-> P",
+ ["P | True <-> True", "True | P <-> True",
+ "P | False <-> P", "False | P <-> P",
"P | P <-> P",
"(P | Q) | R <-> P | (Q | R)"];
val not_rews = map int_prove_fun
- ["~ False <-> True", "~ True <-> False"];
+ ["~ False <-> True", "~ True <-> False"];
val imp_rews = map int_prove_fun
- ["(P --> False) <-> ~P", "(P --> True) <-> True",
- "(False --> P) <-> True", "(True --> P) <-> P",
- "(P --> P) <-> True", "(P --> ~P) <-> ~P"];
+ ["(P --> False) <-> ~P", "(P --> True) <-> True",
+ "(False --> P) <-> True", "(True --> P) <-> P",
+ "(P --> P) <-> True", "(P --> ~P) <-> ~P"];
val iff_rews = map int_prove_fun
- ["(True <-> P) <-> P", "(P <-> True) <-> P",
+ ["(True <-> P) <-> P", "(P <-> True) <-> P",
"(P <-> P) <-> True",
- "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
+ "(False <-> P) <-> ~P", "(P <-> False) <-> ~P"];
val quant_rews = map int_prove_fun
- ["(ALL x.P) <-> P", "(EX x.P) <-> P"];
+ ["(ALL x.P) <-> P", "(EX x.P) <-> P"];
(*These are NOT supplied by default!*)
val distrib_rews = map int_prove_fun
@@ -60,7 +60,7 @@
val refl_iff_T = make_iff_T refl;
val norm_thms = [(norm_eq RS sym, norm_eq),
- (NORM_iff RS iff_sym, NORM_iff)];
+ (NORM_iff RS iff_sym, NORM_iff)];
(* Conversion into rewrite rules *)
@@ -76,7 +76,7 @@
fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
_ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
| _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
- atomize(th RS conjunct2)
+ atomize(th RS conjunct2)
| _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
| _ $ (Const("True",_)) $ _ => []
| _ $ (Const("False",_)) $ _ => []
@@ -90,15 +90,15 @@
structure FOLP_SimpData : SIMP_DATA =
struct
- val refl_thms = [refl, iff_refl]
- val trans_thms = [trans, iff_trans]
- val red1 = iffD1
- val red2 = iffD2
- val mk_rew_rules = mk_rew_rules
- val case_splits = [] (*NO IF'S!*)
- val norm_thms = norm_thms
- val subst_thms = [subst];
- val dest_red = dest_red
+ val refl_thms = [refl, iff_refl]
+ val trans_thms = [trans, iff_trans]
+ val red1 = iffD1
+ val red2 = iffD2
+ val mk_rew_rules = mk_rew_rules
+ val case_splits = [] (*NO IF'S!*)
+ val norm_thms = norm_thms
+ val subst_thms = [subst];
+ val dest_red = dest_red
end;
structure FOLP_Simp = SimpFun(FOLP_SimpData);
@@ -124,8 +124,8 @@
(fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
val cla_rews = map prove_fun
- ["?p:P | ~P", "?p:~P | P",
- "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"];
+ ["?p:P | ~P", "?p:~P | P",
+ "?p:~ ~ P <-> P", "?p:(~P --> P) <-> P"];
val FOLP_rews = IFOLP_rews@cla_rews;