Axioms

Encoding forall ``\x P(x) = \x true` is saying that the predictae p is always true.

HOL

HOL4 https://kth-step.github.io/itppv-course/

HOL light

https://github.com/jrh13/hol-light/ harrison itp school https://cakeml.org/candle candle hol light on cakeml

botstrap https://github.com/jrh13/hol-light/blob/master/hol.ml

kernel https://github.com/jrh13/hol-light/blob/master/fusion.ml

echo "
;question, can I write re
(declare-const b Bool)
(assert (distinct b b))
(check-sat)" > /tmp/test.smt2
vampire /tmp/test.smt2

#

Isabelle

https://slawekk.wordpress.com/ isar mathlib https://isarmathlib.org/index.html

https://www.cl.cam.ac.uk/teaching/2122/L21/materials.html pauleson course

metis https://www.gilith.com/software/metis/ metitarski. Resolution + Qepcad

FOLP first order logic with proofs. Interesting idea

ZF

typedecl judgement axiomatization

argo smt solver. hmm

HOL nonstadnard reals

https://isabelle.in.tum.de/library/

paulson’s blog slaps https://lawrencecpaulson.github.io/ https://github.com/lawrencecpaulson/lawrencecpaulson.github.io/tree/main/Isabelle-Examples

semantic search https://behemoth.cl.cam.ac.uk/search/ serapis

isabelle isar reference manual is useful

src/HOL directory impp mutablle nominal nonstandard-analysis

from lcf to isabelle sel4 - verified microkernel

Metalevel is a syntax for describing inference rules

  • !! x. \Lambda Universal variables at the meta level. enables Schema
  • ==> is inference rule
  • %x. is meta level lambda?

typeclasses vs locales

Sledgehammer: some history, some tips isabelle cookboook: programming in ML more isabelle ML programming notes

Baby examples

Isabelle => vs –> vs ==> => is the function type –> is implication ==> is meta implication, which is something like a sequent |-

theory play (* same as file name *)
imports Main (* You usually want Main *)
begin
(* https://isabelle.in.tum.de/doc/tutorial.pdf *)

(* defining a datatype *)
datatype 'a  MyList = MyNil | MyCons 'a "'a MyList"
(* What needs quotes "" vs what doesn't I find confusing 
I think it just infers a lot
*)

(*
difference between fun and primrec. fun is basically better.
https://stackoverflow.com/questions/30419419/what-is-the-difference-between-primrec-and-fun-in-isabelle-hol#:~:text=For%20algebraic%20datatypes%20without%20a,which%20can%20be%20rather%20tedious.
*)

primrec myapp :: "'a MyList \<Rightarrow> 'a MyList \<Rightarrow> 'a MyList"
  where
  "myapp MyNil x = x" 
| "myapp (MyCons x xs) ys = MyCons x (myapp xs ys)"

export_code myapp in OCaml module_name Foo
(* But also I already have definitions and notation imported 
from Main*)
value "[True , False]"
value "nil"

value "rev [True, False]"

definition foo :: nat where "foo = 3"


lemma "(1 :: nat) + 2 = 3"
  by simp

type_synonym bar = nat

lemma "union a b = union b a"
  apply (rule Groups.ac_simps)
  done

(* type \<lbrakk> using [ |  *) 
lemma test_theorem : "\<lbrakk>f a = a\<rbrakk> \<Longrightarrow>  f (f a) = a"
  print_state
  apply simp
  print_state
  done

print_commands
print_theory
print_theorems
print_locales

help

(* How do I model a new theory?
Locales I guess
https://lawrencecpaulson.github.io/2022/03/23/Locales.html


typedecl and axiomatization. To be avoided in many cases since it is easy to make an inconsistent tehory
https://isabelle.in.tum.de/library/HOL/HOL/Set.html
Set is axiomatized
*)

lemma "a \<in> (A :: 'a set) \<longrightarrow> a \<in> A \<union> B" 
  apply simp
  done

(*
Note the state panel on the right. 
Also a proof state checkbox in the output panel
*)

fun myadd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   "myadd 0 x = x"
|  "myadd (Suc n) x = Suc (myadd n x)"
(* Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}" *)

find_consts name:myadd
(* 
  play.myadd :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  play.myadd_dom :: "nat \<times> nat \<Rightarrow> bool"
  play.myadd_sumC :: "nat \<times> nat \<Rightarrow> nat"
*)
value "True \<and> False \<or> True \<longrightarrow> False"
(* lemma "\<lambda>x. \<lambda>y. true = \<lambda>x. \<lambda>y. true" *)

find_theorems name:myadd
(*
found 6 theorem(s):
  play.myadd.simps(1): myadd 0 ?x = ?x
  play.myadd.simps(2): myadd (Suc ?n) ?x = Suc (myadd ?n ?x)
  play.myadd.induct:
    (\<And>x. ?P 0 x) \<Longrightarrow>
    (\<And>n x. ?P n x \<Longrightarrow> ?P (Suc n) x) \<Longrightarrow> ?P ?a0.0 ?a1.0
  play.myadd.cases:
    (\<And>x. ?x = (0, x) \<Longrightarrow> ?P) \<Longrightarrow>
    (\<And>n x. ?x = (Suc n, x) \<Longrightarrow> ?P) \<Longrightarrow> ?P
  play.myadd.elims:
    myadd ?x ?xa = ?y \<Longrightarrow>
    (\<And>x. ?x = 0 \<Longrightarrow> ?xa = x \<Longrightarrow> ?y = x \<Longrightarrow> ?P) \<Longrightarrow>
    (\<And>n x. ?x = Suc n \<Longrightarrow>
            ?xa = x \<Longrightarrow> ?y = Suc (myadd n x) \<Longrightarrow> ?P) \<Longrightarrow>
    ?P
  play.myadd.pelims:
    myadd ?x ?xa = ?y \<Longrightarrow>
    myadd_dom (?x, ?xa) \<Longrightarrow>
    (\<And>x. ?x = 0 \<Longrightarrow>
          ?xa = x \<Longrightarrow> ?y = x \<Longrightarrow> myadd_dom (0, x) \<Longrightarrow> ?P) \<Longrightarrow>
    (\<And>n x. ?x = Suc n \<Longrightarrow>
            ?xa = x \<Longrightarrow>
            ?y = Suc (myadd n x) \<Longrightarrow>
            myadd_dom (Suc n, x) \<Longrightarrow> ?P) \<Longrightarrow>
    ?P
*)


(*
https://isabelle.in.tum.de/library/Pure/Pure/Pure.html
Pure doesn't import anything. I followed an import chain
up from Set.
It is unfortunate that the deeper stuff is always magical.
Users do not need the sorts of things in this file
*)

(*
HOL theory
https://isabelle.in.tum.de/library/HOL/HOL/HOL.html

typedecl of bool
judgement command
*)

(*
https://isabelle.in.tum.de/library/HOL/HOL/Orderings.html
*)


(* https://lawrencecpaulson.github.io/2023/03/22/Binomial_Coeffs.html 
*)
value "binomial 3 1" 


end

Querying

theory isabelleplay
  imports Complex_Main
begin
print_commands
(*
find_consts
find_
prf
*)

value "1 + 2::nat"
(*  Comment *)
lemma "a \<Longrightarrow> b"

find_theorems "_ \<longrightarrow> _" 
find_theorems "_ \<and> _ \<longrightarrow> _"
find_theorems name:impI
find_consts name:list
(* lemma is nameless? *)
lemma "p \<and> q \<longrightarrow> p::bool"
  apply (rule impI)
  apply (erule conjunct1)
  done
(* drule erule frule *)
(* cheatsheet https://www.inf.ed.ac.uk/teaching/courses/ar/isabelle/FormalCheatSheet.pdf *)

find_consts "_ \<Rightarrow> _"
(*
Arrows
\<longrightarrow> implication?
\<rightarrow> ?
\<Rightarrow> function
\<Longrightarrow> inference rule? Sequent?
*)

lemma "1 = 2"
  apply (rule eq.sym)
  (* by auto *)
(*
auto 
force
blast
arith
clairfy
clarsimp
*)
lemma "s \<inter> t \<subseteq> s"
by (rule Set.Int_lower1)


theorem foo : "1 + 2 = 3"
  by simp

datatype aexpr = Lit nat | Plus aexpr aexpr
print_theorems (* datatype defines a ton of theorems*)
find_consts aexpr

find_consts 

value "1 + 2::nat"
print_theorems

value "(1::nat) # []"
find_consts name:"Lam [_]._"
find_consts name:sin
find_theorems sin
(* my commented isabelle https://www.lri.fr/~wolff/papers/other/TR_my_commented_isabelle.pdf *)
ML val x = 1 + 2
(*
  declare [[show_types]]
  declare [[show_sorts]]
declare [[show_consts]]
*)
(* ctrl + hover 
https://stackoverflow.com/questions/15489508/how-do-i-view-hidden-type-variables-in-isabelle-proof-goals
I get burned by bad type inference a lot *)
lemma "sin x \<le> (1::real)"
  apply (rule Transcendental.sin_le_one)
  done
find_theorems "(sin _ * sin _)"
find_theorems name:sin_cos_sq


lemma "cos (x::real) * Transcendental.cos x + sin x * sin x = (1::real)"
  by simp (* but the other direction doesn't work *)
 lemma "sin x * sin x + cos (x::real) * cos x  = (1::real)"
   apply   

end

The isabelle command line https://stackoverflow.com/questions/48939929/verify-an-isabelle-proof-from-the-command-line isabelle build isabelle process -T

Isabelle system manual https://isabelle.in.tum.de/doc/system.pdf

ROOT files

Usage: isabelle process [OPTIONS]

  Options are:
    -T THEORY    load theory
    -d DIR       include session directory
    -e ML_EXPR   evaluate ML expression on startup
    -f ML_FILE   evaluate ML file on startup
    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
    -m MODE      add print mode for output
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)

  Run the raw Isabelle ML process in batch mode.

#isabelle process -e "1 + 1" # eval ML expr
#isabelle process -e ’Thy_Info.get_theory "Main"’
#isabelle process -T /home/philip/Documents/philzook58.github.io/_notes/Languages/isabelle/play
cat <<'EOF' > /tmp/test.thy
theory test
imports Main
begin
lemma "1 + 1 = 2" by simp
value "3::int"
(* print_commands *)
(* defining a datatype *)
datatype 'a  MyList = MyNil | MyCons 'a "'a MyList"
(* defining a function *)
fun mylength :: "'a MyList \<Rightarrow> nat" where
  "mylength MyNil = 0"
| "mylength (MyCons x xs) = 1 + mylength xs"
end
EOF
isabelle process -T /tmp/test


isabelle console

https://github.com/isabelle-prover/mirror-isabelle

PURE is the isabelle framework. The core rules are resolution? https://github.com/isabelle-prover/mirror-isabelle/blob/master/src/Pure/thm.ML

(*Resolution: exactly one resolvent must be produced*)
fun tha RSN (i, thb) =
  (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of
    ([th], _) => solve_constraints th
  | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
  | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));

(*Resolution: P \<Longrightarrow> Q, Q \<Longrightarrow> R gives P \<Longrightarrow> R*)
fun tha RS thb = tha RSN (1,thb);

Higher order unfication https://github.com/isabelle-prover/mirror-isabelle/blob/master/src/Pure/unify.ML

simplifier https://github.com/isabelle-prover/mirror-isabelle/blob/master/src/Pure/simplifier.ML https://github.com/isabelle-prover/mirror-isabelle/blob/master/src/Pure/raw_simplifier.ML

Example simple HOL def https://github.com/isabelle-prover/mirror-isabelle/blob/master/src/Pure/Examples/Higher_Order_Logic.thy

https://github.com/isabelle-prover/mirror-isabelle/tree/master/src/Provers provers.