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/

HOL light

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

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