From 79d00e7f08b900325238da7a8f7ddbe41e2c03a8 Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Wed, 3 Dec 2025 17:52:52 +1100 Subject: [PATCH] isa: more notes --- trees/isa/isa-001B.tree | 59 ++++++++++++++++++++++------------------- trees/isa/isa-001J.tree | 6 ++--- trees/isa/isa-001K.tree | 9 ++++++- trees/isa/isa-001M.tree | 2 +- trees/isa/isa-001N.tree | 7 +++++ trees/isa/isa-001O.tree | 23 ++++++++++++++++ trees/isa/isa-001P.tree | 8 ++++++ trees/isa/isa-001Q.tree | 17 ++++++++++++ trees/isa/isa-001R.tree | 10 +++++++ trees/isa/isa-001S.tree | 10 +++++++ trees/isa/isa-001T.tree | 19 +++++++++++++ trees/isa/isa-001U.tree | 12 +++++++++ trees/isa/isa-001V.tree | 14 ++++++++++ trees/isa/isa-001W.tree | 21 +++++++++++++++ trees/isa/isa-001X.tree | 9 +++++++ trees/isa/isa-001Y.tree | 13 +++++++++ trees/isa/isa-001Z.tree | 11 ++++++++ trees/isa/isa-0020.tree | 11 ++++++++ trees/isa/isa-0021.tree | 15 +++++++++++ trees/isa/isa-0022.tree | 11 ++++++++ trees/isa/isa-0023.tree | 10 +++++++ trees/isa/isa-0024.tree | 10 +++++++ trees/isa/isa-0025.tree | 10 +++++++ trees/isa/isa-0026.tree | 10 +++++++ trees/isa/isa-0027.tree | 16 +++++++++++ trees/isa/isa-0028.tree | 4 +++ trees/isa/isa-0029.tree | 5 ++++ trees/isa/isa-002A.tree | 13 +++++++++ trees/isa/isa-002B.tree | 20 ++++++++++++++ trees/isa/isa-002C.tree | 11 ++++++++ trees/isa/isa-002D.tree | 14 ++++++++++ trees/isa/isa-002E.tree | 14 ++++++++++ trees/isa/isa-002F.tree | 4 +++ trees/isa/isa-002G.tree | 4 +++ trees/isa/isa-002H.tree | 20 ++++++++++++++ trees/isa/isa-002I.tree | 4 +++ trees/isa/isa-002J.tree | 42 +++++++++++++++++++++++++++++ 37 files changed, 465 insertions(+), 33 deletions(-) create mode 100644 trees/isa/isa-001N.tree create mode 100644 trees/isa/isa-001O.tree create mode 100644 trees/isa/isa-001P.tree create mode 100644 trees/isa/isa-001Q.tree create mode 100644 trees/isa/isa-001R.tree create mode 100644 trees/isa/isa-001S.tree create mode 100644 trees/isa/isa-001T.tree create mode 100644 trees/isa/isa-001U.tree create mode 100644 trees/isa/isa-001V.tree create mode 100644 trees/isa/isa-001W.tree create mode 100644 trees/isa/isa-001X.tree create mode 100644 trees/isa/isa-001Y.tree create mode 100644 trees/isa/isa-001Z.tree create mode 100644 trees/isa/isa-0020.tree create mode 100644 trees/isa/isa-0021.tree create mode 100644 trees/isa/isa-0022.tree create mode 100644 trees/isa/isa-0023.tree create mode 100644 trees/isa/isa-0024.tree create mode 100644 trees/isa/isa-0025.tree create mode 100644 trees/isa/isa-0026.tree create mode 100644 trees/isa/isa-0027.tree create mode 100644 trees/isa/isa-0028.tree create mode 100644 trees/isa/isa-0029.tree create mode 100644 trees/isa/isa-002A.tree create mode 100644 trees/isa/isa-002B.tree create mode 100644 trees/isa/isa-002C.tree create mode 100644 trees/isa/isa-002D.tree create mode 100644 trees/isa/isa-002E.tree create mode 100644 trees/isa/isa-002F.tree create mode 100644 trees/isa/isa-002G.tree create mode 100644 trees/isa/isa-002H.tree create mode 100644 trees/isa/isa-002I.tree create mode 100644 trees/isa/isa-002J.tree diff --git a/trees/isa/isa-001B.tree b/trees/isa/isa-001B.tree index 69debb0..346cb8f 100644 --- a/trees/isa/isa-001B.tree +++ b/trees/isa/isa-001B.tree @@ -32,36 +32,39 @@ thm ssubst} \transclude{isa-001J} \transclude{isa-001L} \transclude{isa-001M} +\transclude{isa-001N} +\transclude{isa-001O} +\transclude{isa-001P} +\transclude{isa-001S} +\transclude{isa-001T} +\transclude{isa-001U} +\transclude{isa-001V} +\transclude{isa-001W} +\transclude{isa-001X} +\transclude{isa-001Y} +\transclude{isa-001Z} +\transclude{isa-0021} +\transclude{isa-0022} +\transclude{isa-0024} +\transclude{isa-0023} +\transclude{isa-0025} +\transclude{isa-0026} +\transclude{isa-0027} +\transclude{isa-0028} +\transclude{isa-002A} +\transclude{isa-0029} +\transclude{isa-002B} +\transclude{isa-002C} +\transclude{isa-002D} +\transclude{isa-002E} +\transclude{isa-002F} +\transclude{isa-002G} +\transclude{isa-002H} +\transclude{isa-002I} +\transclude{isa-002J} \ul{ - \li{natural numbers} - \li{Fun command} - \li{rpt} - \li{induct method (structural)} - \li{rpt twice theorem} - \li{twos type} - \li{prepend} - \li{prepend prepend theorem} - \li{semicolon operator} - \li{append} - \li{append prepend theorem} - \li{append assoc} - \li{lists (replicate function)} - \li{decompress} - \li{compress} - \li{decompress compress thm} - \li{compress app} - \li{compress replicate} - \li{inductive predicates} - \li{rule induction} - \li{wellformedness} - \li{compress decompress thm} - \li{arbitrary} - \li{chaining} - \li{repeating} - \li{subsequence example} - \li{subsequence theorems} \li{safe vs unsafe rules} - \li{intro, elim, clarify, blast, (fast,slow,best)}} + \li{intro, elim, clarify, blast, (fast,slow,best)} \li{automation: clarsimp, auto, fastforce (slowsimp, bestsimp), force} \li{sledgehammer, try, find_theorems} \li{clarify, clarsimp} diff --git a/trees/isa/isa-001J.tree b/trees/isa/isa-001J.tree index 5086a02..45b06ad 100644 --- a/trees/isa/isa-001J.tree +++ b/trees/isa/isa-001J.tree @@ -3,8 +3,8 @@ \parent{isa-001B} \import{shiki-macros} \put\shiki/language{Isabelle Theory} -\title{The \code{two} type} -\shiki{datatype two = ONE | TWO +\title{The \code{oot} type} +\shiki{datatype oot = 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}) } +\p{This defines a type called \code{oot} with two values, \code{ONE : oot} and \code{TWO : oot}. 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{oot} apart from \code{ONE} and \code{TWO}) } diff --git a/trees/isa/isa-001K.tree b/trees/isa/isa-001K.tree index ae7c58d..03abb2e 100644 --- a/trees/isa/isa-001K.tree +++ b/trees/isa/isa-001K.tree @@ -1,5 +1,6 @@ \date{2025-12-02T12:59:55Z} \title{The \code{datatype} command} +\author{liamoc} \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. } @@ -7,4 +8,10 @@ | Constructor2 (* ... *) (* ... *) } -\p{These datatypes are analogous to the algebraic data types found in many functional programming languages.} \ No newline at end of file +\p{These datatypes are analogous to the algebraic data types found in many functional programming languages.} +\p{The \code{datatype} command automatically proves many lemmas about these types for you, chiefly:} +\ul{ +\li{Disjointness: Values made with one constructor are not equal to values made with another constructor.} +\li{Exhaustivity: The only values of this type are those made by the listed constructors.} +\li{Injectivity: Two values of the same constructor are equal iff their arguments are equal.} +} \ No newline at end of file diff --git a/trees/isa/isa-001M.tree b/trees/isa/isa-001M.tree index 594070c..653d0b3 100644 --- a/trees/isa/isa-001M.tree +++ b/trees/isa/isa-001M.tree @@ -5,7 +5,7 @@ \parent{isa-001B} \taxon{Example} \put\shiki/language{Isabelle Theory} -\shiki{lemma ‹f (f (f (b::two))) = f b›} +\shiki{lemma lm001M: ‹f (f (f (b::two))) = f b›} \solnblock{ \shiki{apply (case_tac b) apply simp diff --git a/trees/isa/isa-001N.tree b/trees/isa/isa-001N.tree new file mode 100644 index 0000000..0030da8 --- /dev/null +++ b/trees/isa/isa-001N.tree @@ -0,0 +1,7 @@ +\date{2025-12-03T02:35:03Z} +\title{Natural numbers in Isabelle} +\author{liamoc} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\p{Isabelle/HOL's [theory of natural numbers](https://isabelle.in.tum.de/library/HOL/HOL/Nat.html) defines natural numbers in a different way, but they behave much as if they were defined with [the \code{datatype} command](isa-001K). } +\shiki{datatype nat = 0 | Suc "nat"} diff --git a/trees/isa/isa-001O.tree b/trees/isa/isa-001O.tree new file mode 100644 index 0000000..10a8d15 --- /dev/null +++ b/trees/isa/isa-001O.tree @@ -0,0 +1,23 @@ +\date{2025-12-03T02:48:14Z} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\title{Defining functions in Isabelle} +\p{The \code{fun} command can be used to define functions in Isabelle. Unlike [\code{definition}s](isa-001G), functions can be defined by \em{multiple} pattern-matching equations, they may be recursive, and their equations are automatically added to [the simpset](isa-001H).} +\subtree{\taxon{Example}\title{Fibonacci as a \code{fun}}\author{liamoc} +\shiki{fun fib :: "nat ⇒ nat" where + "fib 0 = 0" +| "fib (Suc 0) = Suc 0" +| "fib (Suc (Suc n)) = fib n + fib (Suc n)" +print_theorems} +} +\p{The \code{print_theorems} command allows us to see all of the lemmas generated by this command. +} +\problemblock{ + \p{Isabelle functions must provably terminate. The problem with non-terminating functions can be illustrated by a definition like:} + \shiki{fun bad :: "nat ⇒ bool" where "bad x = ¬ (bad x)"} + \p{If such a non-terminating definition were allowed, this would render our logic inconsistent (as \code{bad x} is equal to its own negation). Therefore, Isabelle requires that all functions be accompanied by a proof of termination.} + \p{The \code{fun} command attempts to prove termination automatically. If it does not succeed, it will give an error message and fail to define the function. Manual proofs of termination can be supplied if the \code{function} command is used instead, but the \code{function} command is beyond the scope of this course. } +} +\p{In cases where the recursion and pattern matching follows exactly the structure of the datatype in one argument, \code{primrec} can be used instead of \code{fun}, which is a bit more efficient:} +\transclude{isa-001R} \ No newline at end of file diff --git a/trees/isa/isa-001P.tree b/trees/isa/isa-001P.tree new file mode 100644 index 0000000..4034dd4 --- /dev/null +++ b/trees/isa/isa-001P.tree @@ -0,0 +1,8 @@ +\date{2025-12-03T03:46:57Z} +\author{liamoc} +\taxon{Proof Method} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{\code{induct} (for structural induction)} +\p{While it is possible to use \code{rule} or \code{erule} with the generated \code{.induct} theorem from a [\code{datatype}](isa-001K), it is usually much simpler and more convenient to use the \code{induct} proof method. Similar to the [[isa-001L]] method, \code{apply (induct t)} splits the goal into various cases, one for each constructor of the type of \code{t}. The difference is that for recursive cases of the datatype, we also get an \em{inductive hypothesis} added to our assumptions.} +\transclude{isa-001Q} diff --git a/trees/isa/isa-001Q.tree b/trees/isa/isa-001Q.tree new file mode 100644 index 0000000..94536a3 --- /dev/null +++ b/trees/isa/isa-001Q.tree @@ -0,0 +1,17 @@ +\date{2025-12-03T03:55:36Z} +\author{liamoc} +\taxon{Example} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\p{We can prove a theorem about our [factorial definition](isa-001R):} +\shiki{theorem factorial_mult: "factorial n * factorial m ≤ factorial (n + m)"} +\solnblock{ +\shiki{apply (induct n) + apply simp +apply (simp only: factorial.simps add_Suc mult.assoc) +apply (rule mult_le_mono) + apply simp +apply simp +done} +} \ No newline at end of file diff --git a/trees/isa/isa-001R.tree b/trees/isa/isa-001R.tree new file mode 100644 index 0000000..7c7f964 --- /dev/null +++ b/trees/isa/isa-001R.tree @@ -0,0 +1,10 @@ +\date{2025-12-03T03:55:43Z} +\taxon{Example} +\title{Factorial as a \code{primrec}} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\shiki{primrec factorial :: "nat ⇒ nat" where + "factorial 0 = Suc 0" +| "factorial (Suc n) = Suc n * factorial n" +print_theorems} \ No newline at end of file diff --git a/trees/isa/isa-001S.tree b/trees/isa/isa-001S.tree new file mode 100644 index 0000000..836eb00 --- /dev/null +++ b/trees/isa/isa-001S.tree @@ -0,0 +1,10 @@ +\date{2025-12-03T04:05:58Z} +\taxon{Example} +\author{liamoc} +\title{Higher-order functions} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\shiki{primrec rpt :: ‹('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a› where + ‹rpt f 0 x = x › +| ‹rpt f (Suc n) x = f (rpt f n x)›} +\p{The above function is given \em{another function} as an input.} \ No newline at end of file diff --git a/trees/isa/isa-001T.tree b/trees/isa/isa-001T.tree new file mode 100644 index 0000000..dfcd545 --- /dev/null +++ b/trees/isa/isa-001T.tree @@ -0,0 +1,19 @@ +\date{2025-12-03T04:10:30Z} +\author{liamoc} +\taxon{Exercise} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\import{dt-macros} +\parent{isa-001B} +\shiki{definition twice :: ‹('a ⇒ 'a) ⇒ 'a ⇒ 'a› where +‹twice f x = f (f x)›} +\shiki{lemma ‹rpt (twice f) n (f (x::two)) = f x›} +\solnblock{ +\shiki{apply (unfold twice_def) +apply (induct n) + apply simp +apply simp +apply (rule lm001M) +done} +\p{Using the lemma from \ref{isa-001M}.} +} \ No newline at end of file diff --git a/trees/isa/isa-001U.tree b/trees/isa/isa-001U.tree new file mode 100644 index 0000000..d6ab93b --- /dev/null +++ b/trees/isa/isa-001U.tree @@ -0,0 +1,12 @@ +\date{2025-12-03T04:29:49Z} +\author{liamoc} +\taxon{Definition} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\parent{isa-001B} +\title{The \code{oots} type} +\shiki{datatype oots = + ONEs "nat" "oots" + | TWOs "nat" "oots" + | Empty} +\p{This type encodes a sequence of [\code{oot}](isa-001J) values. For example, the value \code{ONEs 3 (TWOs 2 (ONEs 1 Empty))} encodes the sequence \code{[ONE, ONE, ONE, TWO, TWO, ONE]}. } diff --git a/trees/isa/isa-001V.tree b/trees/isa/isa-001V.tree new file mode 100644 index 0000000..45fc751 --- /dev/null +++ b/trees/isa/isa-001V.tree @@ -0,0 +1,14 @@ +\date{2025-12-03T04:41:52Z} +\author{liamoc} +\taxon{Definition} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\parent{isa-001B} +\title{The \code{prepend} function} +\shiki{fun prepend :: ‹oot ⇒ nat ⇒ oots ⇒ oots› where + ‹prepend ONE n Empty = ONEs n Empty› +| ‹prepend TWO n Empty = TWOs n Empty› +| ‹prepend ONE n (TWOs m r) = ONEs n (TWOs m r)› +| ‹prepend TWO n (ONEs m r) = TWOs n (ONEs m r)› +| ‹prepend ONE n (ONEs m r) = ONEs (n+m) r› +| ‹prepend TWO n (TWOs m r) = TWOs (n+m) r›} \ No newline at end of file diff --git a/trees/isa/isa-001W.tree b/trees/isa/isa-001W.tree new file mode 100644 index 0000000..869f032 --- /dev/null +++ b/trees/isa/isa-001W.tree @@ -0,0 +1,21 @@ +\date{2025-12-03T04:45:13Z} +\taxon{Theorem} +\import{dt-macros} +\import{shiki-macros} +\author{liamoc} +\title{\code{prepend_prepend}} +\parent{isa-001B} +\put\shiki/language{Isabelle Theory} +\shiki{lemma prepend_prepend: ‹prepend s n (prepend s m r) = prepend s (n + m) r›} +\solnblock{ +\shiki{apply (case_tac s) + apply simp + apply (case_tac r) + apply simp + apply simp + apply simp + apply (case_tac r) + apply simp + apply simp +apply simp +done}} \ No newline at end of file diff --git a/trees/isa/isa-001X.tree b/trees/isa/isa-001X.tree new file mode 100644 index 0000000..a89d44c --- /dev/null +++ b/trees/isa/isa-001X.tree @@ -0,0 +1,9 @@ +\date{2025-12-03T04:52:32Z} +\author{liamoc} +\title{Combining methods with semicolons} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\p{Methods can be combined using the \code{;} operator:} +\shiki{apply (m1; m2)} +\p{This applies \code{m2} to \em{every subgoal} that results from applying \code{m1} to the current goal. It can be chained together multiple times. For example, the entire proof of \ref{isa-001W} can be much more succinctly expressed as one line:} +\shiki{by (case_tac s; case_tac r; simp)} \ No newline at end of file diff --git a/trees/isa/isa-001Y.tree b/trees/isa/isa-001Y.tree new file mode 100644 index 0000000..002b249 --- /dev/null +++ b/trees/isa/isa-001Y.tree @@ -0,0 +1,13 @@ +\date{2025-12-03T04:58:18Z} +\author{liamoc} +\taxon{Definition} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\parent{isa-001B} +\title{The \code{cat} function} +\shiki{fun cat :: ‹oots ⇒ oots ⇒ oots› where + ‹cat (ONEs n xs) ys = prepend ONE n (cat xs ys)› +| ‹cat (TWOs n xs) ys = prepend TWO n (cat xs ys)› +| ‹cat Empty ys = ys› +} +\p{This function uses [the \code{prepend} function](isa-001V) to concatenate two \code{oots} sequences together.} \ No newline at end of file diff --git a/trees/isa/isa-001Z.tree b/trees/isa/isa-001Z.tree new file mode 100644 index 0000000..104d0bc --- /dev/null +++ b/trees/isa/isa-001Z.tree @@ -0,0 +1,11 @@ +\date{2025-12-03T05:07:08Z} +\author{liamoc} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\parent{isa-001B} +\title{\code{cat_prepend}} +\shiki{lemma cat_prepend: ‹cat (prepend s n x) y = prepend s n (cat x y)›} +\solnblock{ + \shiki{by (case_tac s; case_tac x; simp add: prepend_prepend)}} diff --git a/trees/isa/isa-0020.tree b/trees/isa/isa-0020.tree new file mode 100644 index 0000000..eb5acbf --- /dev/null +++ b/trees/isa/isa-0020.tree @@ -0,0 +1,11 @@ +\date{2025-12-03T05:09:52Z} +\author{liamoc} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\parent{isa-001B} +\title{\code{cat_assoc}} +\shiki{lemma cat_assoc: ‹cat x (cat y z) = cat (cat x y) z›} +\solnblock{\shiki{by (induct x;simp add: cat_prepend)}} + diff --git a/trees/isa/isa-0021.tree b/trees/isa/isa-0021.tree new file mode 100644 index 0000000..11bda18 --- /dev/null +++ b/trees/isa/isa-0021.tree @@ -0,0 +1,15 @@ +\date{2025-12-03T05:16:30Z} +\author{liamoc} +\title{Lists in Isabelle} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\p{The Isabelle/HOL [theory of Lists](https://isabelle.in.tum.de/library/HOL/HOL/List.html) defines lists as follows:} +\shiki{datatype 'a list = Nil | Cons "'a" "'a list" } +\p{This is an example of a \em{polymorphic} data type, where the type variable \code{'a} stands for a type. For example, the type \code{nat list} is the type of lists of \code{nat}, and \code{oot list} is the type of a list of [\code{oot}s](isa-001J). } +\p{The notation \code{x#xs} is syntax sugar for \code{Cons x xs} and \code{[]} is syntax sugar for \code{Nil}. Lists can also be written in square brackets, so:} +\shiki{[1,2,3]} +\p{is equivalent to:} +\shiki{1 # 2 # 3 # []} +\p{which is equivalent to:} +\shiki{Cons 1 (Cons 2 (Cons 3 Nil))} +\p{Some provided functions are useful, including \code{replicate :: nat ⇒ 'a ⇒ 'a list}, which produces a list of #{n} copies of the given value, and \code{append :: 'a list ⇒ 'a list ⇒ 'a list} which joins two lists together into one. The \code{append} function also has special notation, so \code{a @ b} is equivalent to \code{append a b}} \ No newline at end of file diff --git a/trees/isa/isa-0022.tree b/trees/isa/isa-0022.tree new file mode 100644 index 0000000..7e394b5 --- /dev/null +++ b/trees/isa/isa-0022.tree @@ -0,0 +1,11 @@ +\date{2025-12-03T05:29:25Z} +\taxon{Definition} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{The \code{expand} function} +\shiki{primrec expand :: ‹oots ⇒ oot list› where + ‹expand (ONEs n r) = replicate n ONE @ expand r› +| ‹expand (TWOs n r) = replicate n TWO @ expand r› +| ‹expand Empty = []›} diff --git a/trees/isa/isa-0023.tree b/trees/isa/isa-0023.tree new file mode 100644 index 0000000..ba7512b --- /dev/null +++ b/trees/isa/isa-0023.tree @@ -0,0 +1,10 @@ +\date{2025-12-03T05:29:25Z} +\taxon{Definition} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{The \code{compress} function} +\shiki{primrec compress :: ‹oot list ⇒ oots› where + ‹compress [] = Empty› +| ‹compress (x#xs) = prepend x 1 (compress xs)›} diff --git a/trees/isa/isa-0024.tree b/trees/isa/isa-0024.tree new file mode 100644 index 0000000..4fbfb82 --- /dev/null +++ b/trees/isa/isa-0024.tree @@ -0,0 +1,10 @@ +\date{2025-12-03T05:29:25Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{\code{expand_prepend}} +\shiki{lemma expand_prepend: ‹expand (prepend x n r) = replicate n x @ expand r›} +\solnblock{\shiki{by (case_tac r; case_tac x; simp add: replicate_add)}} diff --git a/trees/isa/isa-0025.tree b/trees/isa/isa-0025.tree new file mode 100644 index 0000000..253fc4e --- /dev/null +++ b/trees/isa/isa-0025.tree @@ -0,0 +1,10 @@ +\date{2025-12-03T05:29:25Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{\code{expand_compress}} +\shiki{lemma expand_compress: ‹expand (compress xs) = xs›} +\solnblock{\shiki{by (induct xs;simp add: expand_prepend)}} diff --git a/trees/isa/isa-0026.tree b/trees/isa/isa-0026.tree new file mode 100644 index 0000000..2d64399 --- /dev/null +++ b/trees/isa/isa-0026.tree @@ -0,0 +1,10 @@ +\date{2025-12-03T05:29:25Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{\code{compress_append}} +\shiki{lemma compress_append: ‹compress (xs @ ys) = cat (compress xs) (compress ys)›} +\solnblock{\shiki{by (induct xs; simp add: cat_prepend)}} diff --git a/trees/isa/isa-0027.tree b/trees/isa/isa-0027.tree new file mode 100644 index 0000000..1e36d76 --- /dev/null +++ b/trees/isa/isa-0027.tree @@ -0,0 +1,16 @@ +\date{2025-12-03T05:29:25Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{\code{compress_replicate} lemmas} +\shiki{lemma compress_replicate_ONE: ‹n > 0 ⟹ compress (replicate n ONE) = ONEs n Empty›} +\solnblock{\shiki{apply (induct n; simp) +apply (case_tac "n > 0"; simp) +done}}\p{} +\shiki{lemma compress_replicate_TWO: ‹n > 0 ⟹ compress (replicate n TWO) = TWOs n Empty›} +\solnblock{\shiki{apply (induct n; simp) +apply (case_tac "n > 0"; simp) +done}} \ No newline at end of file diff --git a/trees/isa/isa-0028.tree b/trees/isa/isa-0028.tree new file mode 100644 index 0000000..b15ae5d --- /dev/null +++ b/trees/isa/isa-0028.tree @@ -0,0 +1,4 @@ +\date{2025-12-03T06:13:19Z} +\author{liamoc} +\title{\code{inductive} predicates} +\p{TODO} \ No newline at end of file diff --git a/trees/isa/isa-0029.tree b/trees/isa/isa-0029.tree new file mode 100644 index 0000000..6442863 --- /dev/null +++ b/trees/isa/isa-0029.tree @@ -0,0 +1,5 @@ +\date{2025-12-03T06:14:12Z} +\author{liamoc} +\taxon{Proof Method} +\title{\code{induct} (for rule induction)} +\p{TODO} \ No newline at end of file diff --git a/trees/isa/isa-002A.tree b/trees/isa/isa-002A.tree new file mode 100644 index 0000000..b4ffd87 --- /dev/null +++ b/trees/isa/isa-002A.tree @@ -0,0 +1,13 @@ +\date{2025-12-03T06:15:34Z} +\author{liamoc} +\taxon{Example} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{Wellformedness for \code{oots}} +\p{We define \code{well}, an inductive wellformedness predicate for \code{oots} sequences, that state there are no segments of zero length, and that no two adjacent segments have the same \code{oot} value.} +\shiki{inductive well :: ‹oots ⇒ bool› where + ‹well Empty› +| ‹n > 0 ⟹ well (ONEs n Empty)› +| ‹n > 0 ⟹ well (TWOs n Empty)› +| ‹n > 0 ⟹ well (ONEs m r) ⟹ well (TWOs n (ONEs m r))› +| ‹n > 0 ⟹ well (TWOs m r) ⟹ well (ONEs n (TWOs m r))›} \ No newline at end of file diff --git a/trees/isa/isa-002B.tree b/trees/isa/isa-002B.tree new file mode 100644 index 0000000..1bccece --- /dev/null +++ b/trees/isa/isa-002B.tree @@ -0,0 +1,20 @@ +\date{2025-12-03T06:23:23Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{\code{compress_expand}} +\shiki{lemma compress_expand:‹well s ⟹ compress (expand s) = s›} +\solnblock{\shiki{apply (induct rule: well.induct) + apply simp + apply (simp add: compress_replicate_ONE) + apply (simp add: compress_replicate_TWO) + apply (simp add: compress_replicate_ONE + compress_replicate_TWO + compress_app) +apply (simp add: compress_replicate_ONE + compress_replicate_TWO + compress_app) +done}} diff --git a/trees/isa/isa-002C.tree b/trees/isa/isa-002C.tree new file mode 100644 index 0000000..cbcf32b --- /dev/null +++ b/trees/isa/isa-002C.tree @@ -0,0 +1,11 @@ +\date{2025-12-03T06:30:43Z} +\author{liamoc} +\taxon{Definition} +\parent{isa-001B} +\import{shiki-macros} +\put\shiki/language{Isabelle Theory} +\title{List subsequence relation} +\shiki{inductive subsequence :: ‹'a list ⇒ 'a list ⇒ bool› where + ss_empty: ‹subsequence [] []› +| ss_keep: ‹subsequence xs ys ⟹ subsequence (x#xs) (x#ys)› +| ss_drop: ‹subsequence xs ys ⟹ subsequence xs (y#ys)›} \ No newline at end of file diff --git a/trees/isa/isa-002D.tree b/trees/isa/isa-002D.tree new file mode 100644 index 0000000..b1e09e9 --- /dev/null +++ b/trees/isa/isa-002D.tree @@ -0,0 +1,14 @@ +\date{2025-12-03T06:34:53Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{Reflexivity of \code{subsequence}} +\shiki{lemma ss_refl: ‹subsequence ls ls›} +\solnblock{\shiki{apply (induct ls) + apply (rule ss_empty) +apply (rule ss_keep) +apply assumption +done}} diff --git a/trees/isa/isa-002E.tree b/trees/isa/isa-002E.tree new file mode 100644 index 0000000..0aab6da --- /dev/null +++ b/trees/isa/isa-002E.tree @@ -0,0 +1,14 @@ +\date{2025-12-03T06:40:22Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{Length of \code{subsequence}} +\shiki{lemma ss_length : ‹subsequence xs ys ⟹ length xs ≤ length ys›} +\solnblock{\shiki{apply (induct rule: subsequence.induct) + apply simp + apply simp +apply simp +done}} diff --git a/trees/isa/isa-002F.tree b/trees/isa/isa-002F.tree new file mode 100644 index 0000000..0aac458 --- /dev/null +++ b/trees/isa/isa-002F.tree @@ -0,0 +1,4 @@ +\date{2025-12-03T06:41:41Z} +\title{Controlling backtracking, chaining methods with comma} +\author{liamoc} +\p{TODO} \ No newline at end of file diff --git a/trees/isa/isa-002G.tree b/trees/isa/isa-002G.tree new file mode 100644 index 0000000..dfe69ed --- /dev/null +++ b/trees/isa/isa-002G.tree @@ -0,0 +1,4 @@ +\date{2025-12-03T06:42:16Z} +\title{Repeating methods with \code{+}} +\author{liamoc} +\p{TODO} diff --git a/trees/isa/isa-002H.tree b/trees/isa/isa-002H.tree new file mode 100644 index 0000000..78765a8 --- /dev/null +++ b/trees/isa/isa-002H.tree @@ -0,0 +1,20 @@ +\date{2025-12-03T06:43:34Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{Antisymmetry of \code{subsequence}} +\shiki{lemma ss_antisym: ‹subsequence ys xs ⟹ subsequence xs ys ⟹ xs = ys›} +\solnblock{\shiki{apply (induct rule: subsequence.induct) + apply simp + apply simp + apply (erule subsequence.cases, clarsimp, clarsimp,clarsimp) + apply (drule ss_length)+ + apply simp + apply (drule ss_length)+ +apply simp +done}} + + diff --git a/trees/isa/isa-002I.tree b/trees/isa/isa-002I.tree new file mode 100644 index 0000000..18fc726 --- /dev/null +++ b/trees/isa/isa-002I.tree @@ -0,0 +1,4 @@ +\date{2025-12-03T06:48:06Z} +\author{liamoc} +\title{Generalising the induction hypothesis with \code{arbitrary}} +\p{TODO} \ No newline at end of file diff --git a/trees/isa/isa-002J.tree b/trees/isa/isa-002J.tree new file mode 100644 index 0000000..e89e1e3 --- /dev/null +++ b/trees/isa/isa-002J.tree @@ -0,0 +1,42 @@ +\date{2025-12-03T06:48:59Z} +\taxon{Theorem} +\import{shiki-macros} +\import{dt-macros} +\put\shiki/language{Isabelle Theory} +\author{liamoc} +\parent{isa-001B} +\title{Transitivity of \code{subsequence}} +\shiki{lemma ss_trans: ‹subsequence ys zs ⟹ subsequence xs ys ⟹ subsequence xs zs›} +\solnblock{\shiki{apply (induct ys zs arbitrary: xs rule: subsequence.induct) + apply simp + apply (erule subsequence.cases) + apply simp + apply clarsimp + + apply (erule subsequence.cases) + apply simp + apply clarsimp + apply (rule ss_keep) + apply simp + apply simp + apply clarsimp + apply (rule ss_drop) + apply simp + apply simp + apply clarsimp + + apply (erule subsequence.cases) + apply clarsimp + apply clarsimp + apply (rule ss_keep) + apply clarsimp + apply clarsimp + apply (rule ss_drop) + apply clarsimp +apply (rule ss_drop) +apply simp +done}} + + + + -- 2.51.2