# Axioms

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

# HOL light

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

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://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

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

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

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
(* Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}" *)

(*
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" *)

(*
found 6 theorem(s):
(\<And>x. ?P 0 x) \<Longrightarrow>
(\<And>n x. ?P n x \<Longrightarrow> ?P (Suc n) x) \<Longrightarrow> ?P ?a0.0 ?a1.0
(\<And>x. ?x = (0, x) \<Longrightarrow> ?P) \<Longrightarrow>
(\<And>n x. ?x = (Suc n, x) \<Longrightarrow> ?P) \<Longrightarrow> ?P
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
myadd ?x ?xa = ?y \<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:
-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