my forest
isa: more notes
+465
-33
+31
-28
trees/isa/isa-001B.tree
+31
-28
trees/isa/isa-001B.tree
···
32
32
\transclude{isa-001J}
33
33
\transclude{isa-001L}
34
34
\transclude{isa-001M}
35
+
\transclude{isa-001N}
36
+
\transclude{isa-001O}
37
+
\transclude{isa-001P}
38
+
\transclude{isa-001S}
39
+
\transclude{isa-001T}
40
+
\transclude{isa-001U}
41
+
\transclude{isa-001V}
42
+
\transclude{isa-001W}
43
+
\transclude{isa-001X}
44
+
\transclude{isa-001Y}
45
+
\transclude{isa-001Z}
46
+
\transclude{isa-0021}
47
+
\transclude{isa-0022}
48
+
\transclude{isa-0024}
49
+
\transclude{isa-0023}
50
+
\transclude{isa-0025}
51
+
\transclude{isa-0026}
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}
35
65
\ul{
36
-
\li{natural numbers}
37
-
\li{Fun command}
38
-
\li{rpt}
39
-
\li{induct method (structural)}
40
-
\li{rpt twice theorem}
41
-
\li{twos type}
42
-
\li{prepend}
43
-
\li{prepend prepend theorem}
44
-
\li{semicolon operator}
45
-
\li{append}
46
-
\li{append prepend theorem}
47
-
\li{append assoc}
48
-
\li{lists (replicate function)}
49
-
\li{decompress}
50
-
\li{compress}
51
-
\li{decompress compress thm}
52
-
\li{compress app}
53
-
\li{compress replicate}
54
-
\li{inductive predicates}
55
-
\li{rule induction}
56
-
\li{wellformedness}
57
-
\li{compress decompress thm}
58
-
\li{arbitrary}
59
-
\li{chaining}
60
-
\li{repeating}
61
-
\li{subsequence example}
62
-
\li{subsequence theorems}
63
66
\li{safe vs unsafe rules}
64
-
\li{intro, elim, clarify, blast, (fast,slow,best)}}
67
+
\li{intro, elim, clarify, blast, (fast,slow,best)}
65
68
\li{automation: clarsimp, auto, fastforce (slowsimp, bestsimp), force}
66
69
\li{sledgehammer, try, find_theorems}
67
70
\li{clarify, clarsimp}
+3
-3
trees/isa/isa-001J.tree
+3
-3
trees/isa/isa-001J.tree
···
3
3
\parent{isa-001B}
4
4
\import{shiki-macros}
5
5
\put\shiki/language{Isabelle Theory}
6
-
\title{The \code{two} type}
7
-
\shiki{datatype two = ONE | TWO
6
+
\title{The \code{oot} type}
7
+
\shiki{datatype oot = ONE | TWO
8
8
print_theorems
9
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
+
\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}) }
+8
-1
trees/isa/isa-001K.tree
+8
-1
trees/isa/isa-001K.tree
···
1
1
\date{2025-12-02T12:59:55Z}
2
2
\title{The \code{datatype} command}
3
+
\author{liamoc}
3
4
\import{shiki-macros}
4
5
\put\shiki/language{Isabelle Theory}
5
6
\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
8
| Constructor2 (* ... *)
8
9
(* ... *)
9
10
}
10
-
\p{These datatypes are analogous to the algebraic data types found in many functional programming languages.}
11
+
\p{These datatypes are analogous to the algebraic data types found in many functional programming languages.}
12
+
\p{The \code{datatype} command automatically proves many lemmas about these types for you, chiefly:}
13
+
\ul{
14
+
\li{Disjointness: Values made with one constructor are not equal to values made with another constructor.}
15
+
\li{Exhaustivity: The only values of this type are those made by the listed constructors.}
16
+
\li{Injectivity: Two values of the same constructor are equal iff their arguments are equal.}
17
+
}
+1
-1
trees/isa/isa-001M.tree
+1
-1
trees/isa/isa-001M.tree
+7
trees/isa/isa-001N.tree
+7
trees/isa/isa-001N.tree
···
1
+
\date{2025-12-03T02:35:03Z}
2
+
\title{Natural numbers in Isabelle}
3
+
\author{liamoc}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\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). }
7
+
\shiki{datatype nat = 0 | Suc "nat"}
+23
trees/isa/isa-001O.tree
+23
trees/isa/isa-001O.tree
···
1
+
\date{2025-12-03T02:48:14Z}
2
+
\import{shiki-macros}
3
+
\import{dt-macros}
4
+
\put\shiki/language{Isabelle Theory}
5
+
\title{Defining functions in Isabelle}
6
+
\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).}
7
+
\subtree{\taxon{Example}\title{Fibonacci as a \code{fun}}\author{liamoc}
8
+
\shiki{fun fib :: "nat ⇒ nat" where
9
+
"fib 0 = 0"
10
+
| "fib (Suc 0) = Suc 0"
11
+
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
12
+
print_theorems}
13
+
}
14
+
\p{The \code{print_theorems} command allows us to see all of the lemmas generated by this command.
15
+
}
16
+
\problemblock{
17
+
\p{Isabelle functions must provably terminate. The problem with non-terminating functions can be illustrated by a definition like:}
18
+
\shiki{fun bad :: "nat ⇒ bool" where "bad x = ¬ (bad x)"}
19
+
\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.}
20
+
\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. }
21
+
}
22
+
\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:}
23
+
\transclude{isa-001R}
+8
trees/isa/isa-001P.tree
+8
trees/isa/isa-001P.tree
···
1
+
\date{2025-12-03T03:46:57Z}
2
+
\author{liamoc}
3
+
\taxon{Proof Method}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\title{\code{induct} (for structural induction)}
7
+
\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.}
8
+
\transclude{isa-001Q}
+17
trees/isa/isa-001Q.tree
+17
trees/isa/isa-001Q.tree
···
1
+
\date{2025-12-03T03:55:36Z}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\import{shiki-macros}
5
+
\import{dt-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\p{We can prove a theorem about our [factorial definition](isa-001R):}
8
+
\shiki{theorem factorial_mult: "factorial n * factorial m ≤ factorial (n + m)"}
9
+
\solnblock{
10
+
\shiki{apply (induct n)
11
+
apply simp
12
+
apply (simp only: factorial.simps add_Suc mult.assoc)
13
+
apply (rule mult_le_mono)
14
+
apply simp
15
+
apply simp
16
+
done}
17
+
}
+10
trees/isa/isa-001R.tree
+10
trees/isa/isa-001R.tree
···
1
+
\date{2025-12-03T03:55:43Z}
2
+
\taxon{Example}
3
+
\title{Factorial as a \code{primrec}}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\shiki{primrec factorial :: "nat ⇒ nat" where
8
+
"factorial 0 = Suc 0"
9
+
| "factorial (Suc n) = Suc n * factorial n"
10
+
print_theorems}
+10
trees/isa/isa-001S.tree
+10
trees/isa/isa-001S.tree
···
1
+
\date{2025-12-03T04:05:58Z}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\title{Higher-order functions}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\shiki{primrec rpt :: ‹('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a› where
8
+
‹rpt f 0 x = x ›
9
+
| ‹rpt f (Suc n) x = f (rpt f n x)›}
10
+
\p{The above function is given \em{another function} as an input.}
+19
trees/isa/isa-001T.tree
+19
trees/isa/isa-001T.tree
···
1
+
\date{2025-12-03T04:10:30Z}
2
+
\author{liamoc}
3
+
\taxon{Exercise}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\import{dt-macros}
7
+
\parent{isa-001B}
8
+
\shiki{definition twice :: ‹('a ⇒ 'a) ⇒ 'a ⇒ 'a› where
9
+
‹twice f x = f (f x)›}
10
+
\shiki{lemma ‹rpt (twice f) n (f (x::two)) = f x›}
11
+
\solnblock{
12
+
\shiki{apply (unfold twice_def)
13
+
apply (induct n)
14
+
apply simp
15
+
apply simp
16
+
apply (rule lm001M)
17
+
done}
18
+
\p{Using the lemma from \ref{isa-001M}.}
19
+
}
+12
trees/isa/isa-001U.tree
+12
trees/isa/isa-001U.tree
···
1
+
\date{2025-12-03T04:29:49Z}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\parent{isa-001B}
7
+
\title{The \code{oots} type}
8
+
\shiki{datatype oots =
9
+
ONEs "nat" "oots"
10
+
| TWOs "nat" "oots"
11
+
| Empty}
12
+
\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]}. }
+14
trees/isa/isa-001V.tree
+14
trees/isa/isa-001V.tree
···
1
+
\date{2025-12-03T04:41:52Z}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\parent{isa-001B}
7
+
\title{The \code{prepend} function}
8
+
\shiki{fun prepend :: ‹oot ⇒ nat ⇒ oots ⇒ oots› where
9
+
‹prepend ONE n Empty = ONEs n Empty›
10
+
| ‹prepend TWO n Empty = TWOs n Empty›
11
+
| ‹prepend ONE n (TWOs m r) = ONEs n (TWOs m r)›
12
+
| ‹prepend TWO n (ONEs m r) = TWOs n (ONEs m r)›
13
+
| ‹prepend ONE n (ONEs m r) = ONEs (n+m) r›
14
+
| ‹prepend TWO n (TWOs m r) = TWOs (n+m) r›}
+21
trees/isa/isa-001W.tree
+21
trees/isa/isa-001W.tree
···
1
+
\date{2025-12-03T04:45:13Z}
2
+
\taxon{Theorem}
3
+
\import{dt-macros}
4
+
\import{shiki-macros}
5
+
\author{liamoc}
6
+
\title{\code{prepend_prepend}}
7
+
\parent{isa-001B}
8
+
\put\shiki/language{Isabelle Theory}
9
+
\shiki{lemma prepend_prepend: ‹prepend s n (prepend s m r) = prepend s (n + m) r›}
10
+
\solnblock{
11
+
\shiki{apply (case_tac s)
12
+
apply simp
13
+
apply (case_tac r)
14
+
apply simp
15
+
apply simp
16
+
apply simp
17
+
apply (case_tac r)
18
+
apply simp
19
+
apply simp
20
+
apply simp
21
+
done}}
+9
trees/isa/isa-001X.tree
+9
trees/isa/isa-001X.tree
···
1
+
\date{2025-12-03T04:52:32Z}
2
+
\author{liamoc}
3
+
\title{Combining methods with semicolons}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\p{Methods can be combined using the \code{;} operator:}
7
+
\shiki{apply (m1; m2)}
8
+
\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:}
9
+
\shiki{by (case_tac s; case_tac r; simp)}
+13
trees/isa/isa-001Y.tree
+13
trees/isa/isa-001Y.tree
···
1
+
\date{2025-12-03T04:58:18Z}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\parent{isa-001B}
7
+
\title{The \code{cat} function}
8
+
\shiki{fun cat :: ‹oots ⇒ oots ⇒ oots› where
9
+
‹cat (ONEs n xs) ys = prepend ONE n (cat xs ys)›
10
+
| ‹cat (TWOs n xs) ys = prepend TWO n (cat xs ys)›
11
+
| ‹cat Empty ys = ys›
12
+
}
13
+
\p{This function uses [the \code{prepend} function](isa-001V) to concatenate two \code{oots} sequences together.}
+11
trees/isa/isa-001Z.tree
+11
trees/isa/isa-001Z.tree
···
1
+
\date{2025-12-03T05:07:08Z}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\import{shiki-macros}
5
+
\import{dt-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\parent{isa-001B}
8
+
\title{\code{cat_prepend}}
9
+
\shiki{lemma cat_prepend: ‹cat (prepend s n x) y = prepend s n (cat x y)›}
10
+
\solnblock{
11
+
\shiki{by (case_tac s; case_tac x; simp add: prepend_prepend)}}
+11
trees/isa/isa-0020.tree
+11
trees/isa/isa-0020.tree
···
1
+
\date{2025-12-03T05:09:52Z}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\import{shiki-macros}
5
+
\import{dt-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\parent{isa-001B}
8
+
\title{\code{cat_assoc}}
9
+
\shiki{lemma cat_assoc: ‹cat x (cat y z) = cat (cat x y) z›}
10
+
\solnblock{\shiki{by (induct x;simp add: cat_prepend)}}
11
+
+15
trees/isa/isa-0021.tree
+15
trees/isa/isa-0021.tree
···
1
+
\date{2025-12-03T05:16:30Z}
2
+
\author{liamoc}
3
+
\title{Lists in Isabelle}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\p{The Isabelle/HOL [theory of Lists](https://isabelle.in.tum.de/library/HOL/HOL/List.html) defines lists as follows:}
7
+
\shiki{datatype 'a list = Nil | Cons "'a" "'a list" }
8
+
\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). }
9
+
\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:}
10
+
\shiki{[1,2,3]}
11
+
\p{is equivalent to:}
12
+
\shiki{1 # 2 # 3 # []}
13
+
\p{which is equivalent to:}
14
+
\shiki{Cons 1 (Cons 2 (Cons 3 Nil))}
15
+
\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}}
+11
trees/isa/isa-0022.tree
+11
trees/isa/isa-0022.tree
···
1
+
\date{2025-12-03T05:29:25Z}
2
+
\taxon{Definition}
3
+
\import{shiki-macros}
4
+
\put\shiki/language{Isabelle Theory}
5
+
\author{liamoc}
6
+
\parent{isa-001B}
7
+
\title{The \code{expand} function}
8
+
\shiki{primrec expand :: ‹oots ⇒ oot list› where
9
+
‹expand (ONEs n r) = replicate n ONE @ expand r›
10
+
| ‹expand (TWOs n r) = replicate n TWO @ expand r›
11
+
| ‹expand Empty = []›}
+10
trees/isa/isa-0023.tree
+10
trees/isa/isa-0023.tree
···
1
+
\date{2025-12-03T05:29:25Z}
2
+
\taxon{Definition}
3
+
\import{shiki-macros}
4
+
\put\shiki/language{Isabelle Theory}
5
+
\author{liamoc}
6
+
\parent{isa-001B}
7
+
\title{The \code{compress} function}
8
+
\shiki{primrec compress :: ‹oot list ⇒ oots› where
9
+
‹compress [] = Empty›
10
+
| ‹compress (x#xs) = prepend x 1 (compress xs)›}
+10
trees/isa/isa-0024.tree
+10
trees/isa/isa-0024.tree
···
1
+
\date{2025-12-03T05:29:25Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{\code{expand_prepend}}
9
+
\shiki{lemma expand_prepend: ‹expand (prepend x n r) = replicate n x @ expand r›}
10
+
\solnblock{\shiki{by (case_tac r; case_tac x; simp add: replicate_add)}}
+10
trees/isa/isa-0025.tree
+10
trees/isa/isa-0025.tree
···
1
+
\date{2025-12-03T05:29:25Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{\code{expand_compress}}
9
+
\shiki{lemma expand_compress: ‹expand (compress xs) = xs›}
10
+
\solnblock{\shiki{by (induct xs;simp add: expand_prepend)}}
+10
trees/isa/isa-0026.tree
+10
trees/isa/isa-0026.tree
···
1
+
\date{2025-12-03T05:29:25Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{\code{compress_append}}
9
+
\shiki{lemma compress_append: ‹compress (xs @ ys) = cat (compress xs) (compress ys)›}
10
+
\solnblock{\shiki{by (induct xs; simp add: cat_prepend)}}
+16
trees/isa/isa-0027.tree
+16
trees/isa/isa-0027.tree
···
1
+
\date{2025-12-03T05:29:25Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{\code{compress_replicate} lemmas}
9
+
\shiki{lemma compress_replicate_ONE: ‹n > 0 ⟹ compress (replicate n ONE) = ONEs n Empty›}
10
+
\solnblock{\shiki{apply (induct n; simp)
11
+
apply (case_tac "n > 0"; simp)
12
+
done}}\p{}
13
+
\shiki{lemma compress_replicate_TWO: ‹n > 0 ⟹ compress (replicate n TWO) = TWOs n Empty›}
14
+
\solnblock{\shiki{apply (induct n; simp)
15
+
apply (case_tac "n > 0"; simp)
16
+
done}}
+4
trees/isa/isa-0028.tree
+4
trees/isa/isa-0028.tree
+5
trees/isa/isa-0029.tree
+5
trees/isa/isa-0029.tree
+13
trees/isa/isa-002A.tree
+13
trees/isa/isa-002A.tree
···
1
+
\date{2025-12-03T06:15:34Z}
2
+
\author{liamoc}
3
+
\taxon{Example}
4
+
\import{shiki-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\title{Wellformedness for \code{oots}}
7
+
\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.}
8
+
\shiki{inductive well :: ‹oots ⇒ bool› where
9
+
‹well Empty›
10
+
| ‹n > 0 ⟹ well (ONEs n Empty)›
11
+
| ‹n > 0 ⟹ well (TWOs n Empty)›
12
+
| ‹n > 0 ⟹ well (ONEs m r) ⟹ well (TWOs n (ONEs m r))›
13
+
| ‹n > 0 ⟹ well (TWOs m r) ⟹ well (ONEs n (TWOs m r))›}
+20
trees/isa/isa-002B.tree
+20
trees/isa/isa-002B.tree
···
1
+
\date{2025-12-03T06:23:23Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{\code{compress_expand}}
9
+
\shiki{lemma compress_expand:‹well s ⟹ compress (expand s) = s›}
10
+
\solnblock{\shiki{apply (induct rule: well.induct)
11
+
apply simp
12
+
apply (simp add: compress_replicate_ONE)
13
+
apply (simp add: compress_replicate_TWO)
14
+
apply (simp add: compress_replicate_ONE
15
+
compress_replicate_TWO
16
+
compress_app)
17
+
apply (simp add: compress_replicate_ONE
18
+
compress_replicate_TWO
19
+
compress_app)
20
+
done}}
+11
trees/isa/isa-002C.tree
+11
trees/isa/isa-002C.tree
···
1
+
\date{2025-12-03T06:30:43Z}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\parent{isa-001B}
5
+
\import{shiki-macros}
6
+
\put\shiki/language{Isabelle Theory}
7
+
\title{List subsequence relation}
8
+
\shiki{inductive subsequence :: ‹'a list ⇒ 'a list ⇒ bool› where
9
+
ss_empty: ‹subsequence [] []›
10
+
| ss_keep: ‹subsequence xs ys ⟹ subsequence (x#xs) (x#ys)›
11
+
| ss_drop: ‹subsequence xs ys ⟹ subsequence xs (y#ys)›}
+14
trees/isa/isa-002D.tree
+14
trees/isa/isa-002D.tree
···
1
+
\date{2025-12-03T06:34:53Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{Reflexivity of \code{subsequence}}
9
+
\shiki{lemma ss_refl: ‹subsequence ls ls›}
10
+
\solnblock{\shiki{apply (induct ls)
11
+
apply (rule ss_empty)
12
+
apply (rule ss_keep)
13
+
apply assumption
14
+
done}}
+14
trees/isa/isa-002E.tree
+14
trees/isa/isa-002E.tree
···
1
+
\date{2025-12-03T06:40:22Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{Length of \code{subsequence}}
9
+
\shiki{lemma ss_length : ‹subsequence xs ys ⟹ length xs ≤ length ys›}
10
+
\solnblock{\shiki{apply (induct rule: subsequence.induct)
11
+
apply simp
12
+
apply simp
13
+
apply simp
14
+
done}}
+4
trees/isa/isa-002F.tree
+4
trees/isa/isa-002F.tree
+4
trees/isa/isa-002G.tree
+4
trees/isa/isa-002G.tree
+20
trees/isa/isa-002H.tree
+20
trees/isa/isa-002H.tree
···
1
+
\date{2025-12-03T06:43:34Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{Antisymmetry of \code{subsequence}}
9
+
\shiki{lemma ss_antisym: ‹subsequence ys xs ⟹ subsequence xs ys ⟹ xs = ys›}
10
+
\solnblock{\shiki{apply (induct rule: subsequence.induct)
11
+
apply simp
12
+
apply simp
13
+
apply (erule subsequence.cases, clarsimp, clarsimp,clarsimp)
14
+
apply (drule ss_length)+
15
+
apply simp
16
+
apply (drule ss_length)+
17
+
apply simp
18
+
done}}
19
+
20
+
+4
trees/isa/isa-002I.tree
+4
trees/isa/isa-002I.tree
+42
trees/isa/isa-002J.tree
+42
trees/isa/isa-002J.tree
···
1
+
\date{2025-12-03T06:48:59Z}
2
+
\taxon{Theorem}
3
+
\import{shiki-macros}
4
+
\import{dt-macros}
5
+
\put\shiki/language{Isabelle Theory}
6
+
\author{liamoc}
7
+
\parent{isa-001B}
8
+
\title{Transitivity of \code{subsequence}}
9
+
\shiki{lemma ss_trans: ‹subsequence ys zs ⟹ subsequence xs ys ⟹ subsequence xs zs›}
10
+
\solnblock{\shiki{apply (induct ys zs arbitrary: xs rule: subsequence.induct)
11
+
apply simp
12
+
apply (erule subsequence.cases)
13
+
apply simp
14
+
apply clarsimp
15
+
16
+
apply (erule subsequence.cases)
17
+
apply simp
18
+
apply clarsimp
19
+
apply (rule ss_keep)
20
+
apply simp
21
+
apply simp
22
+
apply clarsimp
23
+
apply (rule ss_drop)
24
+
apply simp
25
+
apply simp
26
+
apply clarsimp
27
+
28
+
apply (erule subsequence.cases)
29
+
apply clarsimp
30
+
apply clarsimp
31
+
apply (rule ss_keep)
32
+
apply clarsimp
33
+
apply clarsimp
34
+
apply (rule ss_drop)
35
+
apply clarsimp
36
+
apply (rule ss_drop)
37
+
apply simp
38
+
done}}
39
+
40
+
41
+
42
+