my forest
finish all but the last chunk of notes
+118
-35
+1
trees/isa/isa-0001.tree
+1
trees/isa/isa-0001.tree
-22
trees/isa/isa-001B.tree
-22
trees/isa/isa-001B.tree
···
50
50
\transclude{isa-0025}
51
51
\transclude{isa-0026}
52
52
\transclude{isa-0027}
53
-
\transclude{isa-0028}
54
-
\transclude{isa-002A}
55
-
\transclude{isa-0029}
56
-
\transclude{isa-002B}
57
-
\transclude{isa-002C}
58
-
\transclude{isa-002D}
59
-
\transclude{isa-002E}
60
-
\transclude{isa-002F}
61
-
\transclude{isa-002G}
62
-
\transclude{isa-002H}
63
-
\transclude{isa-002I}
64
-
\transclude{isa-002J}
65
-
\ul{
66
-
\li{safe vs unsafe rules}
67
-
\li{intro, elim, clarify, blast, (fast,slow,best)}
68
-
\li{automation: clarsimp, auto, fastforce (slowsimp, bestsimp), force}
69
-
\li{sledgehammer, try, find_theorems}
70
-
\li{clarify, clarsimp}
71
-
\li{structured proofs}
72
-
\li{calculational proofs}
73
-
\li{examples examples examples}
74
-
}
+3
-1
trees/isa/isa-0028.tree
+3
-1
trees/isa/isa-0028.tree
···
1
1
\date{2025-12-03T06:13:19Z}
2
2
\author{liamoc}
3
3
\title{\code{inductive} predicates}
4
-
\p{TODO}
4
+
\p{With the \code{inductive} command, we define a predicate by specifying a collection of inference rules, and the inductive predicate is the smallest predicate closed under those rules.}
5
+
\p{In other words: An element satisfies the predicate exactly if it can be derived using the given rules.}
6
+
\p{From the given rules, Isabelle automatically generates an induction principle (\code{.induct}) which can be used with the \code{induct} method (see \ref{isa-0029}) and a cases theorem (\code{.cases}) for use with the [[isa-001L]] method. }
+8
-1
trees/isa/isa-0029.tree
+8
-1
trees/isa/isa-0029.tree
···
1
1
\date{2025-12-03T06:14:12Z}
2
2
\author{liamoc}
3
3
\taxon{Proof Method}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
4
6
\title{\code{induct} (for rule induction)}
5
-
\p{TODO}
7
+
\p{You’ve already seen [how to use \code{induct}](isa-001P) for structural induction. Exactly the same \code{induct} method can also be used for rule induction, when your induction is over an \code{inductive}ly defined predicate, not over the structure of some \code{datatype}.}
8
+
\p{When you define a predicate \code{p} with the [\code{inductive} command](isa-0028), Isabelle automatically produces an induction rule named \code{p.induct}. This rule expresses how to perform induction over derivations of \code{p x}, one case for each introduction rule of the predicate.}
9
+
\p{Although you could apply the raw rule with \code{rule} or \code{erule}, it is almost always easier to use:}
10
+
\shiki{apply (induct rule: p.induct)}
11
+
\p{This behaves just like structural induction:
12
+
The goal is split into one subgoal per introduction rule of the predicate, and recursive premises of the rules give rise to induction hypotheses, added to your assumptions.}
+1
-1
trees/isa/isa-002B.tree
+1
-1
trees/isa/isa-002B.tree
+1
-1
trees/isa/isa-002C.tree
+1
-1
trees/isa/isa-002C.tree
+1
-1
trees/isa/isa-002D.tree
+1
-1
trees/isa/isa-002D.tree
+1
-1
trees/isa/isa-002E.tree
+1
-1
trees/isa/isa-002E.tree
···
4
4
\import{dt-macros}
5
5
\put\shiki/language{Isabelle Theory}
6
6
\author{liamoc}
7
-
\parent{isa-001B}
7
+
\parent{isa-002N}
8
8
\title{Length of \code{subsequence}}
9
9
\shiki{lemma ss_length : ‹subsequence xs ys ⟹ length xs ≤ length ys›}
10
10
\solnblock{\shiki{apply (induct rule: subsequence.induct)
+14
-1
trees/isa/isa-002F.tree
+14
-1
trees/isa/isa-002F.tree
···
1
1
\date{2025-12-03T06:41:41Z}
2
2
\title{Controlling backtracking, chaining methods with comma}
3
3
\author{liamoc}
4
-
\p{TODO}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\p{Some methods (like [\code{erule}](isa-0011) when there are multiple matching assumptions) are \em{nondeterministic}, producing multiple alternative proof states.}
7
+
\p{The \code{back} command interactively explores a different alternative branch produced by the previous step.}
8
+
\shiki{lemma "C ∧ D ⟹ A ∧ B ⟹ A"
9
+
apply (erule conjE) (* could apply to either assumption *)
10
+
back
11
+
apply assumption
12
+
done}
13
+
\p{This is useful for interactive exploration, but is \em{very brittle} and considered poor style.}
14
+
\p{Instead, we can combine methods with the \em{comma} operator \code{,}: The command \code{apply (m1, m2)} first runs \code{m1}, and then runs \code{m2}, accepting only the nondeterministic branches where the second method \code{m2} succeeds. This avoids the need for back:}
15
+
\shiki{lemma "C ∧ D ⟹ A ∧ B ⟹ A"
16
+
apply (erule conjE, assumption)
17
+
done}
+5
-1
trees/isa/isa-002G.tree
+5
-1
trees/isa/isa-002G.tree
···
1
1
\date{2025-12-03T06:42:16Z}
2
2
\title{Repeating methods with \code{+}}
3
3
\author{liamoc}
4
-
\p{TODO}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\p{For a method \code{m}:}
7
+
\shiki{apply (m)+}
8
+
\p{Repeatedly applies the \code{m} as many times as possible until it fails. It stops automatically when \code{m} can no longer make progress; and does not backtrack.}
+3
-3
trees/isa/isa-002H.tree
+3
-3
trees/isa/isa-002H.tree
···
4
4
\import{dt-macros}
5
5
\put\shiki/language{Isabelle Theory}
6
6
\author{liamoc}
7
-
\parent{isa-001B}
7
+
\parent{isa-002N}
8
8
\title{Antisymmetry of \code{subsequence}}
9
9
\shiki{lemma ss_antisym: ‹subsequence ys xs ⟹ subsequence xs ys ⟹ xs = ys›}
10
10
\solnblock{\shiki{apply (induct rule: subsequence.induct)
11
11
apply simp
12
12
apply simp
13
-
apply (erule subsequence.cases, clarsimp, clarsimp,clarsimp)
13
+
apply (erule subsequence.cases, simp, simp, simp)
14
14
apply (drule ss_length)+
15
-
apply simp
15
+
apply (drule sym, simp)
16
16
apply (drule ss_length)+
17
17
apply simp
18
18
done}}
+6
-1
trees/isa/isa-002I.tree
+6
-1
trees/isa/isa-002I.tree
···
1
1
\date{2025-12-03T06:48:06Z}
2
2
\author{liamoc}
3
+
\import{shiki-macros}
4
+
\put\shiki/language{Isabelle Theory}
3
5
\title{Generalising the induction hypothesis with \code{arbitrary}}
4
-
\p{TODO}
6
+
\p{By default, [structural induction](isa-001P) \code{induct t} produces an induction hypothesis for the variables directly mentioned in \code{t}, and [rule induction](isa-0029) \code{induct rule: p.induct} produces a hypothesis for the variables directly mentioned by the eliminated \code{p} assumption.}
7
+
\p{Sometimes you need a stronger hypothesis that generalises across additional variables in the goal. The \code{arbitrary} option tells the \code{induct} method to generalise certain variables, so the induction hypothesis assumes the property holds for all values of those variables.}
8
+
9
+
\transclude{isa-002M}
+1
-1
trees/isa/isa-002J.tree
+1
-1
trees/isa/isa-002J.tree
···
4
4
\import{dt-macros}
5
5
\put\shiki/language{Isabelle Theory}
6
6
\author{liamoc}
7
-
\parent{isa-001B}
7
+
\parent{isa-002N}
8
8
\title{Transitivity of \code{subsequence}}
9
9
\shiki{lemma ss_trans: ‹subsequence ys zs ⟹ subsequence xs ys ⟹ subsequence xs zs›}
10
10
\solnblock{\shiki{apply (induct ys zs arbitrary: xs rule: subsequence.induct)
+10
trees/isa/isa-002K.tree
+10
trees/isa/isa-002K.tree
···
1
+
\date{2025-12-03T11:17:28Z}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\import{shiki-macros}
5
+
\parent{isa-002N}
6
+
\title{Even numbers as an \code{inductive}}
7
+
\put\shiki/language{Isabelle Theory}
8
+
\shiki{inductive even :: "nat ⇒ bool" where
9
+
even0: "even 0"
10
+
| evenSS: "even n ⟹ even (Suc (Suc n))"}
+17
trees/isa/isa-002L.tree
+17
trees/isa/isa-002L.tree
···
1
+
\date{2025-12-03T11:17:28Z}
2
+
\author{liamoc}
3
+
\taxon{Exercise}
4
+
\import{shiki-macros}
5
+
\import{dt-macros}
6
+
\parent{isa-002N}
7
+
\title{Even numbers are multiples of two}
8
+
\put\shiki/language{Isabelle Theory}
9
+
\shiki{lemma "even n ⟹ ∃m. (m * 2 = n)"}
10
+
\solnblock{
11
+
\shiki{apply (induct rule: even.induct)
12
+
apply simp
13
+
apply (erule exE)
14
+
apply (rule_tac x = ‹Suc m› in exI)
15
+
apply simp
16
+
done}}
17
+
+15
trees/isa/isa-002M.tree
+15
trees/isa/isa-002M.tree
···
1
+
\date{2025-12-03T12:43:00Z}
2
+
\author{liamoc}
3
+
\import{shiki-macros}
4
+
\put\shiki/language{Isabelle Theory}
5
+
\taxon{Example}
6
+
\title{Inequality as an \code{inductive}}
7
+
\shiki{inductive myLE :: "nat ⇒ nat ⇒ bool" where
8
+
base: "myLE 0 n"
9
+
| step: "myLE m n ⟹ myLE (Suc m) (n+1)"}
10
+
\p{Proving that this implies the normal inequality relation requires the use of [variable generalising](isa-002I):}
11
+
\shiki{lemma "myLE m n ⟹ m ≤ n"
12
+
apply (induct m arbitrary: n)
13
+
apply simp
14
+
apply (erule myLE.cases; simp)
15
+
done}
+31
trees/isa/isa-002N.tree
+31
trees/isa/isa-002N.tree
···
1
+
\date{2025-12-03T12:50:18Z}
2
+
\author{liamoc}
3
+
\taxon{Lecture}
4
+
\title{Rule Induction, Automation, Structured Proofs}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\p{This lecture continues the theory file begun in \ref{isa-001B}.}
8
+
\transclude{isa-0028}
9
+
\transclude{isa-002K}
10
+
\transclude{isa-0029}
11
+
\transclude{isa-002L}
12
+
\transclude{isa-002A}
13
+
\transclude{isa-002B}
14
+
\transclude{isa-002C}
15
+
\transclude{isa-002D}
16
+
\transclude{isa-002E}
17
+
\transclude{isa-002F}
18
+
\transclude{isa-002G}
19
+
\transclude{isa-002H}
20
+
\transclude{isa-002I}
21
+
\transclude{isa-002J}
22
+
\ul{
23
+
\li{safe vs unsafe rules}
24
+
\li{intro, elim, clarify, blast, (fast,slow,best)}
25
+
\li{automation: clarsimp, auto, fastforce (slowsimp, bestsimp), force}
26
+
\li{sledgehammer, try, find_theorems}
27
+
\li{clarify, clarsimp}
28
+
\li{structured proofs}
29
+
\li{calculational proofs}
30
+
\li{examples examples examples}
31
+
}