Re: [ProofPower] "Unicode" vs. UTF8

On 07/11/2023 10:09, Makarius wrote: I first heard of "Unicode" approx. 1990. Everybody was talking about "wide charaters" (16bit) and made moves to support them (e.g. major Unix vendors and MicroSoft). That was the time of now obsolete UCS16: "16bit should be sufficient for everyone, i.e.

Re: [ProofPower] Existential Elimination

David, Something odd about your message which confuses my mail tool and doesn't quote it properly, so this is hand cranked (your text in italics) / //What is confusing is the 3 parameters.  e.g. In this partial proof, there is only one premise, but you mention 2? /I'm afraid I'm confused by

Re: [ProofPower] ∃_elim

David, The existential rule most closely analogous to universal instantiation is existential introduction. The ∃_elim rule is more complex, and the name perhaps misleading. The conclusion is always exactly the conclusion of the second premise. The existential "eliminated" is the conclusion of

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

On 04/11/2019 02:01, David Topham wrote: Those two don't seem to get along!  Probably my error and sorry to be burdening you with debugging due to partial understanding on my part. you need ⌜sum (pow r)⌝ and now you are in the reals, / instead of Div, so: ⌜λ n⦁ ∀ r⦁ sum (pow r) n = 1.0 -

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

David, Good to see you are making some progress. For the examples in 9.2 you best course is probably to have a power function with type:     ℝ→ℕ→ℝ ⓈHOLCONST │ pow:ℝ→ℕ→ℝ ├── │ ∀b e⦁ (pow b 0) = 1. ∧ │       (pow b (e + 1)) = b * (pow b e) ■ This will fit with Rob's suggestion for modelling

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

On 02/11/2019 19:10, Rob Arthan wrote: If I need to work with the rationals I just treat them as a subset of the reals. Though I think for these examples even that is an unnecessary complication, since the proof over the reals as a whole will be closest (apart from the actual types) to what a

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

David, Thanks for the reference to the text you are working from, it makes it much clearer what you are trying to do. In example 9.2 I think he should stipulate 0 < r < 1 not just r not= 1. I think strictly speaking if you work with real numbers you are not doing discrete maths, but I don't

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

David The ascii may not be readable, but it can be converted back to ext, or to utf8: ⓈHOLCONST │ sum:ℕ→ℕ ├── │ ∀n⦁ sum 0 = 0 ∧ sum (n) = n + (sum n-1) ■ ⓈHOLCONST │ pow:ℕ→ℕ→ℕ ├── │ ∀b e⦁ (pow b 0) = 1 ∧ (pow b e) = b * (pow b (e - 1)) ■ =SML val ex92 = ⌜λ n r⦁ sum (pow r n) = (1 - (pow r (n

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

David, I missed a pair of brackets in my last. Should be: ⓈHOLCONST │    tri : ℕ → ℕ ├── │    ∀n⦁    tri 0 = 0 │    ∧    tri (n+1) = (tri n)+n+1 ■ ⌜∀n⦁ tri n = (n*(n+1)) Div 2⌝; val tri_p = ⌜λn⦁ tri n = (n*(n+1)) Div 2⌝; ∀_elim tri_p induction_thm; val lemma1 =

Re: [ProofPower] ProofPower and Discrete Math

David, On 28/10/2019 02:39, David Topham wrote: Hello Rob,Roger, et al. Hope you are doing well. I am still trying to apply ProofPower to forward proofs. Glad to hear that. I am working on proof by induction and came across this: induction_thm In the notes, there is an intriguing statement

Re: [ProofPower] ProofPower and Discrete Math

> David, Good to hear you are still moving forward. If the transformation you seek is a propositional tautology, the following general prescription should work. 1. Formulate the transformation as an equivalence using propositional (Boolean) variables, with the starting point on the left of

Re: [ProofPower] Font for SML

David, Looks like one problem for you is the way you are processing the latex files. There is a ProofPower manual, USR001, called:ProofPower - Document Preparation which tells you how to process ProofPower files for printing (or to .dvi

Re: [ProofPower] file conversion

On 18/08/2016 21:15, Rob Arthan wrote: Roger, On 17 Aug 2016, at 11:41, Roger Bishop Jones <r...@rbjones.com> wrote: Rob, It would be helpful for intelligible email discussions about ProofPower if you could tell us all the slickest way to get a proofpower script into a form in which

Re: [ProofPower] ProofPower and Discrete Math

David, There is a reason why the ProofPower tutorials don't say much about the forward proof tools you are trying to use. I have given courses on ProofPower HOL and on ProofPower Z and wrote the tutorials. What I did in the courses was to teach just enough about forward proof for the students

Re: [ProofPower] ProofPower and Discrete Math

On 14/08/2016 08:44, David Topham wrote: Thanks Roger, I am using slides he distributes. He has false introduction rules starting on page 24 (attached). Sorry about my poor example, please ignore that since is a confused use of this technique anyway! -Dave Looks like he changed the name.

Re: [ProofPower] ProofPower on Ubuntu 16.04

f you build poly yourself, rather than install the package you might not need to do (2), but the patch does not harm. Regards, Rob. On 21 Jul 2016, at 11:15, Rob Arthan <r...@lemma-one.com> wrote: Roger, On 18 Jul 2016, at 22:15, Roger Bishop Jones <r...@rbjones.com> wrote: I

[ProofPower] Installing ProofPower on OS X El Capitain

Here is my reconstruction of the method I used to get ProofPower running on OS X 10.11.4, which is an adaptation of a recipe posted by Rob for an earlier version of OS X. From the App Store install Xcode. The rest of the process is done on the command line, so you either need to use terminal

Re: [ProofPower] ProofPower build on OS X

Magic. Build complete. I just had to change the path. xpp seems to come up ok. Thanks, I’ll post a resume. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

Rob, Now failing to find mkfontdir. PATH=/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/Emacs.app/Contents/MacOS/bin-x86_64-10_9:/Applications/Emacs.app/Contents/MacOS/libexec-x86_64-10_9 Am I missing something from the PATH or do I need to install something else?

Re: [ProofPower] ProofPower build on OS X

Rob, Thanks for you continuing support. > On 30 Apr 2016, at 10:16, Rob Arthan wrote: > > ... > Try it in in src/dev. I think it will fail. If so, try it without the > obsolete options: > > polyc -o pp-ml pp-ml.o > Here are the results: bash-3.2$ polyc

[ProofPower] ProofPower build on OS X

Rob, OK, so now I am through to the ProofPower build, which fails pretty fast, just after compiling dtd108. Here’s the tail of the log: rm -f hol.polydb Compiling dtd108.sml and imp108.sml { { echo "val system_version : string = \"3.1w7\"; val build_date : Date.date =

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

On 28/09/15 11:05, Lin, Yuhui wrote: > Thank you very much. Your solution works perfectly for me. Just be a little > curious, what dose the following promoted message means when applying the > tactic > > 'Tactics proof introduced the subgoal 2 but did not request it as a > subgoal" > >

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

Further to my last on this topic, I now see that simple_eq_match_conv already does what is needed for the solution of the first approximation to the requirement. If you take a theorem of the form: forall x, y. P(x,y) ==> A(x,y) = B(x,y) and infer: P(x,y) |- A(x,y) = B(x,y)

[ProofPower] Hard copy manuals

From version 3.1w6 most of the ProofPower manuals are available as paperback books from amazon websites. A search on a US or European amazon website for ProofPower Manuals brings them up, or you can use the links provided at the top of the ProofPower documentation page which is created when

Re: [ProofPower] apply conditional rewriting

On 04/06/15 10:30, YuHui Lin wrote: Hi, How can I apply a conditional rewrite rule in proof power. For example, applying the following thm: forall x,y, z | x y dot x - y + z = x + z -y where x y is the condition, to generate the following two subgoals: 1) x y 2) goal [x - y + z

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

On 09/05/13 23:03, Piotr Trojanek wrote: Thank you for your reply. I have groff installed, so this is not the reason. As far as I understand, the build workflow is .doc-.sml-.err. With my experience in SML I can only attach the files with indication of the problem and kindly ask for your

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

Further to my last, this is what I did before building on Ubuntu 12.04 sudo apt-get install texlive-latex-extra texlive-fonts-extra sudo apt-get install libXp-dev libXext-dev \ libXmu-dev libXt-dev \ libxft-dev libjpeg-dev libpng12-dev sudo apt-get install libmotif4

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

On 09/05/13 15:16, Piotr Trojanek wrote: Dear ProofPower experts, I triy to install the latest OpenProofPower under Ubuntu 12.04, but it fails with the (somewhat cryptic) tail of build.log: docsml -f hol.svf imp001 Compiling (code) imp001.sml make[1]: *** [imp001.ldd] Error 1 My setup

Re: [ProofPower] directory path

Sarah, The reason why you had problems after setting the PATH variable to point to the ProofPower binary directory is because you set it to include only that one directory, so xpp was found, but lots of other necessary binaries were no longer in the search path. As recommended by Phil, the

Re: [ProofPower] (no subject)

On 19/02/13 00:55, Phil Clayton wrote: Easy - by doing exactly that before you run xpp, e.g. PATH=/home/sarah/pp/bin:$PATH Put this in /home/sarah/.bash_profile to have this done automatically when you log in. (That's for Fedora, at leats. For other Linux distributions, it may

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, Your file does not show what you were trying to do with LEMMA_T, or what you actually did, so its hard to offer much help. lemma_tac is easier to understand that LEMMA_T, so you could try doing it with lemma_tac first. (you can always collapse it down to an application of LEMMA_T once

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, I should have mentioned that the problem goal you are looking at can be solved by linear arithmetic so you don't need any lemma at all. Linear arithmetic is not covered by the tutorlal but this is one way to prove the goal: a (PC_T1 z_lin_arith asm_prove_tac[]); Roger

[ProofPower] Recursion theorems without constructors

I make quite a lot of use of recursion theorems to enable various kinds of recursive definitions to be proven consistent automatically. The facilities provided in ProofPower are designed to support recursive definitions over recursive datatypes, in which every element of the type is obtained

Re: [ProofPower] Trying to Prove my Zed Specifications

On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote: After fixing the correction you pointed out, I was able to get the existance proofs completed and I removed the precondition proofs for those init operations. You can see this in the attached specification file. You are now using after

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 16 Oct 2012 01:12, Jon Lockhart wrote: I guess I didn't quite understand or comprehend properly the second point you were trying to make. I inserted an existance proof like I had done for the state schemas and I unfortunately get a very interesting goal after the rewrite, as

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Friday 12 Oct 2012 20:35, Jon Lockhart wrote: I got back to the specification today, and moved on to proving the elevator state schema, Elevator_State, and I moved the static component elevator to an axiom, similar to the static components of button. Unfortunately I get a weird sub

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote: I am having a little trouble getting the axioms created, moving the static portions of the Button_State to an axiom from the schema. I can't seem to get the proof to operate properly. Any suggestions? The problem is that the existential

Re: [ProofPower] Trying to Prove my Zed Specifications

On Friday 28 Sep 2012 22:26, Jon Lockhart wrote: I have two questions on that then. First, from a since and style standpoint, if I wanted to make everything neat in the spec I would place the no changing sets in the axiom after the state schema, but for functionality standpoint, if I wanted

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 25 Sep 2012 22:05, Jon Lockhart wrote: I started doing the There Exist proofs, and as you said they seem quite trivial indeed, but I seem to be stuck after the first two lines. So I have the goal, and it has been rewritten, now I am not sure what is the right question to

Re: [ProofPower] Initialisation convention

Phil, On Sunday 23 Sep 2012 21:11, Phil Clayton wrote: By making initialization an operation without a before state, the initialization can be used with schema operators such as composition and pre, e.g. Init ⨟ Op pre Init the latter being another way to write the following:

[ProofPower] Initialisation convention

I see that Potter Sinclair and Till An Introduction to Formal Specification Using Z 1991 use the primed version of the convention, and offer the following rationale (p43): Here we use Vocab' as the variable to suggest that initialisation is like an operation which produces after objects which

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, I had a brief look at the last spec that you posted. I also had a problem unzipping it, but despite a failure message got a decompression by opening the file in emacs. The file decompressed in this way had two issues in it. The first was that it terminated mid paragraph. The second was

Re: [ProofPower] Trying to Prove my Zed Specifications

On Friday 14 Sep 2012 10:36, Phil Clayton wrote: On 14/09/12 10:05, Roger Bishop Jones wrote: I had a brief look at the last spec that you posted. I also had a problem unzipping it, ... This doesn't surprise me because the attachment was byte for byte the same as the previous attachment

Re: [ProofPower] Best platform for ProofPower?

On Thursday 13 Sep 2012 19:37, Phil Clayton wrote: On 12/09/12 21:05, Roger Bishop Jones wrote: So far I'm not having much success on Ubuntu 12.04 (the PolyML build doesn't seem to work for me). What error message do you get? I ask because David Matthews is about to release 5.5 so

Re: [ProofPower] ProofPower Update

Rob, Sorry for the slow response. I have thought quite a bit about this, but these days such cogitations don't always go anywhere useful. On Thursday 30 Aug 2012 21:58, Rob Arthan wrote: On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote: and a number of cases where identifiers which I had

[ProofPower] Best platform for ProofPower?

I'm having bad luck lately getting suitable environments for running ProofPower. My laptop is on Ubuntu 10.4, and that is fine for ProofPower, but is now so out of date that I can't upgrade it, I would have to install a more recent version of Ubuntu from scratch. So I revived an old server

Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 03 Sep 2012 21:03, Jon Lockhart wrote: Most of the tactics return the exact same goal and the comment printed with the goal is that it is alpha-convertible to its goal. The significance of this is simply that the proof step you have just done has not moved you forward. i.e. it says

Re: [ProofPower] Trying to Prove my Zed Specifications

On Saturday 25 Aug 2012 20:47, Jon Lockhart wrote: I did have a question on some of the outputs from the tutorial document. Currently I am on user013C and when I have placed some of the commands into the terminal, via the execute line command, the ProofPower output is not the same as is

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, You are right that Rob is the man to answer your technical problem, but in the meantime I might be able to help you round it. save_and_quit(); is something that I never use. If your system otherwise seems OK then you should go right ahead and work through the tutorial. Why don't I use

Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 13 Aug 2012 03:24, Jon Lockhart wrote: I have already written the specifications in Word using Z Word Tools, and they are already saved in a variety of formats. I have them transferred over to my linux image. What format do they need to be in for me to get to import them into XPP

Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 13 Aug 2012 13:12, Rob Arthan wrote: Jon is using Anthony Hall's Z Word Tools, which actually go quite a long way to bridging this gap. Z Word Tools allows you to prepare a Z specification inside a Word document and project out the Z in a format suitable for processing by other

Re: [ProofPower] ProofPower Update

I have now managed to build my theories on the new ProofPower and MathsEgs. I had to modify 13 source files to get them through. It seems probable that the changes all resulted from the new MathsEgs, and primarily were changes to names. These include the changes to theorems plus = additive

Re: [ProofPower] ProofPower Update

Rob, On Thursday 09 Aug 2012 10:26, Rob Arthan wrote: I plan to make a new ProofPower release shortly. In the meantime, if you want the state of the art, I uploaded an experimental version built from the latest source. You can find this here:

Re: [ProofPower] ProofPower Update

Rob, My theories fail to build on the latest version of maths_egs because I have been using R_plus_ops_thm and R_plus_group_thm which were in wrk068 but are no longer. Looks like you have just changed some names, is that right? Roger Jones ___

Re: [ProofPower] ProofPower RCS Repository

On Sunday 05 Aug 2012 15:36, Rob Arthan wrote: If anyone feels minded to look at this and advise how it could be adapted to work with Mercurial or Git, I would be very grateful. My ideal would be to be able to map between Mercurial or Git and RCS. Any feedback on this would be gratefully

Re: [ProofPower] ProofPower RCS Repository

On Monday 06 Aug 2012 19:40, Rob Arthan wrote: Could you try again with PPMOTIFLINKING=dynamic ? That worked fine. I'm afraid I can't help with mercurial or git, but I am due for a new development regime so I will be following you closely. Roger

[ProofPower] ProofPower on AWS EC2

Thanks to Phil, Rob and Wolfram for help so far. I was completely distracted yesterday by the delivery of a new keyboard (7-octave variety), but seem to have made some progress. Phil's Yum prescription was helpful. The amazon repositories don't have SML, but do contain a satisfactory

Re: [ProofPower] Trouble Installing in cloud

On Thursday 02 Aug 2012 00:33, you wrote: On 01/08/12 14:35, Roger Bishop Jones wrote: The real challenge (for me at least) is to get xpp and/or emacs to run in the cloud with a display here on earth, I don't have much clue how to do that. I've been thinking about this. To me, it seems

[ProofPower] ProofPower in the cloud?

Has anyone tried, or even considered, running ProoPower in the Amazon cloud (AWS they call it Amazon Web Services)? They offer a number of Linux images which might be used as starting points. Presumably one could run ProofPower and xpp in the cloud and access it using an X-client on cygwin on

Re: [ProofPower] Writing Z schema predicates with decorations

On Wednesday 28 Sep 2011 13:52, Phil Clayton wrote: I wondered whether the original design intended to map decoration differently for predicates and expressions? Then the user could determine the mapping of e.g. S' as either mk_z_schema_pred (S, ') mk_z_schema_pred (mk_z_decor%down%s

Re: [ProofPower] Writing Z schema predicates with decorations

On Sunday 25 Sep 2011 16:20, Phil Clayton wrote: Although the Z'SchemaPred semantic constant enables renaming to be avoided, Z'SchemaPred HOL terms are not Z when the schema components are decorated inconsistently. So perhaps renaming is useful? I'm sure it is. But I doubt that it is

Re: [ProofPower] Writing Z schema predicates with decorations

On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote: On Saturday 24 Sep 2011 13:09, Rob Arthan wrote: The quick answer is no - the term generator (imp063.doc) never calls mk_z_schema_pred with non-empty decoration. I need to remind myself exactly what the decoration

Re: [ProofPower] Writing Z schema predicates with decorations

On Saturday 24 Sep 2011 13:09, Rob Arthan wrote: The quick answer is no - the term generator (imp063.doc) never calls mk_z_schema_pred with non-empty decoration. I need to remind myself exactly what the decoration in mk_z_schema_pred is for (I know what the semantics is intended to be but I

Re: [ProofPower] Printing of \not\in

Rob, I just made something like your document to exhibit the problem and I see that it doesn't. In a sample document exhibiting the problem I have: \usepackage{latexsym} \usepackage{rbj} and rbj.sty has in it: \RequirePackage{Proofpower} \RequirePackage{mathabx} However, adding these two

Re: [ProofPower] Printing of \not\in

On Sunday 10 Jul 2011 12:22, Rob Arthan wrote: Roger, I had put this on my list of things to fix by changing \not\in in the style file to \notin, but I get exactly the opposite problem: \not\in work but \notin fails. Are you still having this problem? I am suspecting that you are using a

Re: [ProofPower] Printing of \not\in

Rob, On Sunday 10 Jul 2011 15:59, you wrote: What happens if you just run doctex and then texdvi on this file: http://dl.dropbox.com/u/34693999/ProofPower/rbj-not-in.te x For me it fails on the second GFT section, when the %notmem% character is expanded to \notin rather than \not\in.

Re: [ProofPower] Printing of \not\in

On Tuesday 29 Mar 2011 16:48, Rob Arthan wrote: It works fine for me. What goes wrong? The failing occurrences are either in index brackets or in theory listings (probably also in index brackets). The actual error message is: ! Undefined control sequence. \not #1-\let \@@not

[ProofPower] Error on set_merge_pcs after add_cs_E_thm

Here is a sequence of actions with ProofPower which is causing me puzzlement. :) set_merge_pcs [unalg, 'latt2]; val it = () : unit :) add_%exists%_cd_thms [MkLat_recursion_lemma] 'latt2; val it = () : unit :) set_merge_pcs [unalg, 'latt2]; Exception Fail * Element cannot be found in list

Re: [ProofPower] Cut and Paste problem

On Thursday 08 Jul 2010 11:21, m...@proof-technologies.com wrote: In fact, Roger, could you confirm that you are using OpenMotif 2.3.0? No. 2.2.3-4. I'm on Ubuntu 9.04 so I think I will have to go up to 9.10. Roger ___ Proofpower mailing list

Re: [ProofPower] help

On Monday 09 November 2009 19:48:04 Igorj V wrote: may be some one could explain me such error when installing proofpower?! troff: fatal error: can't find macro file s I had that problem, and the question has been asked and answered. The answer is in the archive here:

Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

On Tuesday 24 March 2009 05:07:09 Artur Oliveira Gomes wrote: I'm having hard times to achieve some proofs of preciondition and initialization using ProofPower. The file attached contains 3 examples that I still can not prove. If anyone could help me out with those proofs, I will be thankful.

Re: [ProofPower] Schemas and Operations

Artur, After my last post I remembered the previous conversation and realised that you were reducing the width of your schemas and then having a problem translating the theta expressions in the original. I've been a bit busier than usual so I didn't get back. In fact I forgot. To use a theta