/home/bill/web/
#] 
#] *********************
#] "$d_web"'CompLangs/math proof Isabelle/0_Isabelle notes.txt'
# www.BillHowell.ca  29Jan2024 initial 
# view in text editor, using constant-width font (eg courier), tabWidth = 3

#48************************************************48




#24************************24
# Table of Contents, generate with :
# $ grep  "^#]"  "$d_web"'CompLangs/math proof Isabelle/0_Isabelle notes.txt' |  sed "s/^#\]/  /" 
#


#24************************24
# Setup, ToDos,   


#08********08
#] ??Jan2024 


#08********08
#] ??Jan2024 


#08********08
#] ??Jan2024 


#08********08
#] 29Jan2024 search "Isabelle math prover and how do I run it?"


+-----+
https://stackoverflow.com/questions/53766579/isabelle-2017-getting-started
Isabelle 2017 -- getting started
Asked 5 years, 1 month ago
Modified 5 years, 1 month ago
Viewed 1k times
>> not much starter help - the video below isfar more helpful, does a good job

+-----+
https://www.youtube.com/watch?v=1nEpUoVopT0
Isabelle Theorem Prover tutorial
bhari88
30 subscribers
>> great, that helped a LOT!


+-----+
https://isabelle.in.tum.de/dist/Isabelle2023/doc/prog-prove.pdf
Tobias Nipkow
Programming and Proving in
Isabelle/HOL
September 11, 2023

Isabelle is a generic system for implementing logical formalisms, and Isa-
belle/HOL is the specialization of Isabelle for HOL, which abbreviates Higher-
Order Logic. We introduce HOL step by step following the equation
HOL = Functional Programming + Logic.
>> nice, but doesn't tell me how to run it

#08********08
#] 29Jan2024 update my Isabelle? (is it even installed at this time?)
LMDE Software Manager - not in it

https://isabelle.in.tum.de/installation.html
	to: /home/bill/PROJECTS/SW install & maintain/Isabelle
$ cd "$d_web"'CompLangs/'
$ tar -xzf "$d_PROJECTS"'SW install & maintain/Isabelle/Isabelle2023_linux.tar.gz'
>> awesome works well

to launch: click on 'Isabelle2023' settings-like icon
>> starts up nicely 
how do I run it (probably simple comd line?)


#08********08
#] 29Jan2024 seach "Isabelle math proover example"

+-----+
https://isabelle.in.tum.de/
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle overview for a brief introduction.
>> seems HOL used in Isabelle?


+-----+
https://lawrencecpaulson.github.io/2022/05/04/baby-examples.html
Getting started with Isabelle: baby examples, cool proof methods
04 May 2022
Machine Logic is maintained by Lawrence C Paulson.


https://lawrencecpaulson.github.io/tag/Isabelle
Tag: Isabelle
	Coinductive puzzle, by Jasmin Blanchette and Dmitriy Traytel (08 Nov 2023)
	The End (?) of the ALEXANDRIA project (31 Aug 2023)
	Porting the HOL Light metric space library (12 Jul 2023)
	The ALEXANDRIA Project: what has been accomplished? (27 Apr 2023)
		>> cool article, gives me hope, many good examples to copy-paste
		https://link.springer.com/article/10.1365/s13291-020-00221-1
		>> Awesome examples
	Martin-Löf type theory in Isabelle: examples (30 Nov 2022)
	Martin-Löf type theory in Isabelle: formalisation (23 Nov 2022)
	(Hilbert, Isabelle) and more universal pairs, by Marco David (09 Nov 2022)
	Porting libraries of mathematics between proof assistants (14 Sep 2022)
	How Isabelle emerged from the trends of the 1980s (13 Jul 2022)
	Formalising Ramsey theory, II (15 Jun 2022)
	Dealing with descriptions in Isabelle/HOL: least, greatest, whatever (08 Jun 2022)
	Getting started: basic Isabelle/jEdit tricks (11 May 2022)
	Getting started with Isabelle: baby examples, cool proof methods (04 May 2022)
	Type classes versus locales (23 Mar 2022)
	Axiomatic type classes: some history, some examples (02 Mar 2022)
	A classical proof: exponentials are irrational (16 Feb 2022)
	Fun with Ackermann's function (09 Feb 2022)
	ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician (08 Dec 2021)
	Introductory example: Fibonacci numbers (13 Oct 2021)








# enddoc