diff --git a/trees/isa/isa-0001.tree b/trees/isa/isa-0001.tree index 07d34da..16ee571 100644 --- a/trees/isa/isa-0001.tree +++ b/trees/isa/isa-0001.tree @@ -3,3 +3,4 @@ \taxon{Lecture Notes} \p{These notes are the basis of my short course at the [ANU Logic Summer School]() 2025. \strong{THEY ARE NOT YET COMPLETE.}} \transclude{isa-0002} +\transclude{isa-001B} diff --git a/trees/isa/isa-0002.tree b/trees/isa/isa-0002.tree index 7eecb19..9430643 100644 --- a/trees/isa/isa-0002.tree +++ b/trees/isa/isa-0002.tree @@ -6,16 +6,12 @@ \put\shiki/language{Isabelle Theory} \transclude{isa-0003} - -\shiki{theory ND - imports Pure -begin - -typedecl bool -judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5) -} - +\transclude{isa-0016} +\transclude{isa-0017} +\transclude{isa-0018} \transclude{isa-0005} +\transclude{isa-0019} +\transclude{isa-001C} \transclude{isa-000Z} \transclude{isa-0010} \transclude{isa-000C} @@ -38,7 +34,9 @@ judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5) \transclude{isa-000J} \transclude{isa-000K} \transclude{isa-000L} + \transclude{isa-000N} +\transclude{isa-001A} \transclude{isa-000P} \transclude{isa-000O} \transclude{isa-000Q} diff --git a/trees/isa/isa-000M.tree b/trees/isa/isa-000M.tree index 4b56442..df8f060 100644 --- a/trees/isa/isa-000M.tree +++ b/trees/isa/isa-000M.tree @@ -6,7 +6,7 @@ \import{dt-macros} \put\shiki/language{Isabelle Theory} -\shiki{lemma imp_as_disj: "¬ A ⟶ B ⟹ A ∨ B" } +\shiki{lemma disjCI: "¬ A ⟶ B ⟹ A ∨ B" } \solnblock{\shiki{apply (rule ccontr) apply (erule impE) diff --git a/trees/isa/isa-000N.tree b/trees/isa/isa-000N.tree index 782800b..4da43bb 100644 --- a/trees/isa/isa-000N.tree +++ b/trees/isa/isa-000N.tree @@ -7,8 +7,8 @@ \put\shiki/language{Isabelle Theory} \shiki{axiomatization - All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10) - where - allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and - spec : ‹∀ a. P a ⟹ P x› + All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10) +where + allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and + spec : ‹∀ a. P a ⟹ P x› } diff --git a/trees/isa/isa-000Y.tree b/trees/isa/isa-000Y.tree index add6d11..9f089a3 100644 --- a/trees/isa/isa-000Y.tree +++ b/trees/isa/isa-000Y.tree @@ -13,7 +13,7 @@ apply (frule_tac x = a in allE, assumption) apply (drule_tac x = a in spec) apply (frule_tac x = "M a" in spec) apply (drule_tac x = "M (M a)" in spec) -apply (drule imp_as_disj)+ +apply (drule disjCI)+ apply (elim disjE) apply (rule_tac x = a in exI; intro conjI; assumption) apply (rule_tac x = "M a" in exI; intro conjI; assumption) diff --git a/trees/isa/isa-0016.tree b/trees/isa/isa-0016.tree new file mode 100644 index 0000000..dffa6f8 --- /dev/null +++ b/trees/isa/isa-0016.tree @@ -0,0 +1,12 @@ +\date{2025-12-02T05:04:28Z} +\author{liamoc} +\parent{isa-0002} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{Definining Theories} +\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}. } +\shiki{theory HOLFromScratch + imports Pure +begin +} +\p{We imported the theory \code{Pure}, which contains only the very basic built-in structures that define Isabelle's logic. } \ No newline at end of file diff --git a/trees/isa/isa-0017.tree b/trees/isa/isa-0017.tree new file mode 100644 index 0000000..0127f20 --- /dev/null +++ b/trees/isa/isa-0017.tree @@ -0,0 +1,18 @@ +\date{2025-12-02T05:07:23Z} +\author{liamoc} +\parent{isa-0002} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{HHFs and Isabelle/Pure} +\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}. } +\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.} +\shiki{typedecl bool +judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5) +} +\p{Formulae in Isabelle are \em{hereditary Harrop formulae}, defined as:} +##{\begin{array}{lclll} +\varphi & ::= & \bigwedge x.\ \varphi & & \textit{(meta-forall)} \\ + & \mid & \varphi \implies \varphi & & \textit{(meta-implication)}\\ + & \mid & t & \text{where}\ t\ \text{:: \texttt{bool}} & \textit{(judgments)} +\end{array}} +\p{In Isabelle's syntax, formulae, terms, and types are typically surrounded by quote marks \code{""} or cartouches \code{‹›} — the two are equivalent.} \ No newline at end of file diff --git a/trees/isa/isa-0018.tree b/trees/isa/isa-0018.tree new file mode 100644 index 0000000..e57fe81 --- /dev/null +++ b/trees/isa/isa-0018.tree @@ -0,0 +1,16 @@ +\date{2025-12-02T05:08:28Z} +\taxon{Example} +\author{liamoc} +\title{Isabelle's Syntax for HHFs} +\p{Consider the following rule: ##{\dfrac{A \quad B}{A \land B}{\text{\small conjI}}} +This is encoded as an Isabelle formula as follows: +##{\bigwedge A. \left(\bigwedge B. (A \implies (B \implies (A \land B)))\right) } +} +\p{Because #{\implies} is right-associative, we can remove some parentheses:} +##{\bigwedge A. \left(\bigwedge B. (A \implies B \implies A \land B)\right) } +\p{We can also combine the meta-quantifiers:} +##{\bigwedge A\ B.\;\; A \implies B \implies A \land B } +\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}.} +##{\bigwedge A\ B.\;\; \llbracket A; B\rrbracket \implies A \land B } +\p{Isabelle will also automatically add quantifiers to unknown variables, so we can drop the meta-quantifiers from the outermost part of the formula:} +##{\llbracket A; B\rrbracket \implies A \land B } \ No newline at end of file diff --git a/trees/isa/isa-0019.tree b/trees/isa/isa-0019.tree new file mode 100644 index 0000000..748771d --- /dev/null +++ b/trees/isa/isa-0019.tree @@ -0,0 +1,17 @@ +\date{2025-12-02T05:15:07Z} +\author{liamoc} +\import{dt-macros} +\title{Isabelle \code{axiomatization}s} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\p{Isabelle's basic mechanism to define new things is the \code{axiomatization} command.} +\shiki{axiomatization + (* constants *) +where + (* axioms *)} +\p{This defines the constants (with their types) in the \code{constants} section, and assumes the formulae stated in the \code{axioms} section. } +\problemblock{ + \p{ + 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. +} +} \ No newline at end of file diff --git a/trees/isa/isa-001A.tree b/trees/isa/isa-001A.tree new file mode 100644 index 0000000..d5df4f6 --- /dev/null +++ b/trees/isa/isa-001A.tree @@ -0,0 +1,9 @@ +\date{2025-11-28T05:41:54Z} +\taxon{Proof Method} +\title{\code{rule_tac}, \code{erule_tac}, \code{drule_tac}, \code{frule_tac}} +\author{liamoc} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\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.} +\shiki{apply (rule_tac x = "term" in exI)} + diff --git a/trees/isa/isa-001B.tree b/trees/isa/isa-001B.tree new file mode 100644 index 0000000..5bf68da --- /dev/null +++ b/trees/isa/isa-001B.tree @@ -0,0 +1,34 @@ +\date{2025-12-02T05:59:44Z} +\author{liamoc} +\taxon{Lecture} +\title{Definitions, Datatypes, Induction, Functions} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} + +\shiki{theory Definitions + imports Main +begin +} +\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:} +\ul{ + \li{Axioms for defining \em{equality}. Try the following: \shiki{thm refl +thm sym +thm trans +thm iffI +thm ssubst} +} +\li{A theory of [sets](https://isabelle.in.tum.de/library/HOL/HOL/Set.html).} +\li{A theory of [natural numbers](https://isabelle.in.tum.de/library/HOL/HOL/Nat.html)} +\li{A theory of [lists](https://isabelle.in.tum.de/library/HOL/HOL/List.html)} +\li{And much more!} +} + +\transclude{isa-001G} +\transclude{isa-001D} +\transclude{isa-001F} +\transclude{isa-001E} +\transclude{isa-001H} +\transclude{isa-001K} +\transclude{isa-001J} +\transclude{isa-001L} +\transclude{isa-001M} diff --git a/trees/isa/isa-001C.tree b/trees/isa/isa-001C.tree new file mode 100644 index 0000000..550e711 --- /dev/null +++ b/trees/isa/isa-001C.tree @@ -0,0 +1,14 @@ +\date{2025-12-02T08:59:51Z} +\title{Isabelle Terms} +\author{liamoc} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\p{Terms in Isabelle are essentially terms of the (polymorphic) \em{typed lambda calculus}. When we declare a constant like: } +\shiki{conj :: "bool ⇒ bool ⇒ bool" (infixr "∧" 35)} +\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}.} +\subtree{ + \taxon{Aside} + \title{Currying} + \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}. } +} + diff --git a/trees/isa/isa-001D.tree b/trees/isa/isa-001D.tree new file mode 100644 index 0000000..698bf7f --- /dev/null +++ b/trees/isa/isa-001D.tree @@ -0,0 +1,12 @@ +\date{2025-12-02T09:24:35Z} +\title{A \code{nand} connective} +\taxon{Definition} +\parent{isa-001B} +\author{liamoc} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} + +\shiki{definition nand :: ‹bool ⇒ bool ⇒ bool› where + ‹nand a b = (¬ (a ∧ b))›} + + diff --git a/trees/isa/isa-001E.tree b/trees/isa/isa-001E.tree new file mode 100644 index 0000000..94e46fb --- /dev/null +++ b/trees/isa/isa-001E.tree @@ -0,0 +1,40 @@ +\date{2025-12-02T09:34:30Z} +\taxon{Example} +\parent{isa-001B} +\import{dt-macros} +\title{Proving the axioms for \code{nand}} +\author{liamoc} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\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:} +\shiki{lemma nandI1: ‹¬A ⟹ nand A B›} +\solnblock{ +\shiki{apply (unfold nand_def) +apply (rule notI) +apply (erule conjE) +apply (erule notE) +apply assumption +done}} +\p{ } +\shiki{lemma nandI2: ‹¬B ⟹ nand A B›} +\solnblock{ +\shiki{apply (unfold nand_def) +apply (rule notI) +apply (erule conjE) +apply (erule notE) +apply assumption +done}} +\p{ } +\shiki{lemma nandE: ‹⟦ nand A B; ¬ A ⟹ C; ¬ B ⟹ C ⟧ ⟹ C›} +\solnblock{ +\shiki{apply (unfold nand_def) +apply (rule ccontr) +apply (erule notE) +apply (rule conjI) + apply (rule ccontr) + apply (erule notE) + apply assumption +apply (rule ccontr) +apply (erule notE) +apply assumption +done}} \ No newline at end of file diff --git a/trees/isa/isa-001F.tree b/trees/isa/isa-001F.tree new file mode 100644 index 0000000..f3f7245 --- /dev/null +++ b/trees/isa/isa-001F.tree @@ -0,0 +1,6 @@ +\author{liamoc} +\taxon{Proof Method} +\title{\code{unfold}} +\date{2025-12-02} +\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}.} +\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.} \ No newline at end of file diff --git a/trees/isa/isa-001G.tree b/trees/isa/isa-001G.tree new file mode 100644 index 0000000..48f1e0f --- /dev/null +++ b/trees/isa/isa-001G.tree @@ -0,0 +1,14 @@ +\date{2025-12-02T10:30:45Z} +\author{liamoc} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{Isabelle \code{definition}s} +\p{The Isabelle \code{definition} command is a safer way to define constants than [the \code{axiomatization}](isa-0019) command. The syntax is similiar: } +\shiki{definition + my_const :: "type" +where + (* equation *)} +\p{However, there are several differences:} +\ul{\li{Only one constant (\code{my_const} above) can be defined.} +\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.}} +\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})} \ No newline at end of file diff --git a/trees/isa/isa-001H.tree b/trees/isa/isa-001H.tree new file mode 100644 index 0000000..f1e9538 --- /dev/null +++ b/trees/isa/isa-001H.tree @@ -0,0 +1,28 @@ +\date{2025-12-02T12:02:58Z} +\author{liamoc} +\taxon{Proof Method} +\import{dt-macros} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{\code{simp}} +\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.} +\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. } +\transclude{isa-001I} +\p{We can also adjust the simpset locally when we invoke the \code{simp} method:} + +\shiki{lemma nand_xt[simp]: ‹nand A True = (¬ A)› +by (simp add: nand_def)} + +\problemblock{ + \p{ + 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:} + \shiki{apply (simp del: nand_t)} + \p{Or explicitly list all the theorems to use:} + \shiki{apply (simp only: nant_t nand_f)} + \p{Or disable the simplification and use of local assumptions:} + \shiki{apply (simp (no_asm))} + \p{Or disable the simplification of (but still use) local assumptions:} + \shiki{apply (simp (no_asm_simp))} + \p{Or disable the use of (but still simplify) local assumptions:} + \shiki{apply (simp (no_asm_use))} +} diff --git a/trees/isa/isa-001I.tree b/trees/isa/isa-001I.tree new file mode 100644 index 0000000..6fd508f --- /dev/null +++ b/trees/isa/isa-001I.tree @@ -0,0 +1,21 @@ +\date{2025-12-02T12:42:28Z} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\taxon{Example} +\title{Simplifier rules for \code{nand}} + \p{ + Continuing our [\code{nand} example](isa-001D), we can prove theorems and attach the \code{[simp]} attribute simultaneously: +\shiki{lemma nand_t[simp]: ‹nand True A = (¬ A)› + apply (unfold nand_def) + apply simp + done} + Alternatively, we can add theorems after-the-fact like so: +\shiki{lemma nand_f: ‹nand False A = True› + apply (unfold nand_def) + apply simp + done +(* ... *) +declare nand_f[simp] +} +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:} +\shiki{declare nand_f[simp del]} diff --git a/trees/isa/isa-001J.tree b/trees/isa/isa-001J.tree new file mode 100644 index 0000000..5086a02 --- /dev/null +++ b/trees/isa/isa-001J.tree @@ -0,0 +1,10 @@ +\date{2025-12-02T12:52:37Z} +\taxon{Example} +\parent{isa-001B} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{The \code{two} type} +\shiki{datatype two = ONE | TWO +print_theorems +} +\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}) } diff --git a/trees/isa/isa-001K.tree b/trees/isa/isa-001K.tree new file mode 100644 index 0000000..ae7c58d --- /dev/null +++ b/trees/isa/isa-001K.tree @@ -0,0 +1,10 @@ +\date{2025-12-02T12:59:55Z} +\title{The \code{datatype} command} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\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. } +\shiki{datatype type_name = Constructor1 "arg_type1" "arg_type2" (* ... *) + | Constructor2 (* ... *) + (* ... *) +} +\p{These datatypes are analogous to the algebraic data types found in many functional programming languages.} \ No newline at end of file diff --git a/trees/isa/isa-001L.tree b/trees/isa/isa-001L.tree new file mode 100644 index 0000000..cdf86ce --- /dev/null +++ b/trees/isa/isa-001L.tree @@ -0,0 +1,8 @@ +\date{2025-12-02T13:17:21Z} +\taxon{Proof Method} +\title{\code{case_tac}} +\author{liamoc} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\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}.} +\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}. } \ No newline at end of file diff --git a/trees/isa/isa-001M.tree b/trees/isa/isa-001M.tree new file mode 100644 index 0000000..594070c --- /dev/null +++ b/trees/isa/isa-001M.tree @@ -0,0 +1,27 @@ +\date{2025-12-02T13:27:09Z} +\author{liamoc} +\import{shiki-macros} +\import{dt-macros} +\parent{isa-001B} +\taxon{Example} +\put\shiki/language{Isabelle Theory} +\shiki{lemma ‹f (f (f (b::two))) = f b›} +\solnblock{ +\shiki{apply (case_tac b) + apply simp + apply (case_tac "(f ONE)") + apply simp + apply simp + apply (case_tac "(f TWO)") + apply simp + apply simp +apply (case_tac "(f ONE)") + apply simp + apply (case_tac "(f TWO)") + apply simp + apply simp +apply simp +apply (case_tac "(f TWO)") + apply simp +apply simp +done}} \ No newline at end of file