# Axioms

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

# HOL

• cakeml a verified implementation of an ML in HOL4
• holpy https://arxiv.org/abs/1905.05970

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

# Isabelle

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
`