From isabelle-internal-request@cl.cam.ac.uk Thu Apr 18 21:13 CST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id VAA18134 for ; Thu, 18 Apr 1996 21:13:35 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id VAA02412; Thu, 18 Apr 1996 21:10:03 +0930 Received: from albatross.cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with smtp (Exim 0.425 #83) id E0u9rD1-0003BA-00; Thu, 18 Apr 1996 11:45:07 +0100 Received: by albatross.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA27228; Thu, 18 Apr 96 11:45:06 BST Received: from tuminfo2.informatik.tu-muenchen.de [131.159.0.81] (root) by heaton.cl.cam.ac.uk with esmtp (Exim 0.425 #83) id E0u9YyS-0008IV-00; Wed, 17 Apr 1996 16:16:52 +0100 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26507-4>; Wed, 17 Apr 1996 17:16:43 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8192>; Wed, 17 Apr 1996 17:16:24 +0200 Delivery-Date: Wed, 17 Apr 1996 16:16:57 +0100 From: Konrad Slind To: klooster@dutian.twi.tudelft.nl Cc: isabelle-users@cl.cam.ac.uk In-Reply-To: <199604161358.PAA10396@dutian.twi.tudelft.nl> (message from Marnix Klooster on Tue, 16 Apr 1996 16:00:46 +0200) Subject: Re: Defining a Quoting operator Message-Id: <96Apr17.171624met_dst.8192@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 17 Apr 1996 17:16:12 +0200 Content-Type: text Content-Length: 3600 Status: RO > Is it possible to define a quoting operator in Isabelle, and if so: > how? There are different choices. To start, you have to say what your object and meta-languages are. Depending how you are representing weakest precondition semantics, the object language could be 1) a datatype of program syntax in e.g., isabelle-HOL (this is a syntactic (also known as "deep" embedding), 2) Isabelle-HOL extended with semantic definitions for program constructs (a semantic, or "shallow" embedding), 3) an instantiation of Isabelle to the logic of weakest preconditions (a lot like (2)). These are only points along a spectrum of choices. Taking the position that the meta-language is the place where the semantic translation is given, (1) amounts to taking the meta-language as being the HOL logic, and (2) amounts to the meta-language being SML, and I think (3) takes the HOL logic as the metalanguage. > I'd like to be able to use > > `x = 5' > > to denote 'the expression x=5'. This is a value without free > variables. In particular, it is independent of the value of x. It would clarify things here if you could say what the type of `x = 5' is. If you choose option (1) above, you get this for free, since binding constructs and substitution would have to be formalized by you (which can be a lot of work, especially if you consider variable capture issues). If you choose option (2), then you can lose control over variables in your object language, unless special conventions are observed. > To combine quoted expressions, one would write `x + ' which has e > as its only free variable, and e.g. is equal to `x + y*2' if e=`y*2'. This is sometimes known as "antiquotation", stemming from its use in LCF. It's analogous to "backquote" in Lisp. > By definition, `' = e, for any quoted expression e. But it's not that simple, since you want to define this for quotations like your previous one: you need to say how a value `y=2' bound to a metalanguage identifier e gets spliced into a mixed object language- metalanguage expression `x + '. > In case you're wondering, quoting would be very useful in implementing > the weakest preconditions semantics, in which programs are functions > mapping boolean expressions to boolean expressions. The isabelle sources have a development of a Hoare logic for an imperative programming language in .../isabelle/src/HOL/IMP/. This takes approach (1) above, as does Peter Homeier's recent thesis (http://www.cs.ucla.edu/csd-grads-gs2/homeier/html/phd.html). Mike Gordon has taken approach (2) above, starting with the paper (http://www.cl.cam.ac.uk/ftp/hvg/papers/Banffpaper.dvi.gz). A recent report on that work is in @incollection{gordon:hoare_sta, AUTHOR = {Michael Gordon}, TITLE = {A Mechanized {H}oare Logic of State Transitions}, BOOKTITLE = {A Classical Mind: Essays in Honour of {C}. {A}. {R}. {H}oare}, YEAR = 1994, PUBLISHER = {Prentice-Hall International Series in Computer Science}, EDITOR = {A. W. Roscoe}, PAGES = {163-185}} > If anyone has done something similar, I'd like to hear it. The quote/antiquote facility in the SML/NJ compiler is discussed briefly in a paper reachable at ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/slind/papers/qaq.html For either approach (1) or (2), using the quote/antiquote facilties of SML/NJ might get you close to what you want, but that of course depends on what you want. A useful question to ask is whether you want to reason about the object language or in it or both. Cheers, Konrad. From isabelle-internal-request@cl.cam.ac.uk Tue May 14 02:18 CST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id CAA15568 for ; Tue, 14 May 1996 02:18:04 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id CAA05768; Tue, 14 May 1996 02:17:52 +0930 Received: from pochard.cl.cam.ac.uk [128.232.0.62] by heaton.cl.cam.ac.uk with smtp (Exim 0.429 #18) id E0uIzpD-0003K1-00; Mon, 13 May 1996 16:46:19 +0100 Received: by pochard.cl.cam.ac.uk with local (Exim 0.37 #1) id E0uIzon-0005kY-00; Mon, 13 May 1996 16:45:53 +0100 Received: from bettina.informatik.uni-bremen.de [134.102.200.16] (root) by heaton.cl.cam.ac.uk with smtp (Exim 0.429 #18) id E0uIwnD-0002BS-00; Mon, 13 May 1996 13:32:03 +0100 Received: by bettina.informatik.uni-bremen.de (8.7.5/3.10.94m) with SMTP from ganymede.informatik.uni-bremen.de [134.102.207.29] id OAA01980 for ; Mon, 13 May 1996 14:32:44 +0200 (MET DST) Received: by ganymede.Informatik.Uni-Bremen.DE (SMI-8.6/SMI-SVR4) id OAA02198; Mon, 13 May 1996 14:31:46 +0200 From: Burkhart Wolff Date: Mon, 13 May 1996 14:31:46 +0200 Message-Id: <199605131231.OAA02198@ganymede.Informatik.Uni-Bremen.DE> To: isabelle-users@cl.cam.ac.uk Subject: unification blues X-Sun-Charset: US-ASCII Sender: Larry Paulson Content-Type: text Content-Length: 3462 Status: RO I proved some basic squiggol-lemmas over list like >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> qed_goal "foldl_neutr_distr" SList.thy "[| !a.f a e = a; !a.f e a = a; \ \ !a b c.f a (f b c) = f(f a b) c |] \ \ ==> foldl f y A = f y (foldl f e A)" (fn [r_neutr,l_neutr,assoc] => [GEN_ALL "y" 1, list_ind_tac "A" 1, ALLGOALS strip_tac, ALLGOALS(simp_tac (list_ss addsimps [r_neutr,l_neutr])), etac all_dupE 1, rtac trans 1, atac 1, simp_tac (HOL_ss addsimps [assoc RS spec RS spec RS spec RS sym])1, res_inst_tac [("f","%c. f xa c")] arg_cong 1, rtac sym 1, etac allE 1, atac 1]); val [r_neutr,l_neutr,assoc] = goal SList.thy "[| !a.f a e = a; !a.f e a = a; \ \ !a b c.f a (f b c) = f(f a b) c |] \ \ ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"; br trans 1; br foldl_append 1; br trans 1; br ([r_neutr,l_neutr,assoc] MRS foldl_neutr_distr) 1; br refl 1; qed("foldl_append_sym"); <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< and was happy with it for a while. foldl_append_sym works fine together with simp_tac, which can eliminate the assumptions for + :: [nat,nat]=> nat, in arith_ss, for example. Then, I thought it would be convenient to change the form to: qed_goal "foldl_neutr_distr3" SList.thy "[| !!a.f a e = a; !!a.f e a = a; \ \ !!a b c.f a (f b c) = f(f a b) c |] \ \ ==> foldl f y A = f y (foldl f e A)" ... and "[| !!a.f a e = a; !!a.f e a = a; \ \ !!a b c.f a (f b c) = f(f a b) c |] \ \ ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"; ... I expected less fuzz in connection with forward-resolution. BUT - already in the proof: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> val [r_neutr,l_neutr,assoc] = goal SList.thy "[| !!a.f a e = a; !!a.f e a = a; \ \ !!a b c.f a (f b c) = f(f a b) c |] \ \ ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"; br trans 1; br foldl_append 1; br trans 1; br ([r_neutr,l_neutr,assoc] MRS foldl_neutr_distr3) 1; <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< unification seems to loop with a trace like: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> - br ([r_neutr,l_neutr,assoc] MRS foldl_neutr_distr3) 1; Enter MATCH %a b c. f (f (f (f (f (f (f (f c (?c17 b c)) (?c15 b c)) (?c13 b c)) (?c11 b c)) (?c9 b c)) (?c7 b c)) (?c5 b c)) (?c3 b c) =?= %a b c. ?c17 a b %a b c. f (f (f (f (f (f (f (f c (?c17 (f a (f (f (f (f (f (f (f (f b (?c17 a b)) (?c15 a b)) (?c13 a b)) (?c11 a b)) (?c9 a b)) (?c7 a b)) (?c5 a b)) (?c3 a b))) c)) (?c15 (f a (f (f (f (f (f (f (f (f b (?c17 a b)) (?c15 a b)) (?c13 a b)) (?c11 a b)) (?c9 a b)) (?c7 a b)) (?c5 a b)) (?c3 a b))) c)) (?c13 (f a (f (f (f (f (f (f (f (f b (?c17 a b)) (?c15 a b)) (?c13 a b)) (?c11 a b)) (?c9 a b)) (?c7 a b)) (?c5 a b)) (?c3 a b))) c)) (?c11 (f a (f (f (f (f (f [cut] <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< I have two questions: 1). What is the reason for this behaviour? 2). What is the pragmatically best form for this (and similar) theorems? bu -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Tue May 14 01:55 CST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id BAA15497 for ; Tue, 14 May 1996 01:55:13 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id BAA06974; Tue, 14 May 1996 01:55:08 +0930 Received: from pochard.cl.cam.ac.uk [128.232.0.62] by heaton.cl.cam.ac.uk with smtp (Exim 0.429 #18) id E0uJ01c-0003HU-00; Mon, 13 May 1996 16:59:08 +0100 Received: by pochard.cl.cam.ac.uk with local (Exim 0.37 #1) id E0uJ01B-0005lE-00; Mon, 13 May 1996 16:58:41 +0100 Received: from cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with esmtp (Exim 0.429 #18) id E0uJ00o-0003PN-00; Mon, 13 May 1996 16:58:18 +0100 X-Mailer: exmh version 1.6.7 96/05/03+cl To: isabelle-users@cl.cam.ac.uk Subject: Re: unification blues X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Mon, 13 May 1996 16:58:18 +0200 From: Lawrence C Paulson Message-Id: Sender: Larry Paulson Content-Type: text Content-Length: 1265 Status: RO Burkhart's question concerns how to derive rules that have general premises. Normally one should minimize the use of object-level connectives when the same effect can be obtained using meta-level connectives. But when Burkhart removed quantifiers from the premises of his rules, unification went crazy. Function variables are usually to blame when this happens. In the critical command br ([r_neutr,l_neutr,assoc] MRS foldl_neutr_distr3) 1; the rule foldl_neutr_distr3 contains function variables, which allow it to unify with the given rules in countless ways. One might hope, however, that br foldl_neutr_distr3 1; would succeed, and instantiate f. Then the three new subgoals could be eliminated using br three times. This illustrates a limitation of Isabelle, namely that one would like to assume laws like r_neutr, l_neutr, assoc over a limited scope, without discharging them from theorems proved. Then the problematical step indicated in the question would not have to be done at all. Such a facility is compatible with Isabelle's architecture, but I have not thought in detail about its design. -- Larry Paulson -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Wed Jun 19 09:31 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with SMTP id JAA25553 for ; Wed, 19 Jun 1996 09:31:50 +1000 (EST) Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id WAA01912; Tue, 18 Jun 1996 22:37:42 +0930 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id WAA05337 for ; Tue, 18 Jun 1996 22:37:38 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id WAA01902; Tue, 18 Jun 1996 22:37:28 +0930 Received: from pochard.cl.cam.ac.uk [128.232.0.62] by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #1) id E0uW04L-0007js-00; Tue, 18 Jun 1996 13:39:41 +0100 Received: from lcp by pochard.cl.cam.ac.uk with local (Exim 0.52 #1) id E0uW03u-000418-00; Tue, 18 Jun 1996 13:39:14 +0100 X-Mailer: exmh version 1.6.4+cl+patch 10/10/95 Message-Id: From: Larry Paulson To: isabelle-internal@cl.cam.ac.uk Date: Tue, 18 Jun 1996 13:39:14 +0100 Content-Type: text Content-Length: 2070 Status: RO >From bu@informatik.uni-bremen.de Tue Jun 18 12:33:25 1996 Return-path: Delivery-date: Tue, 18 Jun 1996 12:33:25 +0100 Received: from bettina.informatik.uni-bremen.de [134.102.200.16] (root) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #1) id E0uVz2D-0005w4-00; Tue, 18 Jun 1996 12:33:25 +0100 Received: by bettina.informatik.uni-bremen.de (8.7.5/3.10.94m) with SMTP from ganymede.informatik.uni-bremen.de [134.102.207.29] id NAA14475 for ; Tue, 18 Jun 1996 13:33:15 +0200 (MET DST) From: Burkhart Wolff Received: by ganymede.Informatik.Uni-Bremen.DE (SMI-8.6/SMI-SVR4) id NAA03580; Tue, 18 Jun 1996 13:32:57 +0200 Date: Tue, 18 Jun 1996 13:32:57 +0200 Message-Id: <199606181132.NAA03580@ganymede.Informatik.Uni-Bremen.DE> To: isabelle-users@cl.cam.ac.uk Subject: papers available X-Sun-Charset: US-ASCII The following papers are now available and can be drawn via WWW: 1) Kolyang, T.Santen, B. Wolff: A Structure Preserving Encoding of Z in Isabelle/HOL. To appear at The 1996 International Conference on Theorem Proving in Higher Order Logic, Turku, Finland. http://www.informatik.uni-bremen.de/~bu/papers/SPEZ_HOL.22.ps.gz 2) Kolyang, C. Lüth, T. Meyer, B. Wolff: Generating Graphical User Interfaces in a functional Setting. To appear at User Interfaces for Theorem Provers 1996, University of York, England, 19.7.96. http://www.informatik.uni-bremen.de/~bu/papers/uitp96.ps.gz More detailed (and future actualized information) is available on my Isabelle Contribution Page: http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html There will be a public release of all our sources (including our Instance of a GUI for Isabelle) on a public-domain, non-commercial basis. We expect that this will happen in September. bu -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Fri Jun 28 12:34 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with SMTP id MAA16850 for ; Fri, 28 Jun 1996 12:33:48 +1000 (EST) Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id CAA10691; Fri, 28 Jun 1996 02:35:02 +0930 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id CAA27576 for ; Fri, 28 Jun 1996 02:35:00 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id CAA13927; Fri, 28 Jun 1996 02:34:25 +0930 Received: from pochard.cl.cam.ac.uk [128.232.0.62] by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #1) id E0uZK9g-0000dD-00; Thu, 27 Jun 1996 17:42:56 +0100 Received: from lcp by pochard.cl.cam.ac.uk with local (Exim 0.52 #1) id E0uZK9G-0000ge-00; Thu, 27 Jun 1996 17:42:30 +0100 Received: from cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #1) id E0uZJiq-00061I-00; Thu, 27 Jun 1996 17:15:12 +0100 X-Mailer: exmh version 1.6.4+cl+patch 10/10/95 To: isabelle-users@cl.cam.ac.uk Subject: fix for previous posting X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Thu, 27 Jun 1996 17:15:12 +0200 From: Lawrence C Paulson Message-Id: Sender: Larry Paulson Content-Type: text Content-Length: 1940 Status: RO Let me congratulate Jeremy Dawson for finding a fault in Isabelle affecting consistency, the first one for a couple of years. He derives an inconsistency by creating an ill-typed term; he can do this because the meta-rule "combination" does not perform type checking. This builds theorems of the form f(x)=g(y), and one must check that the type of the functions is compatible with that of their arguments. This is a serious fault, but it does not affect normal usage. Isabelle only calls "combination" in three places (correctly it seems). If you'd like to disable this "mk_thm" feature, please replace "combination" in Pure/thm.ML by the code attached. I have already checked that this does not break any proofs in the main object-logics. -- Larry Paulson (*The combination rule f==g t==u ------------ f(t)==g(u) *) fun combination th1 th2 = let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2 fun chktypes (f,t) = (case fastype_of f of Type("fun",[T1,T2]) => if T1 <> fastype_of t then raise THM("combination: types", 0, [th1,th2]) else () | _ => raise THM("combination: not function type", 0, [th1,th2])) in case (prop1,prop2) of (Const("==",_) $ f $ g, Const("==",_) $ t $ u) => let val _ = chktypes (f,t) val thm = (*no fix_shyps*) Thm{sign = merge_thm_sgs(th1,th2), der = infer_derivs (Combination, [der1, der2]), maxidx = max[max1,max2], shyps = shyps1 union shyps2, hyps = hyps1 union hyps2, prop = Logic.mk_equals(f$t, g$u)} in nodup_Vars thm "combination"; thm end | _ => raise THM("combination: premises", 0, [th1,th2]) end; -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Fri Jun 28 12:34 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with SMTP id MAA16991 for ; Fri, 28 Jun 1996 12:34:33 +1000 (EST) Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id BAA05096; Fri, 28 Jun 1996 01:58:05 +0930 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id BAA27474 for ; Fri, 28 Jun 1996 01:58:02 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id BAA13094; Fri, 28 Jun 1996 01:57:52 +0930 Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #1) id E0uZJM2-0007pc-00; Thu, 27 Jun 1996 16:51:38 +0100 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.52 #1) id E0uZJM1-00026e-00; Thu, 27 Jun 1996 16:51:37 +0100 Received: from fang.dsto.defence.gov.au [131.185.2.5] by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #1) id E0uZB6J-0004EC-00; Thu, 27 Jun 1996 08:02:52 +0100 Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id QAA32340; Thu, 27 Jun 1996 16:32:44 +0930 Received: from drambuie.remote.dsto.gov.au (etcell.remote.dsto.gov.au [131.185.47.55]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id QAA24322 for ; Thu, 27 Jun 1996 16:32:35 +0930 (CST) Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id RAA04498 for isabelle-users@cl.cam.ac.uk; Thu, 27 Jun 1996 17:02:18 +1000 (EST) Date: Thu, 27 Jun 1996 17:02:18 +1000 (EST) From: Jeremy Dawson Message-Id: <199606270702.RAA04498@drambuie.remote.dsto.gov.au> To: isabelle-users@cl.cam.ac.uk Subject: odd results Sender: Larry Paulson Content-Type: text Content-Length: 4169 Status: RO When I run ZF and then run either of the following two scripts ------------------------------- print_depth 25; fun tc th = cterm_of (#sign (rep_thm th)) (#prop (rep_thm th)) handle e => print_exn e ; val ti = Type ("i", []) ; val Isct = read_cterm (sign_of thy) ("%x.x", ti --> ti) ; val IsIs = reflexive Isct; val PQct = read_cterm (sign_of thy) ("P <-> Q", propT) ; val PQPQ = (assume PQct) RS (freeze iff_reflection) ; val IsPQ = combination IsIs PQPQ; (* fails tc *) goal thy "~(P <-> Q) ==> P == ~Q"; by (cut_facts_tac it 1); br iff_reflection 1; by (fast_tac FOL_cs 1); val IsPnQ = combination IsIs (topthm()); val IsPQeq = (implies_intr_hyps (IsPQ RS meta_eq_to_obj_eq)) ; val IsPnQeq = (implies_intr_hyps (IsPnQ RS meta_eq_to_obj_eq)) ; IsPnQeq COMP (excluded_middle RS disj_imp_disj); val QnQ = standard (IsPQeq COMP it); (* fails tc *) fun tacthm (Tactic tf) state = case Sequence.pull (tf state) of None => state | Some(x,_) => x ; val disjD1 = tacthm ((atac 4) THEN (atac 3) THEN (etac thin_rl 2)) (notE RSN (2, disjE)); val disjD2 = tacthm ((atac 2) THEN (atac 3) THEN (etac thin_rl 2)) (notE RSN (3, disjE)); val twodiff = prove_goal thy "(x) = (y) | (x) = 0 | (y) = 0" (fn [] => [ rtac disjCI 1, etac swap 1, rtac disjCI 1, rtac (QnQ RS disjD1) 1, etac revcut_rl 1, etac contrapos 1, rtac (QnQ RS disjD1) 1, etac contrapos 1, etac trans 1, etac sym 1 ]) ; val pcs = subset_refl RS (Pow_iff RS iffD2) ; val p0n0 = pcs RS not_emptyI; val l3 = twodiff RS disjD1 RS disjD1 ; val l4 = p0n0 RSN (2, l3) ; val l5 = [p0n0, l4] MRS notE; val l6 = l5 COMP notI RS notnotD ; val a0 = [l6 RS equalityD1, pcs] MRS subsetD RS PowD ; val any = [a0, pcs] MRS subsetD RS emptyE ; ------------------ or ---------------------- print_depth 25; fun tacthm (Tactic tf) state = case Sequence.pull (tf state) of None => state | Some(x,_) => x ; fun tc th = cterm_of (#sign (rep_thm th)) (#prop (rep_thm th)) handle e => print_exn e ; val to = Type ("o", []) ; val Ict = read_cterm (sign_of thy) ("%P.P", to --> to) ; val II = reflexive Ict; val [prem] = goal thy "x == y ==> x == y"; val Ixy = combination II prem; (* fails tc *) val ctIxy = cprop_of Ixy; val xy = zero_var_indexes (assume ctIxy); val ta = TFree ("'a", []); val xct = read_cterm (sign_of thy) ("x", ta); val yct = read_cterm (sign_of thy) ("y", ta); val nxy = transitive (reflexive xct) xy ; val xey = iff_reflection RS (standard nxy) RS meta_eq_to_obj_eq ; val twoodiff = prove_goal thy "((P) <-> (Q)) | ((P) <-> (R)) | ((Q) <-> (R))" (fn [] => [fast_tac FOL_cs 1]) ; val didi = disj_imp_disj RSN (3, disj_imp_disj); val di3 = tacthm ((etac thin_rl 5) THEN (etac thin_rl 4) THEN atac 3) didi ; val twodiff2 = prove_goal thy "x = y | x = z | y = z" (fn [] => [ rtac di3 1, REPEAT (etac xey 2), rtac twoodiff 1]) ; val disjD1 = tacthm ((atac 4) THEN (atac 3) THEN (etac thin_rl 2)) (notE RSN (2, disjE)); val disjD2 = tacthm ((atac 2) THEN (atac 3) THEN (etac thin_rl 2)) (notE RSN (3, disjE)); val pcs = subset_refl RS (Pow_iff RS iffD2) ; val p0n0 = pcs RS not_emptyI; val l2 = [twodiff2, p0n0] MRS disjD1; val [symn] = compose (sym, 2, contrapos) ; val pe = [l2, p0n0 RS symn] MRS disjD2; val pos = [(Pow_iff RS iffD1), empty_subsetI] MRS equalityI ; val a0 = pcs RS (pe RS equalityD1 RS subsetD RS pos) ; val any = [p0n0, a0] MRS notE ; val sany = standard any ; --------------------------------- I get a result of the follwing form val any = "?P" : thm and val sany = "?R" : thm. It seems that these can be resolved with any desired goal, to prove anything you like, eg - goal thy "Pow (0) = 0"; Level 0 Pow(0) = 0 1. Pow(0) = 0 val it = [] : thm list - br any 1; Level 1 Pow(0) = 0 No subgoals! val it = () : unit - topthm(); val it = "Pow(0) = 0" : thm Use of the combination function to produce a result which, when used as an argument to the function tc, produces an error, seems to be crucial to getting these results. Jeremy Dawson -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Tue Sep 17 08:26 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with SMTP id IAA28665 for ; Tue, 17 Sep 1996 08:26:13 +1000 (EST) Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id CAA31044; Tue, 17 Sep 1996 02:16:04 +0930 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id CAA16545 for ; Tue, 17 Sep 1996 02:16:02 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id CAA30113; Tue, 17 Sep 1996 02:15:30 +0930 Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0v2gOA-00077i-00; Mon, 16 Sep 1996 17:19:14 +0100 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0v2gO5-0002Td-00; Mon, 16 Sep 1996 17:19:10 +0100 Received: from rainich.dcs.ed.ac.uk [129.215.160.105] (xtpp) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #2) id E0v2c2g-0005QL-00; Mon, 16 Sep 1996 12:40:46 +0100 Received: from craro.dcs.ed.ac.uk by rainich.dcs.ed.ac.uk with SMTP (PP); Mon, 16 Sep 1996 12:40:00 +0100 Received: from dcs.ed.ac.uk by craro.dcs.ed.ac.uk; Mon, 16 Sep 1996 12:39:57 +0100 Message-Id: <28072.9609161139@craro.dcs.ed.ac.uk> To: isabelle-users@cl.cam.ac.uk Subject: Question about "axiomatic" and "syntactic" type classes Date: Mon, 16 Sep 1996 12:39:56 +0100 From: David Aspinall Sender: Larry Paulson Content-Type: text Content-Length: 2057 Status: RO I've been experimenting with axiomatic type classes. If I define a class of partial orders, like this: po = HOL + consts "<" :: "['a,'a] => bool" (infixl 55) axclass po < term refl "x < x" antisym "[| x < y ; y < x |] ==> x = y" trans "[| x < y ; y < z |] ==> x < z" end Then any putative theorems I write as goals need ugly sort-constraints (e.g. "(x::'a::po)=y ==> x x bool" (infixl 55) at the outset, but I haven't found a way of doing this without Isabelle complaining that "po" is undefined, or multiply defined if I add "classes po < term" or "axclass po < term" before the constant definition. Adding "default po" after the class definition means that I can at least write "(x::'a)=y..." but "x=y..." still gets given sort term. Is there a way of combining the "syntactic" and "axiomatic" class definitions like this? It seems strange that constants that are intended to be used only for the axiomatic type class have to be given a more general type scheme. In the examples in HOL/AxClass, the convention seems to be to use *two* classes each time: one "syntactic" and one "axiomatic". Why is this? Just to allow re-use of constant symbols, or for a deeper reason? (Something to do with the OFCLASS mechanism? How do we understand OFCLASS formally as an extension of the meta-logic?) - David. P.S. Although complaining about typing a few extra characters may seem a bit fussy of me, it would mean that I could much more easily adapt my old files using type classes to the axiomatic mechanism... ---- David Aspinall, email: David.Aspinall@dcs.ed.ac.uk Department of Computer Science, URL: http://www.dcs.ed.ac.uk/home/da University of Edinburgh, Tel: +44 131 650 5898 Edinburgh EH9 3JZ, Scotland. Fax: +44 131 667 7209 -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Mon Sep 23 10:42 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with SMTP id KAA15053 for ; Mon, 23 Sep 1996 10:42:46 +1000 (EST) Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id AAA17792; Sat, 21 Sep 1996 00:17:07 +0930 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id AAA13112 for ; Sat, 21 Sep 1996 00:17:05 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id AAA18303; Sat, 21 Sep 1996 00:16:59 +0930 Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0v46Tk-0008Cl-00; Fri, 20 Sep 1996 15:22:52 +0100 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0v46Tj-0001pp-00; Fri, 20 Sep 1996 15:22:51 +0100 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 Message-Id: From: Larry Paulson To: isabelle-internal@cl.cam.ac.uk Date: Fri, 20 Sep 1996 15:22:51 +0100 Content-Type: text Content-Length: 1571 Status: RO >From nipkow@informatik.tu-muenchen.de Fri Sep 20 13:53:12 1996 Return-path: Delivery-date: Fri, 20 Sep 1996 13:53:12 +0100 Received: from tuminfo2.informatik.tu-muenchen.de [131.159.0.81] (root) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #2) id E0v454w-0007j3-00; Fri, 20 Sep 1996 13:53:10 +0100 Received: from sunbroy49.informatik.tu-muenchen.de ([131.159.1.34]) by tuminfo2.informatik.tu-muenchen.de with ESMTP id <52968-18208>; Fri, 20 Sep 1996 14:52:59 +0200 Received: from sunbroy29.informatik.tu-muenchen.de by sunbroy49.informatik.tu-muenchen.de id <173706-28384>; Fri, 20 Sep 1996 14:52:43 +0200 Sender: Tobias Nipkow From: Tobias.Nipkow@informatik.tu-muenchen.de To: da@dcs.ed.ac.uk CC: isabelle-users@cl.cam.ac.uk In-reply-to: <28072.9609161139@craro.dcs.ed.ac.uk> (message from David Aspinall on Mon, 16 Sep 1996 12:39:56 +0100) Subject: Re: Question about "axiomatic" and "syntactic" type classes Message-Id: <96Sep20.145243+0200met_dst.173706-28384+931@sunbroy49.informatik.tu-muenchen.de> Date: Fri, 20 Sep 1996 14:52:42 +0200 > Then any putative theorems I write as goals need ugly sort-constraints > (e.g. "(x::'a::po)=y ==> x x; Tue, 24 Sep 1996 09:13:32 +1000 (EST) Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id CAA30917; Tue, 24 Sep 1996 02:21:47 +0930 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id CAA21194 for ; Tue, 24 Sep 1996 02:21:45 +0930 (CST) Received: from heaton.cl.cam.ac.uk by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id CAA31359; Tue, 24 Sep 1996 02:21:40 +0930 Received: from woodcock.cl.cam.ac.uk [128.232.2.209] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0v5Dhd-0005ij-00; Mon, 23 Sep 1996 17:17:50 +0100 Received: from lcp by woodcock.cl.cam.ac.uk with local (Exim 0.55 #1) id E0v5Dhc-0002SL-00; Mon, 23 Sep 1996 17:17:48 +0100 Received: from tuminfo2.informatik.tu-muenchen.de [131.159.0.81] (root) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #2) id E0v5DPO-0005af-00; Mon, 23 Sep 1996 16:58:58 +0100 Received: from sunbroy49.informatik.tu-muenchen.de ([131.159.1.34]) by tuminfo2.informatik.tu-muenchen.de with ESMTP id <52912-245>; Mon, 23 Sep 1996 17:58:45 +0200 Received: from localhost by sunbroy49.informatik.tu-muenchen.de with SMTP id <173705-28384>; Mon, 23 Sep 1996 17:58:31 +0200 Date: Mon, 23 Sep 1996 17:58:22 +0200 (MET DST) From: Markus Wenzel To: David Aspinall cc: isabelle-users@cl.cam.ac.uk Subject: Re: Question about "axiomatic" and "syntactic" type classes In-Reply-To: <28072.9609161139@craro.dcs.ed.ac.uk> Message-ID: MIME-Version: 1.0 Sender: Larry Paulson Content-Type: TEXT/PLAIN; charset=US-ASCII Content-Length: 4331 Status: RO On Mon, 16 Sep 1996, David Aspinall wrote: > I've been experimenting with axiomatic type classes. . . > In the examples in HOL/AxClass, the convention seems to be to use > *two* classes each time: one "syntactic" and one "axiomatic". Why is > this? Just to allow re-use of constant symbols, or for a deeper > reason? (Something to do with the OFCLASS mechanism? How do we > understand OFCLASS formally as an extension of the meta-logic?) . . > P.S. Although complaining about typing a few extra characters may seem > a bit fussy of me, it would mean that I could much more easily adapt > my old files using type classes to the axiomatic mechanism... These questions touch the two main issues of Isabelle's type classes as I see them, namely: (1) The formal understanding of classes within the meta-logic. (2) Isabelle's enriched type system (wrt. "ordinary" HOL) as a user convenience tool. >From the point (1) of view, "type classes" are really simple --- that is classes (or predicates) of types. Although polymorphic HOL-like systems (such as Isabelle's meta-logic) are *not* capable of expressing things like some_class::TYPE=>prop, all we need is some_class('a)::prop. I.e. propositions with one free type variable (or "type argument"). The latter can be expressed in polymorphic HOL using some neat trick. Now Isabelle's OFCLASS('a,some_class) is simply concrete syntax for a more complicated term that results from this trick. It can be shown, however, that a very straightforward interpretation of this OFCLASS thing really is "type 'a belongs to some_class". Skipping more details, this should answer your last question above as follows: (Axiomatic) Type Classes are not a proper extension of Isabelle's basic meta-logical system. Rather they are an addition to the syntactic infrastructure (esp. the type inference machinery). In this vein, sort constraints of polymorphic constant declarations (like <::'a::term=>'a=>bool vs. <::'a::po=>'a=>bool) do not make any *logical* difference at all. Of course, there *is* a difference, esp. from the view of point (2) above. Declaring polymorphic constants with different sort constraints may yield different Most General Types by Isabelle's type inference. This way, clever restriction of type variables in constant declarations may save the user typing a lot of sort constraints explicitly. Basically, you're free to declare classes and sort-constrained constants any way you like. Care has to be taken when "class axioms" are introduced, though. A more disciplined (and thus more restricted) mechanism is offered by Isabelle as the "axclass" and "instance" theory sections. The basic idea behind "axclass" is to define some property of types --- usually referring to "characteristic constants" (like < in your example). While "instance" transfers class inclusion and class containment from the logical level into the signature --- thus making it accesible to the type checker. This already hints why constants occurring in class axioms have to be declared *more*generally* than the class they are used to define (i.e. 'a::term instead of 'a::po in your example). Before any class instantiation, "instance" has to prove the class axioms for some conrete type. Now if the "characteristic constants" are declared too strictly, this won't result in a well-typed term. Simply putting these types into the axiomatic class beforehand would *not* be sound in general, of course! So --- as a design decision --- Isabelle's "axclass" section restricts the user in the way you've described in your example. A way to avoid some of these problems is to minimize the number of "chararacteristic constants" in class axioms: If these constants name objects stated to exist, one may reformulate the class axioms with EX quantifiers and name these objects later (for example see HOL/AxClasses/Lattice/Lattice.thy). Another trick may be called "definition of derived constants" (see FOL/ex/NatClass.thy e.g.). That way, "porting" FOL/ex/Nat.ML to NatClass.ML turned out trivial, because most theorems stated something about "+", which was declared with a more restrictive sort constraint. Hope this helps, and please excuse the length. Markus -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From pal@cs.uq.edu.au Tue Aug 27 09:48 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with SMTP id JAA02269 for ; Tue, 27 Aug 1996 09:48:43 +1000 (EST) Received: from itd3.dsto.defence.gov.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id IAA15532; Tue, 27 Aug 1996 08:30:14 +0930 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with SMTP id IAA00740 for ; Tue, 27 Aug 1996 08:30:11 +0930 (CST) Received: from wasabi.cs.uq.edu.au by fang.dsto.defence.gov.au; (8.6.12/1.1.8.2/13May95-0346PM) id IAA09983; Tue, 27 Aug 1996 08:30:11 +0930 Received: from everest.cs.uq.edu.au (pal@everest.cs.uq.edu.au [130.102.16.6]) by wasabi.cs.uq.edu.au (8.7.5/8.7.5) with ESMTP id IAA15473; Tue, 27 Aug 1996 08:59:39 +1000 (EST) Received: (from pal@localhost) by everest.cs.uq.edu.au (8.7.5/8.7.5) id IAA24619; Tue, 27 Aug 1996 08:59:37 +1000 (EST) Date: Tue, 27 Aug 1996 08:59:37 +1000 (EST) Message-Id: <199608262259.IAA24619@everest.cs.uq.edu.au> From: Peter Lindsay To: cliff@cs.man.ac.uk CC: Jeremy.Dawson@dsto.defence.gov.au Subject: [Jeremy.Dawson@dsto.defence.gov.au: replacement rules in LPF] Content-Type: text Content-Length: 3881 Status: RO Cliff, a colleague at DSTO - Jeremy Dawson - sent me the following observation that I think could have important practical ramifications for easing the use of LPF. Perhaps you'd like to comment? cheers peter ------- Start of forwarded message ------- Date: Mon, 26 Aug 1996 12:47:15 +1000 (EST) From: Jeremy Dawson To: pal@cs.uq.oz.au Subject: replacement rules in LPF Content-Type: text Content-Length: 3391 Peter, Some time ago I tried to work out a suitable approach to treating what 'non-denoting' or 'undefined' expressions in an automated theorem proving situation. When I subsequently was referred to a number of papers on this subject I discovered that the approach I'd chosen pretty much equated to that used in LPF. Some of the advantages for using LPF seem to be covered pretty well in the papers I've read (Barringer Cheng & Jones, 1984, A Logic Covering Undefinedness in Program Proofs Cheng & Jones, 1991, On the usability of logics which handle partial functions Jones, 1996, TANSTAAFL (with partial functions) ); however what seemed to me the biggest advantage of using the LPF approach isn't discussed there to any extent. If we define rep (x, y) ("x is replaceable by y") to mean that if x is a denoting expression then it is equal to y, then, in LPF, we have rep (P, Q) implies rep (P|R, Q|R) rep (P, Q) implies rep (R|P, R|Q) rep (P, Q) implies rep (~P, ~Q) (and, as a consequence of the above) rep (P, Q) implies rep (P&R, Q&R) rep (P, Q) implies rep (R&P, R&Q) and, generally, rep (P, Q) implies rep (f(P,R), f(Q,R)) rep (P, Q) implies rep (f(R,P), f(R,Q)) for any function f which can be constructed using | and ~ Now, if we define other operators (eg the arithmetic operators) in such a way as to ensure that they preserve 'replaceability' in the same way (this is trivial when a non-denoting operand produces a non-denoting result), then this facilitates application of replacement rules without a lot of tedious checking of definedness conditions. For example, the algebraic rule a/a = 1 provided a is non-zero is simply rep (a/a, 1); and if we apply it to a sub-expression (eg a/a = b -> P becomes 1 = b -> P) without any checking that it is denoting, then the only way this can change the value of the whole expression is to change it from a non-denoting expression to a denoting one. That is, using a replacement rule of this sort does not change the value of a denoting expression. This fits in perfectly well with the model-theory / proof-theory link in LPF, which is that a valid proof is one which always takes true premises to true results, and may take non-denoting premises to any sort of result (eg the contr rule, E1, ~E1 --------- E2 when E1 is non-denoting and E2 is false). For example, the proof 2 * 0 / 0 = 2 * 0 / 0 (2 * 0) / 0 = 2 * (0 / 0) 0/0 = 2 * 1 1 = 2 which is produced by applying replacement rules to non-denoting terms, follows the same pattern (non-denoting premises and false conclusion). It seemed to me that being able to apply the usual replacements to an expression without having to worry about undefinedness must be a major convenience. Now the papers I've read (listed above) do talk about the logical connectives being monotone (which amounts to saying that if an operand changes from non-denoting to denoting, and this changes the result, then it changes from non-denoting to denoting; ie the operators preserve 'replaceability'). Apart from that, they don't mention anything much related to the above. I'm curious as to whether that is because it is too obvious, well-known or insignificant to be worth mentioning, or is it an additional practical advantage of LPF worth pointing out? I'd much appreciate your comments on the above. Regards, Jeremy Dawson ------- End of forwarded message ------- From Jeremy.Dawson@dsto.defence.gov.au Fri Sep 27 10:30 EST 1996 Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id KAA04509 for jeremy; Fri, 27 Sep 1996 10:30:25 +1000 (EST) Date: Fri, 27 Sep 1996 10:30:25 +1000 (EST) From: Jeremy Dawson Message-Id: <199609270030.KAA04509@drambuie.remote.dsto.gov.au> To: jeremy Subject: copy of mail to lcp Content-Type: text Content-Length: 2682 Status: RO Larry, Yes I was looking at something similar to hyp_subst_tac for a new logic, though I don't think it seems feasible. What I have done is put axioms for LPF, a logic which handles undefined terms (references follow) LPF references

LPF References

A Logic Covering Undefinedness in Program Proofs

by H. Barringer, J.H. Cheng and C. B. Jones; published in Acta Informatica, volume 21, pages 251 -269, 1984.

A Typed Logic of Partial Functions Reconstructed Classically

by C.B. Jones and C.A. Middelburg; published in April 1993 as a technical report from Utrecht University (Logic Group Preprint Series, number 89). To appear in Acta Informatica in 1994.

On the usability of logics which handle partial functions

by J. H. Cheng and C. B. Jones; pages 51 - 69 of 3rd Refinement Workshop, edited by C. Morgan and J. C. P. Woodcock; published by Springer-Verlag, 1991. This is also available as a technical report, UMCS-90-3-1.

Partial functions and logics: A warning

bu C. B. Jones; Information Processing Letters Vol 54, pp 65-67, 1995 has stirred up an interesting controversy on the newsgroups comp.specification.larch and comp.specification.z

into an Isabelle theory, and prove lots of derived theorems, together with a 'replaceability' predicate, where rep (P,Q) means that, if P is defined, then P equals Q. (This is useful since [| rep(P,Q) ; P |] ==> Q is a theorem of the system). (In LPF, a valid derivation takes true to true, and false or undefined to anything). This in turn means that, if a function f satisfies rep (p,q) ==> rep (f(p), f(q)) (*) then we have a sort of substitution rule [| rep(P,Q) ; f(P) |] ==> f(Q) Hence my interest in hyp_subst_tac. One has to prove for each expression f(_) that (*) holds, which is true if f is made up of operators each of which satisfies (*); and I can do this automatically (my tactic, when given the conclusion of the following thm, will create the theorem "(!!x. rep(P(x), Q(x))) ==> rep(ALL x. P(x) --> R(x), ALL x. Q(x) --> R(x))" : thm from a store of theorems which includes val rep_imp = "[| rep(?P1, ?Q1); rep(?R, ?S) |] ==> rep(?P1 --> ?R, ?Q1 --> ?S)" : thm and val rep_ex = "(!!x. rep(?P(x), ?Q(x))) ==> rep(EX x. ?P(x), EX x. ?Q(x))" : thm) One would like to have a tactic which would use the above to (e.g.) rewrite any assumption in a subgoal of the form f(a/a) to f(1), where f satisfies (*), using all the above. I don't think it would be easy. Regards, Jeremy Dawson From Jeremy.Dawson@dsto.defence.gov.au Fri Sep 27 10:29 EST 1996 Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id KAA04489; Fri, 27 Sep 1996 10:29:25 +1000 (EST) Date: Fri, 27 Sep 1996 10:29:25 +1000 (EST) From: Jeremy Dawson Message-Id: <199609270029.KAA04489@drambuie.remote.dsto.gov.au> To: Larry.Paulson@cl.cam.ac.uk Cc: jf@it.dtu.dk Subject: Re: 1996 Reference manual Content-Type: text Content-Length: 3869 Status: RO Larry, > From larry.paulson@cl.cam.ac.uk Fri Sep 27 08:51 EST 1996 > To: Jeremy Dawson > Cc: Jacob Frost > Subject: Re: 1996 Reference manual > Date: Thu, 26 Sep 1996 12:38:19 +0200 > From: Lawrence C Paulson > I strongly advise you to get in touch with Jacob Frost , who is > planning to implement LPF also. You appear to be farther along than he is. Thanks, will do. > As I've told him, I suspect the right way to implement LPF is by exploiting > the fact (I think it's true!) that, for the subset of formulas that are > defined, LPF is identical to classical logic. The idea is to have ordinary > classical logic present, and use fast_tac as usual, and also have some rewrite > rules for mapping general LPF formulas to classical formulas once they are > shown to be defined. Otherwise you have to check, over and over again, that > particular subformulas are defined. Not quite sure what you mean here. Do you mean having two separate sets of operators, eg |, &, --> etc for LPF, and another lot of corresponding ones for classical, with some sort of guarantee that the latter ones would not be applied to undefined arguments? If so, how would this guarantee work (eg in the case of terms entered by the user as goals)? If you mean using the classical rules with extra assumptions (namely the definedness of the terms involved) (which assumptions would be satisfied automatically when the terms had been shown to be defined) then this would be consistent with what I've done so far - I'd have to write an LPF variant of fast_tac with the LPF rules, some of which do include a definedness check among the assumptions. As a matter of fact, a lot of the rules don't actually require any definedness assumption. For example we have the following conjI "[| P; Q |] ==> P&Q" conjunct1 "P&Q ==> P" conjunct2 "P&Q ==> Q" dnI "P ==> ~~P" dnD "~~P ==> P" disjI1 "P ==> P|Q" disjI2 "Q ==> P|Q" disjE "[| P|Q; P ==> R; Q ==> R |] ==> R" notE "[| ~P; P |] ==> Q" FalseE "False ==> P" dn_def "~~P == P" imp_or_def "P-->Q == ~P | Q" or_imp_def "P | Q == ~P-->Q" or_and_def "P | Q == ~ (~P & ~Q)" and_or_def "P & Q == ~ (~P | ~Q)" True_def "True == False-->False" not_imp_def "~P == P-->False" iff_def "P<->Q == (P-->Q) & (Q-->P)" eq_reflection "(x=y) ==> (x==y)" iff_reflection "(P<->Q) ==> (P==Q)" val disjD1 = "[| ?P | ?Q; ~ ?P |] ==> ?Q" : thm val disjD2 = "[| ?Q | ?P; ~ ?P |] ==> ?Q" : thm val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm val mp = "[| ?P1 --> ?Q; ?P1 |] ==> ?Q" : thm val mt = "[| ?P3 --> ?Q; ~ ?Q |] ==> ~ ?P3" : thm qed_goalw "impI" LPF.thy [defl_def, imp_or_def] "[| P ==> Q; defl(P) |] ==> P-->Q" val imp_refl = "defl(?P) ==> ?P --> ?P" : thm val imp_transm = "[| ?P1 --> ?Q2; ?Q2 ==> ?Q1 |] ==> ?P1 --> ?Q1 [logic]" : thm val imp_trans = "[| ?P1 --> ?Q2; ?Q2 --> ?Q1 |] ==> ?P1 --> ?Q1 [logic]" : thm val contrapos = "[| ?P7 ==> ?P; defl(?P7); ~ ?P |] ==> ~ ?P7 [logic]" : thm val excl_middle = "defl(?P) ==> ?P --> ?P" : thm val notI = "[| ?P1 ==> False; defl(?P1) |] ==> ~ ?P1" : thm qed_goalw "classical" LPF.thy [defl_def] "[| ~P ==> P; defl(P) |] ==> P" so it's a minority of LPF rules that need any definedness checking, and we'd want to be able to use the majority without any requirement that the terms involved be defined. Would that be possible under the approach you/ve got in mind? I suppose you could say that the line I'm working on is to reduce the impact of the need to do definedness checking by finding useful rules and tactics that don't require it. Thanks again for you comments. Jeremy (PS BTW, I won't be replying to any email for a fortnight now) From larry.paulson@cl.cam.ac.uk Mon Sep 30 08:45 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id IAA20320 for ; Mon, 30 Sep 1996 08:45:01 +1000 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id TAA12785 for ; Fri, 27 Sep 1996 19:04:51 +0930 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id TAA22281 for ; Fri, 27 Sep 1996 19:04:48 +0930 (CST) Received: from heaton.cl.cam.ac.uk (heaton.cl.cam.ac.uk [128.232.32.11]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with SMTP id TAA16949 for ; Fri, 27 Sep 1996 19:04:47 +0930 (CST) Received: from cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #2) id E0v6ZJG-0002Ws-00; Fri, 27 Sep 1996 10:34:14 +0100 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 To: Jeremy Dawson Cc: jf@it.dtu.dk Subject: Re: 1996 Reference manual X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. In-reply-to: Your message of Fri, 27 Sep 1996 10:29:25 +1000. <199609270029.KAA04489@drambuie.remote.dsto.gov.au> Date: Fri, 27 Sep 1996 10:34:13 +0200 From: Lawrence C Paulson Message-Id: Content-Type: text Content-Length: 1335 Status: RO > > The idea is to have ordinary > > classical logic present, and use fast_tac as usual, and also have some rewrite > > rules for mapping general LPF formulas to classical formulas once they are > > shown to be defined. > Do you mean having two separate sets of operators, eg > |, &, --> etc for LPF, and another lot of corresponding ones for > classical, with some sort of guarantee that the latter ones would > not be applied to undefined arguments? If so, how would this > guarantee work (eg in the case of terms entered by the user as goals)? I can't say that I have ever spelt out the details. In my application, the primary logic was classical HOL, and I needed reflection into a type of booleans that included undefined elements. So one normally expressed formulae in HOL. There was no need for separate versions of the connectives at the boolean level. With LPF one can work with formulae like x=0 | x/x=1. I'm not certain how to handle these. I hadn't realized that one could formalize LPF directly with so few definedness conditions. That being the case one might try to use the classical reasoner directly, using it to prove definedness conditions too. It is not so different from the way it already works, e.g. in ZF. In other words your approach might be better after all. -- Larry From Jeremy.Dawson@dsto.defence.gov.au Tue Oct 15 09:06 EST 1996 Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id JAA25565; Tue, 15 Oct 1996 09:03:39 +1000 (EST) Date: Tue, 15 Oct 1996 09:03:39 +1000 (EST) From: Jeremy Dawson Message-Id: <199610142303.JAA25565@drambuie.remote.dsto.gov.au> To: jf@it.dtu.dk Subject: Re: LPF in Isabelle Content-Type: text Content-Length: 1417 Status: RO Jeremy, I hope you have had a nice holiday. I am quite busy the next couple of days, so I am just going to send you a short mail right now. As a part of a project, I am working on an implementation of LPF in Isabelle. The purpose is to be able to reason effectively about VDM-SL specifications. So far we have essentially implemented the rules from the book "Proof in VDM: A Practitioner's Guide", provided a VDM-SL like concrete syntax with many translations and coded a naive propositional LPF reasoner which appears to work surprisingly well. I do not know how much time you plan to spend on this LPF stuff but think it could be a good idea if we could coordinate our work to obtain a better implementation of LPF in Isabelle. What do you say? Best regards, Jacob Jacob, I'd certainly be keen to collaborate, but I don't have a great deal of time to spend on it. All I have done so far is to formulate the LPF axioms (from the Barringer, Cheng, Jones 1984 paper) and prove a number of theorems. (I think I sent you copies of the LPF.thy and LPF.ML files I had created; if I did not, tell me and I will). Also I have tried to explore this concept of 'replaceability', which I think I told you about before - again, if I did not, let me know. So it seems you have got further than I have; I'd be interrested to see/hear more about your LPF reasoner. Best regards, Jeremy From isabelle-internal-request@cl.cam.ac.uk Wed Oct 16 09:20 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA07237; Wed, 16 Oct 1996 09:20:45 +1000 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id CAA26405; Wed, 16 Oct 1996 02:45:39 +0930 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id CAA24959; Wed, 16 Oct 1996 02:45:37 +0930 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id CAA15090; Wed, 16 Oct 1996 02:45:36 +0930 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id CAA29415; Wed, 16 Oct 1996 02:46:08 +0930 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id CAA19933; Wed, 16 Oct 1996 02:44:36 +0930 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vDCRe-0001IP-00; Tue, 15 Oct 1996 17:34:18 +0100 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vDCRd-0002E8-00; Tue, 15 Oct 1996 17:34:17 +0100 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 Message-Id: From: Larry Paulson To: isabelle-internal@cl.cam.ac.uk Date: Tue, 15 Oct 1996 17:34:17 +0100 Content-Type: text Content-Length: 3357 Status: RO >From niese@ls5.informatik.uni-dortmund.de Tue Oct 15 13:58:18 1996 Return-path: Delivery-date: Tue, 15 Oct 1996 13:58:18 +0100 Received: from fbi-mail.informatik.uni-dortmund.de [129.217.4.40] by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vD94G-0007yJ-00; Tue, 15 Oct 1996 13:58:17 +0100 Received: from issan.informatik.uni-dortmund.de by fbi-mail.informatik.uni-dortmund.de with SMTP (Sendmail 8.7.6/UniDo 3.17) id OAA13056; Tue, 15 Oct 1996 14:57:39 +0200 (MES) Received: from yang.informatik.uni-dortmund.de by issan.informatik.uni-dortmund.de id AA28810; Tue, 15 Oct 96 14:57:38 +0200 Received: by yang.informatik.uni-dortmund.de (NX5.67f2/NX3.0S) id AA04855; Tue, 15 Oct 96 14:57:35 +0200 Message-Id: <9610151257.AA04855@yang.informatik.uni-dortmund.de> Content-Type: text/plain Mime-Version: 1.0 (NeXT Mail 3.3risc v118.3) Received: by NeXT.Mailer (1.118.3) From: Niese Oliver Date: Tue, 15 Oct 96 14:57:34 +0200 To: isabelle-users@cl.cam.ac.uk Subject: "if_then_else" in HOL Dear Users, I trie to proof primitive ADT's under HOL. This is a part of a Theory-File: ----------------------------------------- StructList = HOL+ Nat+ datatype 'a item = i 'a |ErrorItem datatype 'a key = k 'a |ErrorKey datatype ('a, 'b) List = Cons ('a item) ('b key) (('a, 'b) List) |EmptyList datatype ('a, 'b) StructList = Def (('a, 'b) List) |ErrorList consts IsInList :: ['a item, 'b key, ('a, 'b) StructList] => bool rules isin_1 "IsInList x y (Def EmptyList) = False" isin_2 "IsInList x y ErrorList = False" isin_3 "IsInList x y (Def (Cons a b xl)) = (if (x=a & y=b) then True else (IsInList x y (Def xl)))" end Now I add the Simpsets: -------------------------------- val list_ss = HOL_ss addsimps StructList.StructList.simps; val list_ss = list_ss addsimps [StructList.isin_1, StructList.isin_2, StructList.isin_3]; The Prove: --------------- goal StructList.thy "IsInList x y (Def (Cons a b xl)) = IsInList x y (Def xl)"; Level 0 IsInList x y (Def (Cons a b xl)) = IsInList x y (Def xl) 1. IsInList x y (Def (Cons a b xl)) = IsInList x y (Def xl) val it = [] : thm list - by (simp_tac list_ss 1); Level 1 IsInList x y (Def (Cons a b xl)) = IsInList x y (Def xl) 1. (if x = a & y = b then True else IsInList x y (Def xl)) = IsInList x y (Def xl) val it = () : unit My Question: ------------------ How can I solve this prove? I'd tried it with conditions in the goal ([|x ~=a; y ~=b|] ==>IsInList x y (Def (Cons a b xl)) = IsInList x y (Def xl)) but Isabelle ignored the condition. Perhaps there is another way to prove with if_then_else? sincerly Oliver. [Some thoughts on this... 1. To make the simplifier notice assumptions of the subgoal, use asm_simp_tac instead of simp_tac. 2. Many proofs about if-then-else can be done automatically if you use a simpset of the form ss setloop split_tac [expand_if]. 3. Instead of declaring a new datatype ('a,'b)List, you could probably use ('a item * 'b key)list. 4. Instead of if P then True else Q you might use P|Q. 5. I'm not certain your theorem holds in the case x=a, y=b and xl=Emptylist. --lcp] -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From jf@it.dtu.dk Tue Oct 22 10:09 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id KAA16842 for ; Tue, 22 Oct 1996 10:08:59 +1000 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id AAA08769 for ; Tue, 22 Oct 1996 00:33:42 +0930 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id AAA24420 for ; Tue, 22 Oct 1996 00:33:40 +0930 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id AAA05499 for ; Tue, 22 Oct 1996 00:33:40 +0930 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id AAA03015 for ; Tue, 22 Oct 1996 00:34:13 +0930 (CST) Received: from idfs3.it.dtu.dk (idfs3.it.dtu.dk [130.225.76.53]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id AAA00485 for ; Tue, 22 Oct 1996 00:32:48 +0930 (CST) Received: from solaris1 (solaris1.it.dtu.dk [130.225.76.59]) by idfs3.it.dtu.dk (8.6.10/8.6.4) with SMTP id RAA17131; Mon, 21 Oct 1996 17:03:04 +0200 Sender: jf@it.dtu.dk Message-ID: <326B9047.2CDE@it.dtu.dk> Date: Mon, 21 Oct 1996 17:01:27 +0200 From: Jacob Frost Organization: Department of Information Technology X-Mailer: Mozilla 3.0Gold (X11; I; SunOS 5.5.1 sun4u) MIME-Version: 1.0 To: Jeremy Dawson CC: jf@it.dtu.dk Subject: Workshop Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=us-ascii Content-Length: 2851 Status: RO Dear Colleague, This is an invitation to participate in an informal workshop to be held at IFAD in Odense, Denmark on November 28--29, 1996 in connection with the project "Towards Industrially Applicable Proof Support for VDM-SL". As you may know IFAD and DTU are working on a proof support tool for the VDM Specification Language in a two-year project supported by the Danish Technical Science Research Council. At the end of the first year we would like to collect a group of experts in VDM and theorem proving technology for a two-day workshop in order to present our first prototype system and discuss future directions for industrially applicable proof support systems for VDM-SL and specification languages in general. The proof support tool that we are currently developing will be integrated with the IFAD VDM-SL Toolbox (see http://www.ifad.dk for more information). This Toolbox supports that formal specifications in VDM-SL can be parsed, type checked, and tested/debugged using an interpreter/debugger. It also supports automatic code generation of fully executable code in C++. The proof support tool further extends the functionality to also support reasoning about specifications, in particular, proving type correctness obligations generated by a new extended type checker. We plan to use the Isabelle system as the theorem proving engine of the proof support tool and are currently developing an LPF and VDM-SL instantiation of Isabelle. Other main components of the proof support system are a Proof Manager and a Proof Editor, which among other things provides a graphical user interface to Isabelle. We sincerely hope that you are interested in attending this workshop. Please let us know as soon as possible if you might be interested in attending and would like to receive more information this Autumn. It is free to attend the workshop, IFAD provides meals and coffee during breaks. Unfortunately we are not able to pay for travel and accommodation expenses of the attendees. Information on how to get to IFAD can be obtained from http://www.ifad.dk/travelinfo/travelinfo.html. This invitation has been sent to a fairly small group of people since we would like to keep the workshop small (and closed). If you are aware of someone not invited, who might be interested, then please send us a mail. If you want more information on the workshop now, on the proof support tool or on anything else, please contact us at the addresses below. Yours sincerely, Sten Agerholm and Peter Gorm Larsen sten@ifad.dk peter@ifad.dk ------------------------------------------------------------- The Institute of Applied Computer Science (IFAD) Forskerparken 10, DK-5230 Odense M, Denmark Phone: +45-63157131, Fax: +45-65-932999 WWW: http://www.ifad.dk ------------------------------------------------------------- From jf@it.dtu.dk Tue Oct 22 10:09 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id KAA16848 for ; Tue, 22 Oct 1996 10:09:04 +1000 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id AAA05033 for ; Tue, 22 Oct 1996 00:23:10 +0930 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id AAA24235 for ; Tue, 22 Oct 1996 00:23:08 +0930 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id AAA11352 for ; Tue, 22 Oct 1996 00:23:08 +0930 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id AAA13124 for ; Tue, 22 Oct 1996 00:23:39 +0930 (CST) Received: from idfs3.it.dtu.dk (idfs3.it.dtu.dk [130.225.76.53]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id AAA06136 for ; Tue, 22 Oct 1996 00:22:14 +0930 (CST) Received: from solaris1 (solaris1.it.dtu.dk [130.225.76.59]) by idfs3.it.dtu.dk (8.6.10/8.6.4) with SMTP id QAA16789; Mon, 21 Oct 1996 16:52:16 +0200 Sender: jf@it.dtu.dk Message-ID: <326B8DC0.5560@it.dtu.dk> Date: Mon, 21 Oct 1996 16:50:40 +0200 From: Jacob Frost Organization: Department of Information Technology X-Mailer: Mozilla 3.0Gold (X11; I; SunOS 5.5.1 sun4u) MIME-Version: 1.0 To: Jeremy Dawson CC: sten@ifad.dk, jf@it.dtu.dk Subject: Re: LPF in Isabelle References: <199610142303.JAA25565@drambuie.remote.dsto.gov.au> Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=us-ascii Content-Length: 1985 Status: RO Jeremy, I have looked a bit at your files. From this it looks to me as you are interested in rewriting (or simplification) in LPF. Is this correct? How does rep differ from (weak) equality? The simple reasoner in our LPF instantiation of Isabelle is based on the ideas of Jen Huan Cheng described in his thesis "A Logic for Partial Function". As I see it, the essence is that instead of breaking down negated formulas on the each side of a sequent by removing the negation and moving them to the other side, one uses rules for distributing negation over the other connectives. Also one has to recognise a sequent as valid when a formula and its negation both occurs on the left hand side of a sequent. The natural deduction system of LPF causes further complications since it does not allow, for example, disjunction to be broken down as in sequent caluculus (only one formula on the rhs). So far we work around this problem by using backtracking, but perhaps we will have to code another solution in the future. I think we should try to work out a way to collaborate. As we (me and Sten Agerholm) already have a quite big LPF frame, I imagine that you could work on an interresting part of this. What do you think? Perhaps you would be interrested in setting up/constructing a powerful simplifier for LPF? Could you tell me some more about what you would be interested in doing? As for our project, I can tell you that it is quite practical oriented, aiming at constructing, amongst other things, an LPF instantiation powerful enough to prove realistic properties about VDM specifications. Until the 28/29 nov. 96 we will be busy constructing a prototype for a project workshop we will host here in Denmark. You are very welcome to attend. I will send you some more information. If you are interested, then I will make a new version of our LPF instantiation (still very much a prototype) available to you in a couple of days when it is finished. So what do you say? Jacob From Jeremy.Dawson@dsto.defence.gov.au Thu Oct 24 09:57 EST 1996 Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id JAA11828; Thu, 24 Oct 1996 09:54:45 +1000 (EST) Date: Thu, 24 Oct 1996 09:54:45 +1000 (EST) From: Jeremy Dawson Message-Id: <199610232354.JAA11828@drambuie.remote.dsto.gov.au> To: jf@it.dtu.dk Subject: Re: LPF in Isabelle Content-Type: text Content-Length: 2220 Status: RO Jacob, I have looked a bit at your files. From this it looks to me as you are interested in rewriting (or simplification) in LPF. Is this correct? How does rep differ from (weak) equality? Yes, that's pretty much correct. At least, I am interested in exploring whether this rep relation and its properties are useful for doing rewriting / simplification while avoiding the need to prove defined-ness of everything that gets rewritten. rep differs from weak equality in that if the first operand is undefined, then rep (_,_) is true; if the first operand is defined, then rep (_,_) is the same as weak equality I think we should try to work out a way to collaborate. As we (me and Sten Agerholm) already have a quite big LPF frame, I imagine that you could work on an interresting part of this. What do you think? Perhaps you would be interrested in setting up/constructing a powerful simplifier for LPF? Could you tell me some more about what you would be interested in doing? As for our project, I can tell you that it is quite practical oriented, aiming at constructing, amongst other things, an LPF instantiation powerful enough to prove realistic properties about VDM specifications. Until the 28/29 nov. 96 we will be busy constructing a prototype for a project workshop we will host here in Denmark. You are very welcome to attend. I will send you some more information. If you are interested, then I will make a new version of our LPF instantiation (still very much a prototype) available to you in a couple of days when it is finished. I'm keen to collaborate but my time to spend on this LPF work is very limited. Since I'm interested in exploring the potential of this rep relation, and seeing how it could be used in a semi-automatic way, that would occupy the time I can spend on LPF for a while. However I'd certainly like to see your LPF instantiation; I could see whether what I do could fit into it, and try to ensure that anything I do does fit in. Thanks for the invitation to the workshop; however I'm afraid it's too far, and LPF is peripheral to my main work, and in our organization it's very difficult to get overseas travel anyway. Jeremy From isabelle-internal-request@cl.cam.ac.uk Mon Oct 28 11:04 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id LAA08676; Mon, 28 Oct 1996 11:04:27 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id BAA04942; Sat, 26 Oct 1996 01:42:55 +0930 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id BAA02708; Sat, 26 Oct 1996 01:42:52 +0930 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id BAA04612; Sat, 26 Oct 1996 01:42:52 +0930 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id BAA01336; Sat, 26 Oct 1996 01:43:24 +0930 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id BAA09026; Sat, 26 Oct 1996 01:39:49 +0930 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vGoMK-0003tF-00; Fri, 25 Oct 1996 16:39:44 +0100 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vGoMI-0007Tj-00; Fri, 25 Oct 1996 16:39:42 +0100 Received: from bettina.informatik.uni-bremen.de [134.102.200.16] (root) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vGn2C-0003G9-00; Fri, 25 Oct 1996 15:14:52 +0100 Received: by bettina.informatik.uni-bremen.de (8.7.5/3.10.94m) with SMTP from ganymede.informatik.uni-bremen.de [134.102.207.29] id PAA14820 for ; Fri, 25 Oct 1996 15:14:38 +0100 (MET) Received: by ganymede.Informatik.Uni-Bremen.DE (SMI-8.6/SMI-SVR4) id QAA09443; Fri, 25 Oct 1996 16:14:19 +0200 From: Burkhart Wolff Date: Fri, 25 Oct 1996 16:14:19 +0200 Message-Id: <199610251414.QAA09443@ganymede.Informatik.Uni-Bremen.DE> To: isabelle-users@cl.cam.ac.uk Subject: Metalogik vs. HOL X-Sun-Charset: US-ASCII Sender: Larry Paulson Content-Type: text Content-Length: 533 Status: RO In Isabelle/HOL, due to "eq_reflection" (meta_eq_to_obj_eq is already a consequence of the rules of the meta-logic), == and = are very tightly coupled together semantically. As a consequence, several "axioms" in Isabelle/HOL are in fact theorems (e.g. "refl" or, as far as I can see, also "ext" and "iff"). Does anybody know what would be a "minimal" axiomatization of HOL on the basis of Pure and "eq_reflection"? bu -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From bu@Informatik.Uni-Bremen.DE Tue Oct 29 10:15 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id KAA18085 for ; Tue, 29 Oct 1996 10:12:25 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id VAA09125 for ; Mon, 28 Oct 1996 21:49:55 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id VAA19966 for ; Mon, 28 Oct 1996 21:49:52 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id VAA07951 for ; Mon, 28 Oct 1996 21:49:53 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id VAA26352 for ; Mon, 28 Oct 1996 21:50:26 +1030 (CST) Received: from bettina.informatik.uni-bremen.de (root@bettina.informatik.uni-bremen.de [134.102.200.16]) by digger1.defence.gov.au (8.7.5/8.7.3) with ESMTP id VAA20023 for ; Mon, 28 Oct 1996 21:48:49 +1030 (CST) Received: by bettina.informatik.uni-bremen.de (8.7.5/3.10.94m) with SMTP from ganymede.informatik.uni-bremen.de [134.102.207.29] id MAA09400 for ; Mon, 28 Oct 1996 12:19:07 +0100 (MET) Received: by ganymede.Informatik.Uni-Bremen.DE (SMI-8.6/SMI-SVR4) id MAA24667; Mon, 28 Oct 1996 12:18:56 +0100 From: Burkhart Wolff Date: Mon, 28 Oct 1996 12:18:56 +0100 Message-Id: <199610281118.MAA24667@ganymede.Informatik.Uni-Bremen.DE> To: Jeremy.Dawson@dsto.defence.gov.au Subject: Re: Metalogik vs. HOL X-Sun-Charset: US-ASCII Content-Type: text Content-Length: 268 Status: RO Dear Jeremy, seems that you are right and you need something stronger for eq_reflection: "?x = ?y == ?x == ?y" : thm in order to proceed with "plan" to build HOL.thy just on top of Pure by conservative extensions plus an axiom for Hilbert and classicality. bu From Jeremy.Dawson@dsto.defence.gov.au Mon Nov 4 10:40 EST 1996 Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id KAA01423; Mon, 4 Nov 1996 10:40:06 +1100 (EST) Date: Mon, 4 Nov 1996 10:40:06 +1100 (EST) From: Jeremy Dawson Message-Id: <199611032340.KAA01423@drambuie.remote.dsto.gov.au> To: jf@it.dtu.dk Subject: Re: LPF Content-Type: text Content-Length: 5410 Status: RO Jacob, Yes, thanks, I got your mail I've managed to get tactics which make use of the 'replaceable' relation I mentioned earlier. Using 'idemp_or' which is rep(P|P, P) I can essentially use that to simplify an expression involving P|P to one involving P, without having to do explicit definedness checks. It only can be used in a forward proof mode, so for the demo I put in an irrelevant goal "X". Although in fact P|P == P, so in this particular case, the result could be achieved using ordianry rewriting, the functions shown below would be equally applicable for rep (a,b) where a may be undefined when b is not, for example, replacing a/a by 1 (where they're not identical when a is be 0). Some of the code (which is a bit of a mess but I've included it in case you want to look at it), and then some examples, (labelled "(*demo") follow. Regards, Jeremy val oT = Type ("o", []) ; val Trpp = Const ("Trueprop", oT --> propT) ; (* dest_rep : term -> term * term, takes term of the form rep (a,b) and returns (a, b) *) fun dest_rep (Const ("Trueprop", _) $ (Const ("rep", _) $ l $ r)) = (l, r) | dest_rep (Const ("Trueprop", _) $ (Const ("rept", _) $ l $ r)) = (l, r) | dest_rep tm = raise TERM ("dest_rep: not rep(_,_) or rept(_,_)", [tm]); (* rep_to_def : term -> term, takes term of the form rep (a,b) and returns term of the form a==b *) val rep_to_def = Logic.mk_equals o dest_rep (* rdthm: thm -> thm, as above, from and to theorems *) fun rdthm rth = let val {sign, prop, ...} = rep_thm rth in trivial (cterm_of sign (rep_to_def prop)) end ; fun rt (Const ("Trueprop",_) $ eo) = eo; val st = Sign.string_of_term (sign_of thy); val tot = term_of o cprop_of ; (* mtcht : term * term -> (indexname * typ) list * (indexname * term) list, mtcht t1 t2 returns lists of assignments to type and term variables of t1 which will make it the same as t2 *) val mtcht = Pattern.match (#tsig (Sign.rep_sg (sign_of thy))) ; (* fun subst_whole pat rep obj = ren_inst (mtcht (pat, obj), rep, pat, obj); *) fun subst_whole pat rep obj = subst_vars (mtcht (pat, obj)) rep ; (* subst_rep : term -> term -> term -> string list -> term, subst_rep pat rep obj [] gives obj, with subterms corresponding to pat changed to rep *) fun subst_rep pat rep obj bounds = subst_whole pat rep obj handle Pattern.MATCH => case obj of t$u => subst_rep pat rep t bounds $ subst_rep pat rep u bounds | Abs(a,T,t) => let val b = variant bounds a val v = Free("." ^ b,T) val t' = subst_rep pat rep (subst_bounds([v],t)) (b::bounds) in Abs(a, T, abstract_over(v,t')) end | t => t ; fun mk_rep (Const ("Trueprop", _) $ t1) (Const ("Trueprop", _) $ t2) = Trpp $ (Const ("rep", [oT,oT] ---> oT) $ t1 $ t2) (* rep_sub : thm -> term -> term, rule is of the form rep (a,b), returns term rep (obj, sub), where sub is obj with instances of a changed to b *) fun rep_sub rule obj = let val (pat, rep) = dest_rep (concl_of rule) val sub = subst_rep pat rep obj [] in mk_rep obj sub end ; val idemp_or = prove_goal LPF.thy "rep (P|P, P)" (fn _ => [rtac repI 1, etac disjE 1, atac 1, atac 1, etac norD1 1]); (* rep_simp_thm : thm -> term -> thm *) fun rep_simp_thm reprule prem = let val tr = trivial (cterm_of (sign_of thy) (rep_sub reprule prem)) val u = tacthm (REPEAT (SOMEGOAL rep_tac)) tr val v = tacthm (REPEAT (SOMEGOAL (rtac reprule))) u in v RS repD end ; (* rep_simp_tac : thm -> int -> int -> thm -> thm Sequence.seq *) fun rep_simp_tac reprule sg pr state = let val (_,_,sgt,_) = dest_state (state, sg) val (prem::_,_) = Logic.strip_prems (pr,[],sgt) in dtac (rep_simp_thm reprule prem) sg state end ; (* rep_simp_rule : thm -> thm -> thm *) fun rep_simp_rule reprule thm = thm RS (rep_simp_thm reprule (concl_of thm)) ; EXAMPLES FOLLOW (* demo goal thy "X"; by (subgoal_tac "P | P <-> (Q | Q) | (R | R) & (S | S)" 1); val (_,_,sgt,_) = dest_state (topthm(), 1); val stsgt = st sgt; val (prem::_,_) = Logic.strip_prems (1,[],sgt); val stpr = st prem; val r = rep_sub idemp_or prem; val str = st r; val tr = trivial (cterm_of sign r); val u = tacthm (REPEAT (SOMEGOAL rep_tac)) tr; val v = tacthm (REPEAT (SOMEGOAL (rtac idemp_or))) u; val w = v RS repD; by (rep_simp_tac idemp_or 1 1); - Level 1 X 1. P | P <-> (Q | Q) | (R | R) & (S | S) ==> X 2. P | P <-> (Q | Q) | (R | R) & (S | S) val stsgt = "P | P <-> (Q | Q) | (R | R) & (S | S) ==> X" : string val stpr = "P | P <-> (Q | Q) | (R | R) & (S | S)" : string val str = "rep(P | P <-> (Q | Q) | (R | R) & (S | S), P <-> Q | R & S)" val tr = "rep(P | P <-> (Q | Q) | (R | R) & (S | S), P <-> Q | R & S) ==> rep(P | P <-> (Q | Q) | (R | R) & (S | S), P <-> Q | R & S)" : thm val u = "[| rep(P | P, P); rep(Q | Q, Q); rep(R | R, R); rep(S | S, S) |] ==> rep(P | P <-> (Q | Q) | (R | R) & (S | S), P <-> Q | R & S)" : thm val v = "rep(P | P <-> (Q | Q) | (R | R) & (S | S), P <-> Q | R & S)" : thm val w = "P | P <-> (Q | Q) | (R | R) & (S | S) ==> P <-> Q | R & S" : thm Level 2 X 1. P <-> Q | R & S ==> X 2. P | P <-> (Q | Q) | (R | R) & (S | S) *) (* demo val [p] = goal thy "P | P <-> (Q | Q) | (R | R) & (S | S) ==> X"; val rp = rep_simp_rule idemp_or p; val p = "P | P <-> (Q | Q) | (R | R) & (S | S) [P | P <-> (Q | Q) | (R | R) & (S | S)]" : thm val rp = "P <-> Q | R & S [P | P <-> (Q | Q) | (R | R) & (S | S)]" : thm *) From Jeremy.Dawson@dsto.defence.gov.au Thu Nov 7 16:57 EST 1996 Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id QAA11279; Thu, 7 Nov 1996 16:57:34 +1100 (EST) Date: Thu, 7 Nov 1996 16:57:34 +1100 (EST) From: Jeremy Dawson Message-Id: <199611070557.QAA11279@drambuie.remote.dsto.gov.au> To: jf@it.dtu.dk Subject: LPF in Isabelle Content-Type: text Content-Length: 437 Status: RO Jacob, Thanks for your big file; I haven't had much of a look at it yet. However I noticed that there are 'obviously stronger' results available than your theorems not_def_intr and not_def_elim, as follows not_not_intr RS contr ; (* cf not_def_intr *) prove_goalw Prop.thy [def_def] "not def P ==> Q" (* cf not_def_elim *) (fn [p] => [ rtac (p RS not_or_elim) 1, etac contr 1, etac not_not_dest 1]); Regards, Jeremy From isabelle-internal-request@cl.cam.ac.uk Thu Nov 14 09:05 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA05078; Thu, 14 Nov 1996 09:04:16 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id EAA28783; Thu, 14 Nov 1996 04:07:15 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id EAA16782; Thu, 14 Nov 1996 04:07:12 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id EAA31250; Thu, 14 Nov 1996 04:07:12 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id EAA30254; Thu, 14 Nov 1996 04:07:45 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id EAA11698; Thu, 14 Nov 1996 04:07:43 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vNibI-0007nU-00; Wed, 13 Nov 1996 16:55:44 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vNibG-0006YN-00; Wed, 13 Nov 1996 16:55:42 +0000 Received: from cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #2) id E0vNiZD-0007ew-00; Wed, 13 Nov 1996 16:53:35 +0000 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 To: isabelle-users@cl.cam.ac.uk Subject: isabelle update: 94-7 X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Wed, 13 Nov 1996 16:53:35 +0100 From: Lawrence C Paulson Message-Id: Sender: Larry Paulson Content-Type: text Content-Length: 1854 Status: RO A new update of Isabelle, Isabelle94-7, is now available from Cambridge. The URL is ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz It is also on the Munich site, at URL http://www4.informatik.tu-muenchen.de/~nipkow/isadist/Isabelle94-7.tar.gz Here is a summary of changes from Isabelle94-6. The correction of a performance problem yields a super-linear speedup for large simplifications. Poly/ML users should note a further 20% speed increase. FOL, ZF and HOL now use miniscoping: rewriting pushes quantifications in as far as possible. This aids the classical reasoner but could make existing proofs fail. You can suppress it using the command Delsimps (ex_simps @ all_simps); De Morgan laws are also now included, by default. Revised Makefiles now allow ISABELLECOMP to start with a /. Unfortunately, people have reported compatibility problems with gmake. Pretty-printing has been changed for ==> : ~: to improve readability. Commands prlev and choplev now accept a negative argument. For example, choplev ~2 is equivalent to chop(); chop(). Tab characters are replaced by blanks in theory files. The new object-logic Sequents adds linear logic, while replacing LK and Modal (thanks to Sara Kalvala). HOL/Auth is a new directory of examples: correctness proofs for authentication protocols. HOL now has auto_tac, which combines rewriting and classical reasoning: try it! (There are many examples on HOL/Auth.) HOL: the command AddIffs is available for declaring theorems of the form P=Q to the rewriter and classical reasoner simultaneously. Function uresult no longer returns theorems in "standard" format. To regain the previous version, declare val uresult = standard o uresult; -- Larry Paulson -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Mon Nov 18 08:29 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id IAA24672; Mon, 18 Nov 1996 08:28:57 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id WAA05207; Sun, 17 Nov 1996 22:10:40 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id WAA11273; Sun, 17 Nov 1996 22:10:36 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id WAA16074; Sun, 17 Nov 1996 22:10:37 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id WAA11433; Sun, 17 Nov 1996 22:11:10 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id WAA10160; Sun, 17 Nov 1996 22:13:16 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vP5Mt-0000t6-00; Sun, 17 Nov 1996 11:26:31 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vP5Ms-0002kN-00; Sun, 17 Nov 1996 11:26:30 +0000 Received: from bettina.informatik.uni-bremen.de [134.102.200.16] (root) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vOO7D-0006IR-00; Fri, 15 Nov 1996 13:15:28 +0000 Received: by bettina.informatik.uni-bremen.de (8.7.5/3.10.94m) with SMTP from ganymede.informatik.uni-bremen.de [134.102.207.29] id OAA13699 for ; Fri, 15 Nov 1996 14:15:33 +0100 (MET) Received: by ganymede.Informatik.Uni-Bremen.DE (SMI-8.6/SMI-SVR4) id OAA06217; Fri, 15 Nov 1996 14:15:11 +0100 From: Burkhart Wolff Date: Fri, 15 Nov 1996 14:15:11 +0100 Message-Id: <199611151315.OAA06217@ganymede.Informatik.Uni-Bremen.DE> To: isabelle-users@cl.cam.ac.uk Subject: Again: Question X-Sun-Charset: US-ASCII Sender: Larry Paulson Content-Type: text Content-Length: 680 Status: RO Sorry for my stupid formulation of my question yesterday, still the problem I was tackling is the same: Assume a theory: >>> New = List + Sum <<< And try: read_ctyp (sign_of List.thy) "['a :: plus, 'a] => 'a"; val it = "['a, 'a] => 'a" : ctyp read_ctyp (sign_of New.thy) "['a :: plus, 'a] => 'a"; Syntax error at: "plus , 'a ] => 'a" Expected tokens: "id", "{}", "{" The error(s) above occurred in type "['a :: plus, 'a] => 'a" (I carefully counted the brackets this time !) There is a declaration of a *constant* "plus" in Sum, but should this matter? bu -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Tue Nov 19 09:31 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA15182; Tue, 19 Nov 1996 09:31:04 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id UAA07636; Mon, 18 Nov 1996 20:18:24 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id UAA20361; Mon, 18 Nov 1996 20:18:20 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id UAA31892; Mon, 18 Nov 1996 20:18:21 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id UAA00191; Mon, 18 Nov 1996 20:18:53 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id UAA10150; Mon, 18 Nov 1996 20:20:54 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vPPwU-0006YL-00; Mon, 18 Nov 1996 09:24:38 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vPPwT-0004Dc-00; Mon, 18 Nov 1996 09:24:37 +0000 Received: from tuminfo2.informatik.tu-muenchen.de [131.159.0.81] (root) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #2) id E0vPNs9-0007HH-00; Mon, 18 Nov 1996 07:12:01 +0000 Received: from sunbroy49.informatik.tu-muenchen.de ([131.159.1.34]) by tuminfo2.informatik.tu-muenchen.de with ESMTP id <52951-242>; Mon, 18 Nov 1996 08:11:54 +0100 Received: from sunbroy29.informatik.tu-muenchen.de by sunbroy49.informatik.tu-muenchen.de id <173704-219>; Mon, 18 Nov 1996 08:11:45 +0100 From: Tobias.Nipkow@informatik.tu-muenchen.de To: bu@Informatik.Uni-Bremen.DE CC: isabelle-users@cl.cam.ac.uk In-reply-to: <199611151315.OAA06217@ganymede.Informatik.Uni-Bremen.DE> (message from Burkhart Wolff on Fri, 15 Nov 1996 14:15:11 +0100) Subject: Re: Again: Question Message-Id: <96Nov18.081145+0100met_dst.173704-219+19@sunbroy49.informatik.tu-muenchen.de> Date: Mon, 18 Nov 1996 08:11:36 +0100 Sender: Larry Paulson Content-Type: text Content-Length: 706 Status: RO bu wrote: > read_ctyp (sign_of New.thy) "['a :: plus, 'a] => 'a"; > Syntax error at: "plus , 'a ] => 'a" > Expected tokens: "id", "{}", "{" > The error(s) above occurred in type "['a :: plus, 'a] => 'a" > > There is a declaration of a *constant* "plus" in Sum, but should this matter? Unfortunately, it does matter: "plus" in Sum is an *infix* constant, and this means that the syntax is modified and "plus" becomes a reserved lexical token. This means that only the following occurrences of "plus" are now legal: plus op plus Sorry, this is the way infixes are treated. Tobias -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Tue Nov 19 09:31 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA15187; Tue, 19 Nov 1996 09:31:09 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id UAA16966; Mon, 18 Nov 1996 20:21:50 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.7.5/sendmail.ITD.EDB+userdb.960305) with ESMTP id UAA20393; Mon, 18 Nov 1996 20:21:46 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id UAA08839; Mon, 18 Nov 1996 20:21:47 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id UAA23794; Mon, 18 Nov 1996 20:22:20 +1030 (CST) Received: from heaton.cl.cam.ac.uk (heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id UAA10250; Mon, 18 Nov 1996 20:24:02 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vPPwo-0006BP-00; Mon, 18 Nov 1996 09:24:58 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vPPwm-0004EC-00; Mon, 18 Nov 1996 09:24:56 +0000 Received: from tuminfo2.informatik.tu-muenchen.de [131.159.0.81] (root) by heaton.cl.cam.ac.uk with esmtp (Exim 0.52 #2) id E0vPODV-0007h6-00; Mon, 18 Nov 1996 07:34:05 +0000 Received: from sunbroy49.informatik.tu-muenchen.de ([131.159.1.34]) by tuminfo2.informatik.tu-muenchen.de with ESMTP id <52938-241>; Mon, 18 Nov 1996 08:33:54 +0100 Received: from localhost by sunbroy49.informatik.tu-muenchen.de with SMTP id <173704-219>; Mon, 18 Nov 1996 08:33:50 +0100 Date: Mon, 18 Nov 1996 08:33:47 +0100 (MET) From: Markus Wenzel To: Burkhart Wolff cc: isabelle-users@cl.cam.ac.uk Subject: Re: Again: Question In-Reply-To: <199611151315.OAA06217@ganymede.Informatik.Uni-Bremen.DE> Message-ID: MIME-Version: 1.0 Sender: Larry Paulson Content-Type: TEXT/PLAIN; charset=US-ASCII Content-Length: 822 Status: RO > read_ctyp (sign_of New.thy) "['a :: plus, 'a] => 'a"; > Syntax error at: "plus , 'a ] => 'a" > Expected tokens: "id", "{}", "{" > The error(s) above occurred in type "['a :: plus, 'a] => 'a" > > > (I carefully counted the brackets this time !) > > There is a declaration of a *constant* "plus" in Sum, but should this matter? Constants per se do not interfere with type classes (and types), but 'plus' is an infix in Sum.thy. Thus a *literal* token hides an *identifier* token. The output of Syntax.test_read illustrates this: > Syntax.test_read (syn_of New.thy) "logic" "['a :: plus, 'a] => 'a"; tokens: "[" tid('a) "::" "plus" "," tid('a) "]" "=>" tid('a) ^^^^^^ Markus -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Wed Nov 20 08:45 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id IAA02541; Wed, 20 Nov 1996 08:44:49 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id UAA30927; Tue, 19 Nov 1996 20:49:31 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/8.7.3/sendmail.ITD.ALC+userdb.961118) with ESMTP id UAA04014; Tue, 19 Nov 1996 20:49:26 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id UAA24799; Tue, 19 Nov 1996 20:49:27 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id UAA09895; Tue, 19 Nov 1996 20:49:59 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id UAA24995; Tue, 19 Nov 1996 20:52:07 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vPmNS-0005lD-00; Tue, 19 Nov 1996 09:21:58 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vPmNQ-0006SW-00; Tue, 19 Nov 1996 09:21:56 +0000 Received: from ormail.intel.com [134.134.248.3] by bescot.cl.cam.ac.uk with smtp (Exim 0.52 #2) id E0vPchp-0003bY-00; Mon, 18 Nov 1996 23:03:25 +0000 Received: from ichips.intel.com (ichips.intel.com [134.134.50.200]) by ormail.intel.com (8.8.3/8.7.3) with ESMTP id OAA28899; Mon, 18 Nov 1996 14:51:37 -0800 (PST) Received: from ichips.intel.com by ichips.intel.com (8.7.4/jIII) id OAA28184; Mon, 18 Nov 1996 14:50:39 -0800 (PST) Message-Id: <199611182250.OAA28184@ichips.intel.com> To: coq-club@pauillac.inria.fr, info-hol@leopard.cs.byu.edu, isabelle-users@cl.cam.ac.uk, nuprlnotes@CS.Cornell.EDU, imps@linus.mitre.org, pvs@csl.sri.com, lambda-usergroup@dcs.ed.ac.uk, nqthm-users@cli.com, qed@mcs.anl.gov Subject: formal verification position at Intel Date: Mon, 18 Nov 1996 14:51:31 -0800 From: Mark Aagaard Sender: Larry Paulson Content-Type: text Content-Length: 3474 Status: RO ------------------------------ Job Opportunities Strategic CAD Technology Intel, Oregon, USA ------------------------------ Strategic CAD Technology (SCT) is a technology development team in Design Technology, Intel's internal CAD organization. SCT's mission is to provide Intel with a competitive advantage in strategic areas of CAD technology. Our focus is on performing research and building technology to meet the CAD needs of future Intel microprocessors. We interact with processor-design teams and academia to create leading-edge solutions for today's and tomorrow's CAD challenges. We predict the future needs of processor-design teams and the co-develop products with the CAD productization teams. SCT has undergone steady growth since its inception in early 1995. We are now one of the top CAD research teams in the world. Almost all of the permanent lab members have significant experience in industrial research or microprocessor design. In addition to day-to-day research, we publish papers, write books, file patents, and teach in universities. Current areas of research include: High-performance circuit design Physical design High-speed synthesis Formal hardware verification Dynamic validation We are located in Hillsboro, Oregon, a suburb of Portland in the scenic Tualatin Valley about sixty miles east of the beautiful Oregon coast. Fishing, hiking, mountain biking, wind-surfing, sailing, and skiing are all in close proximity to Hillsboro. For the second year in a row, Oregon Business Magazine has named Intel the best company to work for in Oregon. ----------------------------------------------------------------------- In formal verification, we are looking for CAD researchers with a strong background digital hardware and computer architecture with a focus in one or more of the following areas: o model-checking o symbolic-simulation o hardware description languages o theorem-proving o algebraic rewriting At the present time we have opportunities in these areas for permanent positions, student interns and co-ops, and visiting faculty. ----------------------------------------------------------------------- Intel offers excellent salaries and benefits that include employee profit sharing and stock ownership plans, tuition reimbursement and periodic paid sabbaticals. Intel is an equal opportunity employer and fully supports affirmative action practices. Intel also supports a drug-free workplace and requires that all offers of employment be contingent on satisfactory pre-employment drug test results. Interested candidates should send their CV, (preferably in both plain ASCII text and Postscript), to either: Carl Seger or Mark Aagaard cseger@ichips.intel.com maagaard@ichips.intel.com by post: Carl Seger Intel Corporation JFT-102 2111 NE 25th Ave Hillsboro OR 97124-5961 FAX: 503-264-9359 Possibly relevant URLs: Intel

Hillsboro

Beaverton

Oregon

Oregon Business Magazine

-------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From dvh@grace.rug.ac.be Wed Dec 4 09:01 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA15975 for ; Wed, 4 Dec 1996 09:01:24 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id TAA18047 for ; Tue, 3 Dec 1996 19:25:20 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id TAA22328 for ; Tue, 3 Dec 1996 19:25:18 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id TAA18952 for ; Tue, 3 Dec 1996 19:25:18 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id TAA11121 for ; Tue, 3 Dec 1996 19:25:52 +1030 (CST) Received: from mserv.rug.ac.be (mserv.rug.ac.be [157.193.40.37]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id TAA19382 for ; Tue, 3 Dec 1996 19:27:42 +1030 (CST) Received: from grace.rug.ac.be by mserv.rug.ac.be with SMTP id AA01772 (5.67b/IDA-1.5 for ); Tue, 3 Dec 1996 09:54:32 +0100 Received: by grace.rug.ac.be id AA10004 (5.67b/IDA-1.5 for Jeremy.Dawson@dsto.defence.GOV.AU); Tue, 3 Dec 1996 09:55:48 GMT Date: Tue, 3 Dec 1996 09:55:48 GMT From: Dirk Van Heule Message-Id: <199612030955.AA10004@grace.rug.ac.be> To: Jeremy.Dawson@dsto.defence.gov.au Subject: 3-valued logic & Isabelle Cc: dvh@grace.rug.ac.be Content-Type: text Content-Length: 1656 Status: RO Hallo Jeremy, some time ago ( I have to apologize, it is now nearly 9 months ago ), you asked me some more information on the research I was doing. Well, here it comes: - we try to implement a 3-valude logic, called PPC, as a object-logic for Isabelle - up to now, I could implement the propositional part of PPC and I started working on the classical reasoner - PPC ( the Partial Predicate Calculus ) is a 3-valued logic, based on the Kleene connectives (AND and NOT), the universal quantifier FORALL and a not-monotone operator DELTA to express that a formula is defined. - the 3 truth values are True, False and Undefined - PPC varies from LCF (Barringer, Chang and Jones) by its definition of VALIDITY 1) M is a model for a formula A if the validitation of A is TRUE 2) A is the consequence of a set of formulas S, ( S |= A ) if A is VALID which means that the validation of A is NOT FALSE ( so A can be true or undefined ) - the calculus used in PPC is based on the assumption calculus of HERMES, it is a mixture of sequent style and natural deduction style and the proofs are always done if forward style So I had to tune all the rule to natural deduction style in order to use Isabelle. Iff you need more information, please contact me. Can you also give me some information on the research you are doing ? Cheers, Dirk ===================================================== Dirk Van Heule Computer Algebra Gent email: dvh@cage.rug.ac.be Galglaan 2 tel : 32-(0)9-264.49.12 9000 Gent fax : 32-(0)9-264.49.93 BELGIUM From Jeremy.Dawson@dsto.defence.gov.au Wed Dec 4 13:52 EST 1996 Received: (from jeremy@localhost) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) id NAA22387; Wed, 4 Dec 1996 13:51:58 +1100 (EST) Date: Wed, 4 Dec 1996 13:51:58 +1100 (EST) From: Jeremy Dawson Message-Id: <199612040251.NAA22387@drambuie.remote.dsto.gov.au> To: dvh@grace.rug.ac.be Subject: Re: 3-valued logic & Isabelle Content-Type: text Content-Length: 729 Status: RO Dirk, Thanks for your email - it looks interesting. The research I was doing consisted, first, of implementing LPF (though I later discovered that Jacob Frost has done a good deal more in that direction); and secondly, of exploring the properties of the rep(_,_) operator, where rep(P,Q) means that if P is defined, then P = Q. Many operators, eg, |, &, -->, have a rep-preserving property, so, eg, rep(P1,P2) implies rep (P1&Q|R-->S, P2&Q|R-->S); this means that you can do automatic rewriting without checking definedness, eg a rewriting tactic can give you rep ((a/a)*b+c, 1*b+c) without any definedness checking along the way. But I won't be doing much more research - my job is to be abolished. regards, Jeremy Dawson From pal@cs.uq.edu.au Mon Dec 9 11:47 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id LAA19307 for ; Mon, 9 Dec 1996 11:47:21 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id LAA01904 for ; Mon, 9 Dec 1996 11:17:19 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id LAA09545 for ; Mon, 9 Dec 1996 11:17:16 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id LAA16401 for ; Mon, 9 Dec 1996 11:17:17 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id LAA19734 for ; Mon, 9 Dec 1996 11:17:51 +1030 (CST) Received: from wasabi.cs.uq.edu.au (wasabi.cs.uq.edu.au [130.102.192.56]) by digger1.defence.gov.au (8.7.5/8.7.3) with ESMTP id LAA28101 for ; Mon, 9 Dec 1996 11:19:38 +1030 (CST) Received: from everest.cs.uq.edu.au (pal@everest.cs.uq.edu.au [130.102.16.6]) by wasabi.cs.uq.edu.au (8.8.4/8.8.4) with ESMTP id KAA15278 for ; Mon, 9 Dec 1996 10:46:45 +1000 (EST) Received: (from pal@localhost) by everest.cs.uq.edu.au (8.8.4/8.8.4) id KAA05215; Mon, 9 Dec 1996 10:46:43 +1000 (EST) Date: Mon, 9 Dec 1996 10:46:43 +1000 (EST) Message-Id: <199612090046.KAA05215@everest.cs.uq.edu.au> From: Peter Lindsay To: Jeremy.Dawson@dsto.defence.gov.au In-reply-to: <199612090027.LAA18920@drambuie.remote.dsto.gov.au> (message from Jeremy Dawson on Mon, 9 Dec 1996 11:27:36 +1100 (EST)) Subject: Re: replacement rules in LPF Content-Type: text Content-Length: 1122 Status: RO Hi Jeremy, sorry to hear the Evaluation Technology cell is winding up, and that you weren't getting very good support from management. BB's reaction sounds very strange. Hope you find something better soon. WRT your LPF proposal & CBJ: it seems Cliff has been going through a large change himself, & is not such a good correspondent just at the moment. (I don't know if you heard but a little while back he announced his sudden departure from academia to return to industry. To compound everyone's surprise, the company he will work for - Harlequin - seem to have little or now formal methods experience, & Cliff himself says he is more interested in OO these days.) So it's perhaps little wonder you haven't heard back from him. As I said before, I think your ideas are very interesting & the VDM community in particular would be interested to hear them. Appropriate places to submit such a paper would include Formal Aspects of Computing (Ian Hayes here is an editor) or Science of Computer Programming. If you like, send me a draft when you have one ready & I'll try to give you some feedback on it. cheers peter From isabelle-internal-request@cl.cam.ac.uk Thu Dec 12 09:18 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA01189; Thu, 12 Dec 1996 09:18:10 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id BAA24288; Thu, 12 Dec 1996 01:09:06 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id BAA21235; Thu, 12 Dec 1996 01:09:03 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id BAA14636; Thu, 12 Dec 1996 01:09:03 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id BAA07074; Thu, 12 Dec 1996 01:09:36 +1030 (CST) Received: from heaton.cl.cam.ac.uk (heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id BAA17973; Thu, 12 Dec 1996 01:11:17 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vXpGL-0005tH-00; Wed, 11 Dec 1996 14:03:53 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vXpGJ-000123-00; Wed, 11 Dec 1996 14:03:51 +0000 Received: from cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with esmtp (Exim 1.59 #2) id 0vXouI-0005lS-00; Wed, 11 Dec 1996 13:41:06 +0000 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 To: pvs@csl.sri.com, info-hol@leopard.cs.byu.edu, isabelle-users@cl.cam.ac.uk Subject: papers available X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Wed, 11 Dec 1996 13:40:57 +0100 From: Lawrence C Paulson Message-Id: Sender: Larry Paulson Content-Type: text Content-Length: 2283 Status: RO Two papers are available via WWW (abstracts below). The first is an introduction to Isabelle based upon my 1996 Marktoberdorf Summer School lectures. The second is on verifying security protocols and assumes a basic knowledge of that problem domain. -- Larry Paulson Title:Tool Support for Logics of Programs http://www/ftp/papers/reports/TR406-lcp-Tool-Support-for-Logics-of-Programs.ps. gz Proof tools must be well designed if they are to be more effective than pen and paper. Isabelle supports a range of formalisms, two of which are described (higher-order logic and set theory). Isabelle's representation of logic is influenced by logic programming: its ``logical variables'' can be used to implement step-wise refinement. Its automatic proof procedures are based on search primitives that are directly available to users. While emphasizing basic concepts, the article also discusses applications such as an approach to the analysis of security protocols. Title:Proving Properties of Security Protocols by Induction http://www/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocol s-by-Induction.dvi.gz Security protocols are formally specified in terms of traces, which may involve many interleaved protocol runs. Traces are defined inductively. Protocol descriptions model accidental key losses as well as attacks. The model spy can send spoof messages made up of components decrypted from previous traffic. Correctness properties are verified using the proof tool Isabelle/HOL. Several symmetric-key protocols have been studied, including Needham-Schroeder, Yahalom and Otway-Rees. A new attack has been discovered in a variant of Otway-Rees (already broken by Mao and Boyd). Assertions concerning secrecy and authenticity have been proved. The approach rests on a common theory of messages, with three operators. The operator "parts" denotes the components of a set of messages. The operator "analz" denotes those parts that can be decrypted with known keys. The operator "synth" denotes those messages that can be expressed in terms of given components. The three operators enjoy many algebraic laws that are invaluable in proofs. -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Thu Dec 12 09:17 EST 1996 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA01170; Thu, 12 Dec 1996 09:17:43 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id DAA20328; Thu, 12 Dec 1996 03:53:30 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id DAA22385; Thu, 12 Dec 1996 03:53:27 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id DAA31268; Thu, 12 Dec 1996 03:53:27 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id DAA05603; Thu, 12 Dec 1996 03:54:00 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id DAA14451; Thu, 12 Dec 1996 03:55:42 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vXrdJ-0007C2-00; Wed, 11 Dec 1996 16:35:45 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vXrdH-0001U5-00; Wed, 11 Dec 1996 16:35:44 +0000 Received: from cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with esmtp (Exim 1.59 #2) id 0vXrc4-0006t5-00; Wed, 11 Dec 1996 16:34:28 +0000 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 To: pvs@csl.sri.com, info-hol@leopard.cs.byu.edu, isabelle-users@cl.cam.ac.uk Subject: papers available (correction) X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Wed, 11 Dec 1996 16:34:22 +0100 From: Lawrence C Paulson Message-Id: Sender: Larry Paulson Content-Type: text Content-Length: 495 Status: RO Unfortunately, my previous message quoted URLs that work only within Cambridge. The following ones ought to work from outside: http://www.cl.cam.ac.uk/ftp/papers/reports/TR406-lcp-Tool-Support-for-Logics-of-Programs.ps.gz http://www.cl.cam.ac.uk/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz Sorry for any inconvenience. -- Larry Paulson -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Tue Jan 21 06:02 EST 1997 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id GAA22728; Tue, 21 Jan 1997 06:02:41 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id EAA16180; Tue, 21 Jan 1997 04:37:56 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id EAA13032; Tue, 21 Jan 1997 04:37:54 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id EAA17724; Tue, 21 Jan 1997 04:37:54 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id EAA15777; Tue, 21 Jan 1997 04:38:27 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id EAA25431; Tue, 21 Jan 1997 04:39:39 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vmNZb-0000Xd-00; Mon, 20 Jan 1997 17:31:55 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vmNZa-0003uJ-00; Mon, 20 Jan 1997 17:31:54 +0000 Received: from utrhcs.cs.utwente.nl [130.89.10.247] by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vmJTi-0006KZ-00; Mon, 20 Jan 1997 13:09:34 +0000 Received: from athena.cs.utwente.nl by utrhcs.cs.utwente.nl (SMI-8.6/csrelay-SVR4_1.3/RBCS) id OAA22452; Mon, 20 Jan 1997 14:09:32 +0100 Received: from campsite.cs.utwente.nl by athena.cs.utwente.nl (SMI-8.6/csrelay-Sol1.4/RB) id OAA06806; Mon, 20 Jan 1997 14:09:29 +0100 Received: from localhost by campsite.cs.utwente.nl (SMI-8.6/SMI-SVR4) id OAA21876; Mon, 20 Jan 1997 14:09:30 +0100 Message-Id: <199701201309.OAA21876@campsite.cs.utwente.nl> To: isabelle-users@cl.cam.ac.uk Subject: Strange behavior of Auto_tac() Mime-Version: 1.0 Date: Mon, 20 Jan 1997 14:09:29 +0100 From: David Spelt Sender: Larry Paulson Content-Type: text/plain; charset="us-ascii" Content-Length: 1867 Status: RO Dear Isabelle users, Recently, I discovered some apparently strange behavior of Auto_tac() from the HOL theory. Consider the following trivial (?) example goal goal List.thy "? x. s1 = snd x & (x = (y, s1))"; Trying Auto_tac() to the above goal fails, whereas the same tactic succeeds(!) on the more or less equivalent goal goal List.thy "? x. (x = (y, s1)) & s1 = snd x"; Failure of the tactic on the first goal seems to originate due to a pecularity in the implementation of the classical tactics, both fast_tac and best_tac, which I don't understand. The tactics repeatedly attack one of the subgoals from the proof state until it either solves or fails. If it solves, the next goal from the list will be selected, but a failure at once causes the entire proof to fail, whereas one would expect it to select one of next goals from the list, thus allowing pending variables to be instantiated causing the goal to be solved during a later stage of the proof. My question is if there were any good reasons to use fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); instead of fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (FIRSTGOAL(step_tac cs))); which when interleaved with the simplifier would have solved both of the above example goals at once Thanks in advance, David Spelt ============================================================================= Centre for Telematics and Information Technology University of Twente Email: spelt@cs.utwente.nl PO Box 217 tel: +31-(0)53-4894625 7500 AE Enschede fax: +31-(0)53-4892927 The Netherlands ============================================================================= -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Tue Jan 21 06:02 EST 1997 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id GAA22731; Tue, 21 Jan 1997 06:02:49 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id EAA17683; Tue, 21 Jan 1997 04:24:11 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id EAA12977; Tue, 21 Jan 1997 04:24:09 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id EAA16784; Tue, 21 Jan 1997 04:24:08 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id EAA26436; Tue, 21 Jan 1997 04:24:42 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id EAA24941; Tue, 21 Jan 1997 04:24:53 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vmNgI-0001pD-00; Mon, 20 Jan 1997 17:38:50 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vmNgH-0003wX-00; Mon, 20 Jan 1997 17:38:49 +0000 Received: from cl.cam.ac.uk [128.232.0.96] (lcp) by heaton.cl.cam.ac.uk with esmtp (Exim 1.59 #2) id 0vmNdk-0002E2-00; Mon, 20 Jan 1997 17:36:12 +0000 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 To: isabelle-users@cl.cam.ac.uk Subject: auto_tac X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Mon, 20 Jan 1997 17:35:56 +0100 From: Lawrence C Paulson Message-Id: Sender: Larry Paulson Content-Type: text Content-Length: 539 Status: RO David Spelt's suggestion might work in some cases; users could experiment with it. But I worry that it would greatly increase the search space and therefore execution time. As a general rule, it is best to avoid using fst and snd, and the analogous functions on lists, etc. Both HOL and ZF allow patterns to appear in all variable-binding positions. The pattern-matching style usually leads to simpler proofs. -- Larry -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Fri Jan 24 09:35 EST 1997 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA29943; Fri, 24 Jan 1997 09:34:51 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id DAA26176; Fri, 24 Jan 1997 03:26:57 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id DAA07804; Fri, 24 Jan 1997 03:26:54 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id DAA32253; Fri, 24 Jan 1997 03:26:54 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id DAA03757; Fri, 24 Jan 1997 03:27:28 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id DAA15591; Fri, 24 Jan 1997 03:28:46 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vnRvL-000221-00; Thu, 23 Jan 1997 16:22:47 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vnRvI-0004r6-00; Thu, 23 Jan 1997 16:22:46 +0000 Received: from tuminfo2.informatik.tu-muenchen.de [131.159.0.81] (root) by heaton.cl.cam.ac.uk with esmtp (Exim 1.59 #2) id 0vnPDX-0007JR-00; Thu, 23 Jan 1997 13:29:23 +0000 Received: from sunbroy49.informatik.tu-muenchen.de ([131.159.1.34]) by tuminfo2.informatik.tu-muenchen.de with ESMTP id <52921-243>; Thu, 23 Jan 1997 14:29:15 +0100 Received: from sunbroy29.informatik.tu-muenchen.de by sunbroy49.informatik.tu-muenchen.de id <173739-215>; Thu, 23 Jan 1997 14:29:03 +0100 From: Tobias.Nipkow@informatik.tu-muenchen.de To: isabelle-users@cl.cam.ac.uk Subject: Isa94-7 Message-Id: <97Jan23.142903+0100met_dst.173739-215+769@sunbroy49.informatik.tu-muenchen.de> Date: Thu, 23 Jan 1997 14:28:58 +0100 Sender: Larry Paulson Content-Type: text Content-Length: 939 Status: RO bu wrote: 1) A lot of theorem names (like hd_Cons, tl_Cons, ...) had been erased from the primrec defs in theory List. Why ? Since this had not been done everywhere, this seems to have happened inadvertently. I can answer this one: in the new version of primrec you may omit the names of all the individual clauses. The point is that primrec clauses are added to the simpset automatically and in 99% of all cases you never want to see them in proofs, because the simplifier does the right thing automatically. The cases where the names are still there are exactly those definitions where you need to refer to some clause explicitly in a proof. Just as an advertisement: the next version of Isabelle will (at last!) also allow primrec for type nat. (Courtesy of Conny Pusch, based on an idea of Norbert Voelker) Tobias -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief From isabelle-internal-request@cl.cam.ac.uk Fri Jan 24 09:36 EST 1997 Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by drambuie.remote.dsto.gov.au (8.7.5/8.7.3) with ESMTP id JAA29953; Fri, 24 Jan 1997 09:36:01 +1100 (EST) Received: from itd3.dsto.defence.gov.au (itd3.dsto.defence.gov.au [131.185.4.3]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id VAA27849; Thu, 23 Jan 1997 21:43:40 +1030 (CST) Received: from fang.dsto.defence.gov.au (fang.dsto.defence.gov.au [131.185.2.5]) by itd3.dsto.defence.gov.au (8.8.3/sendmail.ITD.EDB+userdb.960305) with ESMTP id VAA06725; Thu, 23 Jan 1997 21:43:36 +1030 (CST) Received: from ns.defence.gov.au (ns.defence.gov.au [203.5.216.130]) by fang.dsto.defence.gov.au (8.7.6/8.7.6) with ESMTP id VAA28737; Thu, 23 Jan 1997 21:43:37 +1030 (CST) Received: from digger1.defence.gov.au (digger1.defence.gov.au [203.5.217.4]) by ns.defence.gov.au (8.7.5/8.7.5) with ESMTP id VAA19687; Thu, 23 Jan 1997 21:44:12 +1030 (CST) Received: from heaton.cl.cam.ac.uk (exim@heaton.cl.cam.ac.uk [128.232.32.11]) by digger1.defence.gov.au (8.7.5/8.7.3) with SMTP id VAA06142; Thu, 23 Jan 1997 21:45:15 +1030 (CST) Received: from albatross.cl.cam.ac.uk [128.232.0.96] (exim) by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vnMl1-000539-00; Thu, 23 Jan 1997 10:51:47 +0000 Received: from lcp by albatross.cl.cam.ac.uk with local (Exim 0.55 #1) id E0vnMl0-00041i-00; Thu, 23 Jan 1997 10:51:46 +0000 X-Mailer: exmh version 1.6.9+cl+PEM 96/8/21 Message-Id: From: Larry Paulson To: isabelle-internal@cl.cam.ac.uk Date: Thu, 23 Jan 1997 10:51:46 +0000 Content-Type: text Content-Length: 1893 Status: RO >From bu@informatik.uni-bremen.de Wed Jan 22 13:11:12 1997 Return-path: Delivery-date: Wed, 22 Jan 1997 13:11:12 +0000 Received: from bettina.informatik.uni-bremen.de [134.102.200.16] by heaton.cl.cam.ac.uk with smtp (Exim 1.59 #2) id 0vn2SN-00005K-00; Wed, 22 Jan 1997 13:11:12 +0000 Received: by bettina.informatik.uni-bremen.de (8.8.3/3.10.94m) with SMTP from ganymede.informatik.uni-bremen.de [134.102.204.29] id OAA22985 for ; Wed, 22 Jan 1997 14:11:52 +0100 (MET) From: Burkhart Wolff Received: by ganymede.Informatik.Uni-Bremen.DE (SMI-8.6/SMI-SVR4) id OAA07302; Wed, 22 Jan 1997 14:10:54 +0100 Date: Wed, 22 Jan 1997 14:10:54 +0100 Message-Id: <199701221310.OAA07302@ganymede.Informatik.Uni-Bremen.DE> To: isabelle-users@cl.cam.ac.uk Subject: Isa94-7 X-Sun-Charset: US-ASCII I recently changed to Isabelle94-7 (under sml109). I found two minor problems with the new distribution: 1) A lot of theorem names (like hd_Cons, tl_Cons, ...) had been erased from the primrec defs in theory List. Why ? Since this had not been done everywhere, this seems to have happened inadvertently. 2) Often an additional parameter !!selct. ... is generated out of the blue. It can be eliminated with prune_params_tac by hand, of course, but can this be done automatically by just throwing some new switch? bu [I can answer (2). The tactical SELECT_GOAL sometimes introduces a parameter. Formerly it was called x, but this frequently clashed with users' variables, so I renamed it selct. This new variable name is more likely to be noticed. Moreover, SELECT_GOAL is called more frequently than before, for efficiency reasons. --lcp] -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief