my forest
bunch more isa
+310
-15
+1
trees/isa/isa-0001.tree
+1
trees/isa/isa-0001.tree
+7
-9
trees/isa/isa-0002.tree
+7
-9
trees/isa/isa-0002.tree
···
6
6
\put\shiki/language{Isabelle Theory}
7
7
8
8
\transclude{isa-0003}
9
-
10
-
\shiki{theory ND
11
-
imports Pure
12
-
begin
13
-
14
-
typedecl bool
15
-
judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5)
16
-
}
17
-
9
+
\transclude{isa-0016}
10
+
\transclude{isa-0017}
11
+
\transclude{isa-0018}
18
12
\transclude{isa-0005}
13
+
\transclude{isa-0019}
14
+
\transclude{isa-001C}
19
15
\transclude{isa-000Z}
20
16
\transclude{isa-0010}
21
17
\transclude{isa-000C}
···
38
34
\transclude{isa-000J}
39
35
\transclude{isa-000K}
40
36
\transclude{isa-000L}
37
+
41
38
\transclude{isa-000N}
39
+
\transclude{isa-001A}
42
40
\transclude{isa-000P}
43
41
\transclude{isa-000O}
44
42
\transclude{isa-000Q}
+1
-1
trees/isa/isa-000M.tree
+1
-1
trees/isa/isa-000M.tree
+4
-4
trees/isa/isa-000N.tree
+4
-4
trees/isa/isa-000N.tree
···
7
7
\put\shiki/language{Isabelle Theory}
8
8
9
9
\shiki{axiomatization
10
-
All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10)
11
-
where
12
-
allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and
13
-
spec : ‹∀ a. P a ⟹ P x›
10
+
All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10)
11
+
where
12
+
allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and
13
+
spec : ‹∀ a. P a ⟹ P x›
14
14
}
+1
-1
trees/isa/isa-000Y.tree
+1
-1
trees/isa/isa-000Y.tree
···
13
13
apply (drule_tac x = a in spec)
14
14
apply (frule_tac x = "M a" in spec)
15
15
apply (drule_tac x = "M (M a)" in spec)
16
-
apply (drule imp_as_disj)+
16
+
apply (drule disjCI)+
17
17
apply (elim disjE)
18
18
apply (rule_tac x = a in exI; intro conjI; assumption)
19
19
apply (rule_tac x = "M a" in exI; intro conjI; assumption)
+12
trees/isa/isa-0016.tree
+12
trees/isa/isa-0016.tree
···
1
+
\date{2025-12-02T05:04:28Z}
2
+
\author{liamoc}
3
+
\parent{isa-0002}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\title{Definining Theories}
7
+
\p{An Isabelle file is called a \em{theory}, and they consist of mathematical definitions (of types and terms), lemmas and proofs. Isabelle theories start with a theory name and a declaration of all the theories on which it depends. The theory name must match the file name, so the code from this lecture should be saved into a file called \code{HOLFromScratch.thy}. }
8
+
\shiki{theory HOLFromScratch
9
+
imports Pure
10
+
begin
11
+
}
12
+
\p{We imported the theory \code{Pure}, which contains only the very basic built-in structures that define Isabelle's logic. }
+18
trees/isa/isa-0017.tree
+18
trees/isa/isa-0017.tree
···
1
+
\date{2025-12-02T05:07:23Z}
2
+
\author{liamoc}
3
+
\parent{isa-0002}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\title{HHFs and Isabelle/Pure}
7
+
\p{Isabelle's logical framework consists of \em{terms} (#{t}), \em{types} (#{\tau}) and \em{formulae} (#{\varphi}). Each term #{t} must have a type #{\tau}, written #{t :: \tau}. }
8
+
\p{In the below code, we define a new type called \code{bool}, and we declare that terms of type \code{bool} can be used as judgments in our formulae. The details of the \code{judgment} command are not important for now.}
9
+
\shiki{typedecl bool
10
+
judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5)
11
+
}
12
+
\p{Formulae in Isabelle are \em{hereditary Harrop formulae}, defined as:}
13
+
##{\begin{array}{lclll}
14
+
\varphi & ::= & \bigwedge x.\ \varphi & & \textit{(meta-forall)} \\
15
+
& \mid & \varphi \implies \varphi & & \textit{(meta-implication)}\\
16
+
& \mid & t & \text{where}\ t\ \text{:: \texttt{bool}} & \textit{(judgments)}
17
+
\end{array}}
18
+
\p{In Isabelle's syntax, formulae, terms, and types are typically surrounded by quote marks \code{""} or cartouches \code{‹›} — the two are equivalent.}
+16
trees/isa/isa-0018.tree
+16
trees/isa/isa-0018.tree
···
1
+
\date{2025-12-02T05:08:28Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\title{Isabelle's Syntax for HHFs}
5
+
\p{Consider the following rule: ##{\dfrac{A \quad B}{A \land B}{\text{\small conjI}}}
6
+
This is encoded as an Isabelle formula as follows:
7
+
##{\bigwedge A. \left(\bigwedge B. (A \implies (B \implies (A \land B)))\right) }
8
+
}
9
+
\p{Because #{\implies} is right-associative, we can remove some parentheses:}
10
+
##{\bigwedge A. \left(\bigwedge B. (A \implies B \implies A \land B)\right) }
11
+
\p{We can also combine the meta-quantifiers:}
12
+
##{\bigwedge A\ B.\;\; A \implies B \implies A \land B }
13
+
\p{Isabelle includes special syntax #{\llbracket A_0; A_1, \dots, A_n \rrbracket \implies C} which is equivalent to #{A_0 \implies A_1 \implies \dots \implies A_n \implies C}.}
14
+
##{\bigwedge A\ B.\;\; \llbracket A; B\rrbracket \implies A \land B }
15
+
\p{Isabelle will also automatically add quantifiers to unknown variables, so we can drop the meta-quantifiers from the outermost part of the formula:}
16
+
##{\llbracket A; B\rrbracket \implies A \land B }
+17
trees/isa/isa-0019.tree
+17
trees/isa/isa-0019.tree
···
1
+
\date{2025-12-02T05:15:07Z}
2
+
\author{liamoc}
3
+
\import{dt-macros}
4
+
\title{Isabelle \code{axiomatization}s}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\p{Isabelle's basic mechanism to define new things is the \code{axiomatization} command.}
8
+
\shiki{axiomatization
9
+
(* constants *)
10
+
where
11
+
(* axioms *)}
12
+
\p{This defines the constants (with their types) in the \code{constants} section, and assumes the formulae stated in the \code{axioms} section. }
13
+
\problemblock{
14
+
\p{
15
+
Isabelle does nothing to stop you from assuming false theorems as axioms in \code{axiomatization} commands, which can easily render the logic unsound. We shall later see safer ways to define new constants, which should be preferred over \code{axiomatization} in most cases.
16
+
}
17
+
}
+9
trees/isa/isa-001A.tree
+9
trees/isa/isa-001A.tree
···
1
+
\date{2025-11-28T05:41:54Z}
2
+
\taxon{Proof Method}
3
+
\title{\code{rule_tac}, \code{erule_tac}, \code{drule_tac}, \code{frule_tac}}
4
+
\author{liamoc}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\p{The typical \code{rule}, \code{erule}, \code{drule}, \code{frule} methods rely entirely on unification to determine how to instantiate the variables in the provided rule. Sometimes, it is useful to state explicitly how to instantiate some variables in the rule, particularly when dealing with quantifiers, or when there are multiple possible candidates.}
8
+
\shiki{apply (rule_tac x = "term" in exI)}
9
+
+34
trees/isa/isa-001B.tree
+34
trees/isa/isa-001B.tree
···
1
+
\date{2025-12-02T05:59:44Z}
2
+
\author{liamoc}
3
+
\taxon{Lecture}
4
+
\title{Definitions, Datatypes, Induction, Functions}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
8
+
\shiki{theory Definitions
9
+
imports Main
10
+
begin
11
+
}
12
+
\p{Unlike in \ref{isa-0002}, we import \code{Main} here rather than \code{Pure}. Almost all theories developed in Isabelle/HOL import \code{Main}, which contains all of the axioms and connectives introduced in \ref{isa-0002}, as well as a host of other theories, including:}
13
+
\ul{
14
+
\li{Axioms for defining \em{equality}. Try the following: \shiki{thm refl
15
+
thm sym
16
+
thm trans
17
+
thm iffI
18
+
thm ssubst}
19
+
}
20
+
\li{A theory of [sets](https://isabelle.in.tum.de/library/HOL/HOL/Set.html).}
21
+
\li{A theory of [natural numbers](https://isabelle.in.tum.de/library/HOL/HOL/Nat.html)}
22
+
\li{A theory of [lists](https://isabelle.in.tum.de/library/HOL/HOL/List.html)}
23
+
\li{And much more!}
24
+
}
25
+
26
+
\transclude{isa-001G}
27
+
\transclude{isa-001D}
28
+
\transclude{isa-001F}
29
+
\transclude{isa-001E}
30
+
\transclude{isa-001H}
31
+
\transclude{isa-001K}
32
+
\transclude{isa-001J}
33
+
\transclude{isa-001L}
34
+
\transclude{isa-001M}
+14
trees/isa/isa-001C.tree
+14
trees/isa/isa-001C.tree
···
1
+
\date{2025-12-02T08:59:51Z}
2
+
\title{Isabelle Terms}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\p{Terms in Isabelle are essentially terms of the (polymorphic) \em{typed lambda calculus}. When we declare a constant like: }
7
+
\shiki{conj :: "bool ⇒ bool ⇒ bool" (infixr "∧" 35)}
8
+
\p{We are introducing a new constant called \code{conj} that has type \code{bool ⇒ bool ⇒ bool} — that is, a function that takes two values of type \code{bool} and produces another \code{bool}. The \code{infixr} annotation on the right hand side lets us use familiar notation \code{A ∧ B} instead of writing \code{conj A B}, but the meaning of \code{A ∧ B} is identical to \code{conj A B}.}
9
+
\subtree{
10
+
\taxon{Aside}
11
+
\title{Currying}
12
+
\p{Functions of multiple parameters in Isabelle are typically \em{curried}, meaning that a function of type \code{bool ⇒ bool ⇒ bool} is actually a function of type \code{bool ⇒ (bool ⇒ bool)} — a function that, given a \code{bool} value, produces a \em{function} of type \code{bool ⇒ bool}. }
13
+
}
14
+
+12
trees/isa/isa-001D.tree
+12
trees/isa/isa-001D.tree
···
1
+
\date{2025-12-02T09:24:35Z}
2
+
\title{A \code{nand} connective}
3
+
\taxon{Definition}
4
+
\parent{isa-001B}
5
+
\author{liamoc}
6
+
\import{shiki-macros}
7
+
\put\shiki/language{Isabelle Theory}
8
+
9
+
\shiki{definition nand :: ‹bool ⇒ bool ⇒ bool› where
10
+
‹nand a b = (¬ (a ∧ b))›}
11
+
12
+
+40
trees/isa/isa-001E.tree
+40
trees/isa/isa-001E.tree
···
1
+
\date{2025-12-02T09:34:30Z}
2
+
\taxon{Example}
3
+
\parent{isa-001B}
4
+
\import{dt-macros}
5
+
\title{Proving the axioms for \code{nand}}
6
+
\author{liamoc}
7
+
\import{shiki-macros}
8
+
\put\shiki/language{Isabelle Theory}
9
+
\p{We use the [[isa-001F]] method with the lemma generated by \ref{isa-001D} to replace \code{nand} with its definition in our goal:}
10
+
\shiki{lemma nandI1: ‹¬A ⟹ nand A B›}
11
+
\solnblock{
12
+
\shiki{apply (unfold nand_def)
13
+
apply (rule notI)
14
+
apply (erule conjE)
15
+
apply (erule notE)
16
+
apply assumption
17
+
done}}
18
+
\p{ }
19
+
\shiki{lemma nandI2: ‹¬B ⟹ nand A B›}
20
+
\solnblock{
21
+
\shiki{apply (unfold nand_def)
22
+
apply (rule notI)
23
+
apply (erule conjE)
24
+
apply (erule notE)
25
+
apply assumption
26
+
done}}
27
+
\p{ }
28
+
\shiki{lemma nandE: ‹⟦ nand A B; ¬ A ⟹ C; ¬ B ⟹ C ⟧ ⟹ C›}
29
+
\solnblock{
30
+
\shiki{apply (unfold nand_def)
31
+
apply (rule ccontr)
32
+
apply (erule notE)
33
+
apply (rule conjI)
34
+
apply (rule ccontr)
35
+
apply (erule notE)
36
+
apply assumption
37
+
apply (rule ccontr)
38
+
apply (erule notE)
39
+
apply assumption
40
+
done}}
+6
trees/isa/isa-001F.tree
+6
trees/isa/isa-001F.tree
···
1
+
\author{liamoc}
2
+
\taxon{Proof Method}
3
+
\title{\code{unfold}}
4
+
\date{2025-12-02}
5
+
\p{Given a theorem \code{r}#{: A = B} (typically a defining equation given by [the \code{definition} command](isa-001G)), \code{apply (unfold r)} replaces every occurrence of #{A} in the current goal with #{B}.}
6
+
\p{If the theorem \code{r} has premises, then all of those premises must be directly satisfied by assumptions in the current goal for \code{unfold} to succeed.}
+14
trees/isa/isa-001G.tree
+14
trees/isa/isa-001G.tree
···
1
+
\date{2025-12-02T10:30:45Z}
2
+
\author{liamoc}
3
+
\import{shiki-macros}
4
+
\put\shiki/language{Isabelle Theory}
5
+
\title{Isabelle \code{definition}s}
6
+
\p{The Isabelle \code{definition} command is a safer way to define constants than [the \code{axiomatization}](isa-0019) command. The syntax is similiar: }
7
+
\shiki{definition
8
+
my_const :: "type"
9
+
where
10
+
(* equation *)}
11
+
\p{However, there are several differences:}
12
+
\ul{\li{Only one constant (\code{my_const} above) can be defined.}
13
+
\li{Only one axiom can be defined, and it must be an equation of the format \code{my_const ... = ...}, describing the meaning of \code{my_const} in terms of other, already-defined constants.}}
14
+
\p{If no name is given to the defining equation, the default name produced by appending \code{_def} to the name of the constant is used (e.g. \code{my_const_def})}
+28
trees/isa/isa-001H.tree
+28
trees/isa/isa-001H.tree
···
1
+
\date{2025-12-02T12:02:58Z}
2
+
\author{liamoc}
3
+
\taxon{Proof Method}
4
+
\import{dt-macros}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\title{\code{simp}}
8
+
\p{The Isabelle simplifier, or \code{simp}, is one of the most powerful proof automation features in Isabelle, but it is a very simple idea. Given a set of equations, \code{apply (simp)} will (almost) blindly rewrite the goal by all of those equations (as well as any equations that are local assumptions in the goal) left-to-right. Given a sufficiently expressive set of equations, this allows the simplifier to solve many goals (including all of the theorems in \ref{isa-001E}) on its own.}
9
+
\p{The default set of equations that \code{simp} uses is called the \em{simpset}. We can add theorems to the \em{simpset} by attaching the \code{[simp]} attribute to them. }
10
+
\transclude{isa-001I}
11
+
\p{We can also adjust the simpset locally when we invoke the \code{simp} method:}
12
+
13
+
\shiki{lemma nand_xt[simp]: ‹nand A True = (¬ A)›
14
+
by (simp add: nand_def)}
15
+
16
+
\problemblock{
17
+
\p{
18
+
Isabelle does nothing to guarantee that \code{simp} will terminate, nor that it will be \em{confluent} (i.e. the results can depend on the order in which rewrites are applied). In particular, problems with non-termination can arise if there is a cycle in the equations used for rewriting. In such cases, it can be useful to remove certain lemmas from the simpset locally:}
19
+
\shiki{apply (simp del: nand_t)}
20
+
\p{Or explicitly list all the theorems to use:}
21
+
\shiki{apply (simp only: nant_t nand_f)}
22
+
\p{Or disable the simplification and use of local assumptions:}
23
+
\shiki{apply (simp (no_asm))}
24
+
\p{Or disable the simplification of (but still use) local assumptions:}
25
+
\shiki{apply (simp (no_asm_simp))}
26
+
\p{Or disable the use of (but still simplify) local assumptions:}
27
+
\shiki{apply (simp (no_asm_use))}
28
+
}
+21
trees/isa/isa-001I.tree
+21
trees/isa/isa-001I.tree
···
1
+
\date{2025-12-02T12:42:28Z}
2
+
\import{shiki-macros}
3
+
\put\shiki/language{Isabelle Theory}
4
+
\taxon{Example}
5
+
\title{Simplifier rules for \code{nand}}
6
+
\p{
7
+
Continuing our [\code{nand} example](isa-001D), we can prove theorems and attach the \code{[simp]} attribute simultaneously:
8
+
\shiki{lemma nand_t[simp]: ‹nand True A = (¬ A)›
9
+
apply (unfold nand_def)
10
+
apply simp
11
+
done}
12
+
Alternatively, we can add theorems after-the-fact like so:
13
+
\shiki{lemma nand_f: ‹nand False A = True›
14
+
apply (unfold nand_def)
15
+
apply simp
16
+
done
17
+
(* ... *)
18
+
declare nand_f[simp]
19
+
}
20
+
Occasionally it becomes useful to remove a theorem from the simp set. This can be achieved by using the \code{declare} command and the \code{[simp del]} attribute:}
21
+
\shiki{declare nand_f[simp del]}
+10
trees/isa/isa-001J.tree
+10
trees/isa/isa-001J.tree
···
1
+
\date{2025-12-02T12:52:37Z}
2
+
\taxon{Example}
3
+
\parent{isa-001B}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\title{The \code{two} type}
7
+
\shiki{datatype two = ONE | TWO
8
+
print_theorems
9
+
}
10
+
\p{This defines a type called \code{two} with two values, \code{ONE : two} and \code{TWO : two}. The \code{print_theorems} command here allows us to see all of the theorems automatically created by the \code{datatype} command, chiefly that the constants \code{ONE} and \code{TWO} are \em{disjoint} (i.e. \code{ONE ≠ TWO}) and \em{exhaustive} (i.e. that there are no other values of type \code{two} apart from \code{ONE} and \code{TWO}) }
+10
trees/isa/isa-001K.tree
+10
trees/isa/isa-001K.tree
···
1
+
\date{2025-12-02T12:59:55Z}
2
+
\title{The \code{datatype} command}
3
+
\import{shiki-macros}
4
+
\put\shiki/language{Isabelle Theory}
5
+
\p{The \code{datatype} defines a new type (like \code{typedecl}) but also defines some special constants, called \em{constructors}, which make values of that type. Constructors may optionally take arguments, and these data types may be recursive. }
6
+
\shiki{datatype type_name = Constructor1 "arg_type1" "arg_type2" (* ... *)
7
+
| Constructor2 (* ... *)
8
+
(* ... *)
9
+
}
10
+
\p{These datatypes are analogous to the algebraic data types found in many functional programming languages.}
+8
trees/isa/isa-001L.tree
+8
trees/isa/isa-001L.tree
···
1
+
\date{2025-12-02T13:17:21Z}
2
+
\taxon{Proof Method}
3
+
\title{\code{case_tac}}
4
+
\author{liamoc}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\p{The \code{case_tac} method splits the current goal into multiple cases. Given a term \code{t} of type #{\tau}, \code{apply (case_tac t)} will produce a new goal for each possible case of \code{t} according to the \code{.cases} theorem for the type #{\tau}.}
8
+
\p{This works for all types defined with \code{datatype}, as well as for natural numbers (type \code{nat}) and \code{bool}s — often an easier way to do classical reasoning than using \code{rule ccontr}. }
+27
trees/isa/isa-001M.tree
+27
trees/isa/isa-001M.tree
···
1
+
\date{2025-12-02T13:27:09Z}
2
+
\author{liamoc}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\parent{isa-001B}
6
+
\taxon{Example}
7
+
\put\shiki/language{Isabelle Theory}
8
+
\shiki{lemma ‹f (f (f (b::two))) = f b›}
9
+
\solnblock{
10
+
\shiki{apply (case_tac b)
11
+
apply simp
12
+
apply (case_tac "(f ONE)")
13
+
apply simp
14
+
apply simp
15
+
apply (case_tac "(f TWO)")
16
+
apply simp
17
+
apply simp
18
+
apply (case_tac "(f ONE)")
19
+
apply simp
20
+
apply (case_tac "(f TWO)")
21
+
apply simp
22
+
apply simp
23
+
apply simp
24
+
apply (case_tac "(f TWO)")
25
+
apply simp
26
+
apply simp
27
+
done}}