# HG changeset patch # User clasohm # Date 822920295 -3600 # Node ID d12da312eff42dec9d3441b425a3d0be040ddbd3 # Parent fd510875fb71d4e2cfebdc6a8c6adf50cbdc6ecc expanded tabs diff -r fd510875fb71 -r d12da312eff4 src/CCL/CCL.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/CCL/Fix.ML --- 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. diff -r fd510875fb71 -r d12da312eff4 src/CCL/Gfp.ML --- 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))"; diff -r fd510875fb71 -r d12da312eff4 src/CCL/Hered.ML --- 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. diff -r fd510875fb71 -r d12da312eff4 src/CCL/Lfp.ML --- 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!*) diff -r fd510875fb71 -r d12da312eff4 src/CCL/Set.ML --- 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 ) *) diff -r fd510875fb71 -r d12da312eff4 src/CCL/Term.ML --- 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')", diff -r fd510875fb71 -r d12da312eff4 src/CCL/Trancl.ML --- 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 "[| : r^*; \ \ P(a); \ -\ !!y z.[| : r^*; : r; P(y) |] ==> P(z) |] \ +\ !!y z.[| : r^*; : r; P(y) |] ==> P(z) |] \ \ ==> P(b)"; (*by induction on this formula*) by (subgoal_tac "ALL y. = --> P(y)" 1); @@ -142,7 +142,7 @@ (*elimination of rtrancl -- by induction on a special formula*) val major::prems = goal Trancl.thy "[| : r^*; (a = b) ==> P; \ -\ !!y.[| : r^*; : r |] ==> P |] \ +\ !!y.[| : r^*; : r |] ==> P |] \ \ ==> P"; by (subgoal_tac "a = b | (EX y. : r^* & : r)" 1); by (rtac (major RS rtrancl_induct) 2); @@ -188,7 +188,7 @@ val major::prems = goal Trancl.thy "[| : r^+; \ \ : r ==> P; \ -\ !!y.[| : r^+; : r |] ==> P \ +\ !!y.[| : r^+; : r |] ==> P \ \ |] ==> P"; by (subgoal_tac " : r | (EX y. : r^+ & : r)" 1); by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); diff -r fd510875fb71 -r d12da312eff4 src/CCL/Type.ML --- 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. diff -r fd510875fb71 -r d12da312eff4 src/CCL/Wfd.ML --- 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 *) diff -r fd510875fb71 -r d12da312eff4 src/CCL/coinduction.ML --- 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 =. diff -r fd510875fb71 -r d12da312eff4 src/CCL/equalities.ML --- 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. diff -r fd510875fb71 -r d12da312eff4 src/CCL/eval.ML --- 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 *) diff -r fd510875fb71 -r d12da312eff4 src/CCL/ex/Flag.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/CCL/ex/List.ML --- 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"; diff -r fd510875fb71 -r d12da312eff4 src/CCL/ex/Nat.ML --- 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"; diff -r fd510875fb71 -r d12da312eff4 src/CCL/ex/ROOT.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/CCL/ex/Stream.ML --- 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= & (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= & (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= & (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= & (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); diff -r fd510875fb71 -r d12da312eff4 src/CCL/genrec.ML --- 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 *) diff -r fd510875fb71 -r d12da312eff4 src/CCL/mono.ML --- 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 diff -r fd510875fb71 -r d12da312eff4 src/CCL/subset.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/CCL/typecheck.ML --- 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 *) diff -r fd510875fb71 -r d12da312eff4 src/CTT/Arith.ML --- 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()) : \ -\ 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"; diff -r fd510875fb71 -r d12da312eff4 src/CTT/Bool.ML --- 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*) diff -r fd510875fb71 -r d12da312eff4 src/CTT/CTT.ML --- 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) |] ==> = : 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 diff -r fd510875fb71 -r d12da312eff4 src/CTT/ROOT.ML --- 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*) diff -r fd510875fb71 -r d12da312eff4 src/CTT/ex/ROOT.ML --- 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. diff -r fd510875fb71 -r d12da312eff4 src/CTT/ex/equal.ML --- 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. diff -r fd510875fb71 -r d12da312eff4 src/CTT/ex/synth.ML --- 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)), )"; +\ * Eq(?A, ?b(inr(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)), )"; +\ * Eq(?A(i), ?b(inr(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) \ -\ * Eq(?A, ?b(inr()), j)"; +\ * Eq(?A, ?b(inr()), 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) \ -\ * Eq(?A(i,j), ?b(inr()), j)"; +\ * Eq(?A(i,j), ?b(inr()), 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) \ -\ * Eq(N, ?b(inr()), j)"; + "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl()), i) \ +\ * Eq(N, ?b(inr()), 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); diff -r fd510875fb71 -r d12da312eff4 src/CTT/ex/typechk.ML --- 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 diff -r fd510875fb71 -r d12da312eff4 src/CTT/rew.ML --- 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); diff -r fd510875fb71 -r d12da312eff4 src/Cube/ROOT.ML --- 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*) diff -r fd510875fb71 -r d12da312eff4 src/Cube/ex.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOL/FOL.ML --- 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))) ]); diff -r fd510875fb71 -r d12da312eff4 src/FOL/IFOL.ML --- 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"; diff -r fd510875fb71 -r d12da312eff4 src/FOL/ROOT.ML --- 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*) diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/If.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/List.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/Nat.ML --- 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]; diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/Nat2.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/NatClass.ML --- 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]; diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/Prolog.ML --- 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 diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/ROOT.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/cla.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/foundn.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/int.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/intro.ML --- 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*) diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/mini.ML --- 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); diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/prop.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOL/ex/quant.ML --- 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) diff -r fd510875fb71 -r d12da312eff4 src/FOL/intprover.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOL/simpdata.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOLP/FOLP.ML --- 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)) ]); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/IFOLP.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ROOT.ML --- 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*) diff -r fd510875fb71 -r d12da312eff4 src/FOLP/classical.ML --- 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)); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/If.ML --- 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]; diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/Nat.ML --- 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); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/Prolog.ML --- 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 diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/ROOT.ML --- 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; diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/cla.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/foundn.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/int.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/prop.ML --- 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(); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ex/quant.ML --- 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) diff -r fd510875fb71 -r d12da312eff4 src/FOLP/hypsubst.ML --- 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)); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/intprover.ML --- 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); diff -r fd510875fb71 -r d12da312eff4 src/FOLP/simp.ML --- 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 *) diff -r fd510875fb71 -r d12da312eff4 src/FOLP/simpdata.ML --- 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;