diff --git a/README.md b/README.md
index c1c0f0c252e99f7a094d3d0f052a910ab76cba76..42dac8cacd1cde5aa1a9feb7e698d663fffc9ce2 100644
--- a/README.md
+++ b/README.md
@@ -89,8 +89,8 @@ In the reading list below, HandAR-Ch.2 means Chapter 2 in the Handbook of Practi
 |       | Fri | 01.12.2023 | 13:15 | INR219 | Lecture |  [Approximating Loops. Recursion 1](https://tube.switch.ch/videos/xCQoLRTGKq), [Recursion 2](https://tube.switch.ch/videos/NjerTXfE9z), [Termination](lectures/termination.pdf) |
 | 12    | Thu | 07.12.2023 | 15:15 | GRA330 | Labs | Project discussions with course staff |
 |       |     |            | 17:15 | GRA330 | Labs | Project discussions with course staff |
-|       | Fri | 08.12.2023 | 13:15 | INR219 | Lecture | [SMT Solvers](https://tube.switch.ch/videos/CDDwI5RZD0), [Tableau-Based Theorem Proving](lectures/Lecture_on_Tableau-1.pdf) (by Simon)
-| 13    | Thu | 14.12.2023 | 15:15 | GRA330 | Lecture | Guest lecture by [Prof. Thomas Bourgeat](https://people.epfl.ch/thomas.bourgeat) |
+|       | Fri | 08.12.2023 | 13:15 | INR219 | Lecture | [SMT Solvers](https://tube.switch.ch/videos/CDDwI5RZD0), [Tableau-Based Theorem Proving](lectures/Lecture_on_Tableau-1.pdf) (by Simon), [example tableaux proofs](https://www.umsu.de/trees/)
+| 13    | Thu | 14.12.2023 | 15:15 | GRA330 | Lecture | [Hardware Verification Lecture](lectures/ThomasBourgeat-HardwareVerification.pdf) by [Prof. Thomas Bourgeat](https://people.epfl.ch/thomas.bourgeat) |
 |       |     |            | 17:15 | GRA330 | Labs |  |
 |       | Fri | 15.12.2023 | 13:00 | INR219 | Project Presentations | VIDIGUIERA Manuel, CONTOVOUNESIOS Basil, POIROUX Auguste |
 |       |     |            | 13:30 | INR219 | Project Presentations | ILIESCU Valentina-Florentina, WINDLER Leon, LAZAR David Leonardo| 
diff --git a/lectures/ThomasBourgeat-HardwareVerification.pdf b/lectures/ThomasBourgeat-HardwareVerification.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..c616cbeaa2dbf736e36b4b178981201a5c8a8ca0
Binary files /dev/null and b/lectures/ThomasBourgeat-HardwareVerification.pdf differ
diff --git a/lectures/lec10-isabelle/Demos/AExp.thy b/lectures/lec10-isabelle/Demos/AExp.thy
deleted file mode 100644
index 51135091319a44b56673521bff9de110d0c32f08..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/AExp.thy
+++ /dev/null
@@ -1,95 +0,0 @@
-section "Arithmetic and Boolean Expressions"
-
-theory AExp imports Main begin
-
-subsection "Arithmetic Expressions"
-
-type_synonym vname = string
-type_synonym val = int
-type_synonym state = "vname \<Rightarrow> val"
-
-datatype aexp = N int | V vname | Plus aexp aexp
-
-fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
-"aval (N n) s = n" |
-"aval (V x) s = s x" |
-"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
-
-
-value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
-
-text \<open>The same state more concisely:\<close>
-value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
-
-text \<open>A little syntax magic to write larger states compactly:\<close>
-
-definition null_state ("<>") where
-  "null_state \<equiv> \<lambda>x. 0"
-syntax 
-  "_State" :: "updbinds => 'a" ("<_>")
-translations
-  "_State ms" == "_Update <> ms"
-  "_State (_updbinds b bs)" <= "_Update (_State b) bs"
-
-text \<open>We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:\<close>
-lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))"
-  by (rule refl)
-
-value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
-
-
-text \<open>In the @{term "<a := b>"} syntax, variables that are not mentioned are 0 by default:\<close>
-value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
-
-text \<open>Note that this @{text"<\<dots>>"} syntax works for any function space
-@{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} where @{text "\<tau>\<^sub>2"} has a @{text 0}.\<close>
-
-
-subsection "Constant Folding"
-
-text \<open>Evaluate constant subexpressions:\<close>
-
-fun asimp_const :: "aexp \<Rightarrow> aexp" where
-"asimp_const (N n) = N n" |
-"asimp_const (V x) = V x" |
-"asimp_const (Plus a\<^sub>1 a\<^sub>2) =
-  (case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of
-    )"
-
-theorem aval_asimp_const:
-  "aval (asimp_const a) s = aval a s"
-apply(induction )
-apply (auto)
-done
-
-text \<open>Now we also eliminate all occurrences 0 in additions. The standard
-method: optimized versions of the constructors:\<close>
-
-fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
-"plus "
-
-lemma aval_plus [simp]:
-  "aval (plus a1 a2) s = aval a1 s + aval a2 s"
-apply(induction a1 a2 rule: plus.induct)
-apply auto
-done
-
-fun asimp :: "aexp \<Rightarrow> aexp" where
-"asimp (N n) = N n" |
-"asimp (V x) = V x" |
-"asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)"
-
-
-text \<open>Note that in @{const asimp_const} the optimized constructor was
-inlined. Making it a separate function @{const plus} improves modularity of
-the code and the proofs.\<close>
-
-value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
-
-theorem aval_asimp[simp]:
-  "aval (asimp a) s = aval a s"
-apply(induction a)
-apply (auto)
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/ASM.thy b/lectures/lec10-isabelle/Demos/ASM.thy
deleted file mode 100644
index 6f61b0dd06a2b19fdb3f60e3786c301ca860de35..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/ASM.thy
+++ /dev/null
@@ -1,39 +0,0 @@
-section "Stack Machine and Compilation"
-
-theory ASM
-imports AExp
-begin
-
-subsection "Stack Machine"
-
-datatype instr = LOADI val | LOAD vname | ADD
-
-type_synonym stack = "val list"
-
-fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
-"exec1 (LOADI n) _ stk  =  " |
-"exec1 (LOAD x) s stk  =  " |
-"exec1  ADD _ (i # j # stk)  =  "
-
-fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
-"exec [] _ stk = stk" |
-"exec (i#is) s stk = "
-
-value "exec [LOADI 5, LOAD ''y'', ADD] <''x'' := 42, ''y'' := 43> [50]"
-
-
-subsection "Compilation"
-
-fun comp :: "aexp \<Rightarrow> instr list" where
-"comp (N n) = " |
-"comp (V x) = " |
-"comp (Plus e1 e2) ="
-
-value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
-
-theorem exec_comp: "exec (comp a) s [] = "
-apply(induction)
-apply (auto)
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/AgathaInIsabelle.thy b/lectures/lec10-isabelle/Demos/AgathaInIsabelle.thy
deleted file mode 100644
index 3ef21549a0ae1ab4e7b204710da096f52b1a9635..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/AgathaInIsabelle.thy
+++ /dev/null
@@ -1,20 +0,0 @@
-theory AgathaInIsabelle
-imports Main
-begin
-
-theorem agatha:
-assumes a1 : "EX  x. (lives x & killed x  a)"
-and     a2 : "lives a & lives b & lives c & (ALL x. (lives x --> (x=a | x=b | x=c)))"
-and     a3 : "ALL x. ALL y. killed x y --> (hates x y & ~richer x y)"
-and     a4 : "ALL x. (hates a x --> ~hates c x)"
-and     a5 : "ALL x. (hates a x = (x ~= b))"
-and     a6 : "ALL x. ((~richer x a) = hates b x)"
-and     a7 : "ALL x. (hates a x --> hates b x)"
-and     a8 : "~(EX x. ALL y. hates x y)"
-and     a9 : "a ~= b"
-shows   "killed a a"
-(* use sledgehammer to find suggestion *)
-
-thm "agatha"
-
-end
\ No newline at end of file
diff --git a/lectures/lec10-isabelle/Demos/Auto_Proof_Demo.thy b/lectures/lec10-isabelle/Demos/Auto_Proof_Demo.thy
deleted file mode 100644
index ffccca8d72b1aa1d2fc9556026cae2e1ab1c6504..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Auto_Proof_Demo.thy
+++ /dev/null
@@ -1,58 +0,0 @@
-theory Auto_Proof_Demo
-imports Main
-begin
-
-section "Logic and sets"
-
-lemma "ALL x. EX y. x=y"
-by auto
-
-lemma "A \<subseteq> B \<inter> C \<Longrightarrow> A \<subseteq> B \<union> C"
-by auto
-
-text \<open>Note the bounded quantification notation:\<close>
-
-lemma "\<lbrakk> \<forall>xs \<in> A. \<exists>ys. xs = ys @ ys;  us \<in> A \<rbrakk> \<Longrightarrow> \<exists>n. length us = n+n"
-by fastforce
-
-
-text \<open>Most simple proofs in FOL and set theory are automatic.
-Example: if T is total, A is antisymmetric and T is a subset of A, then A is a subset of T.\<close>
-
-lemma AT:
-  "\<lbrakk> \<forall>x y. T x y \<or> T y x;
-     \<forall>x y. A x y \<and> A y x \<longrightarrow> x = y;
-     \<forall>x y. T x y \<longrightarrow> A x y \<rbrakk>
-   \<Longrightarrow> \<forall>x y. A x y \<longrightarrow> T x y"
-by blast
-
-
-section "Sledgehammer"
-
-lemma "R^* \<subseteq> (R \<union> S)^*"
-oops
-
-text \<open>Find a suitable P and try sledgehammer:\<close>
-
-lemma "a # xs = ys @ [a] \<Longrightarrow> P"
-oops
-
-
-section "Arithmetic"
-
-lemma "\<lbrakk> (a::int) \<le> f x + b; 2 * f x < c \<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c"
-by arith
-
-lemma "\<forall> (k::nat) \<ge> 8. \<exists> i j. k = 3*i + 5*j"
-by arith
-
-lemma "(n::int) mod 2 = 1 \<Longrightarrow> (n+n) mod 2 = 0"
-by arith
-
-lemma "(i + j) * (i - j) \<le> i*i + j*(j::int)"
-by (simp add: algebra_simps)
-
-lemma "(5::int) ^ 2 = 20+5"
-by simp
-
-end
diff --git a/lectures/lec10-isabelle/Demos/BExp.thy b/lectures/lec10-isabelle/Demos/BExp.thy
deleted file mode 100644
index 70b8d961149daddda4d08d63bd94212c6006caa1..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/BExp.thy
+++ /dev/null
@@ -1,63 +0,0 @@
-theory BExp imports AExp begin
-
-subsection "Boolean Expressions"
-
-datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
-
-fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
-"bval (Bc v) s = v" |
-"bval (Not b) s = (\<not> bval b s)" |
-"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
-"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
-
-value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
-            <''x'' := 3, ''y'' := 1>"
-
-
-subsection "Constant Folding"
-
-text \<open>Optimizing constructors:\<close>
-
-fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
-"less "
-
-lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
-apply(induction)
-apply auto
-done
-
-fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
-"and = "
-
-lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
-apply(induction b1 b2 rule: and.induct)
-apply auto
-done
-
-fun not :: "bexp \<Rightarrow> bexp" where
-"not (Bc v) = Bc(\<not> v)" |
-"not b = Not b"
-
-lemma bval_not[simp]: "bval (not b) s = (\<not> bval b s)"
-apply(induction )
-apply auto
-done
-
-text \<open>Now the overall optimizer:\<close>
-
-fun bsimp :: "bexp \<Rightarrow> bexp" where
-"bsimp (Bc v) = Bc v" |
-"bsimp (Not b) = not(bsimp b)" |
-"bsimp (And b\<^sub>1 b\<^sub>2) = and (bsimp b\<^sub>1) (bsimp b\<^sub>2)" |
-"bsimp (Less a\<^sub>1 a\<^sub>2) = less (asimp a\<^sub>1) (asimp a\<^sub>2)"
-
-value "bsimp (And (Less (N 0) (N 1)) b)"
-
-value "bsimp (And (Less (N 1) (N 0)) (Bc True))"
-
-theorem "bval (bsimp b) s = bval b s"
-apply(induction b)
-apply auto
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/BST_Demo.thy b/lectures/lec10-isabelle/Demos/BST_Demo.thy
deleted file mode 100644
index a70cbec1b47527fdddb1f88ea51ce33438f6165e..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/BST_Demo.thy
+++ /dev/null
@@ -1,73 +0,0 @@
-theory BST_Demo
-imports "HOL-Library.Tree"
-begin
-
-(* useful most of the time: *)
-declare Let_def [simp]
-
-section "BST Search and Insertion"
-
-fun isin :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> bool" where
-"isin Leaf x = False" |
-"isin (Node l a r) x =
-  (if x < a then isin l x else
-   if x > a then isin r x
-   else True)"
-
-fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"ins x Leaf = Node Leaf x Leaf" |
-"ins x (Node l a r) =
-  (if x < a then Node (ins x l) a r else
-   if x > a then Node l a (ins x r)
-   else Node l a r)"
-
-subsection "Functional Correctness"
-
-lemma set_tree_isin: "bst t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
-apply(induction t)
-apply auto
-done
-
-lemma set_tree_ins: "set_tree (ins x t) = {x} \<union> set_tree t"
-apply(induction t)
-apply auto
-done
-
-subsection "Preservation of Invariant"
-
-lemma bst_ins: "bst t \<Longrightarrow> bst (ins x t)"
-apply(induction t)
-apply (auto simp: set_tree_ins)
-done
-
-
-section "BST Deletion"
-
-fun split_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
-"split_min (Node l a r) =
-  (if l = Leaf then (a,r)
-   else let (x,l') = split_min l
-        in (x, Node l' a r))"
-
-fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"delete x Leaf = Leaf" |
-"delete x (Node l a r) =
-  (if x < a then Node (delete x l) a r else
-   if x > a then Node l a (delete x r)
-   else if r = Leaf then l else let (a',r') = split_min r in Node l a' r')"
-
-(* A proof attempt *)
-
-lemma "split_min t = (x,t') \<Longrightarrow> set_tree t' = set_tree t - {x}"
-oops
-
-(* The final proof (needs more than auto!): *)
-
-lemma "\<lbrakk> split_min t = (x,t'); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
-  set_tree t' = set_tree t - {x} \<and> x \<in> set_tree t"
-apply(induction t arbitrary: x t')
- apply simp
-apply (force split: if_split_asm prod.splits)
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Induction_Demo.thy b/lectures/lec10-isabelle/Demos/Induction_Demo.thy
deleted file mode 100644
index 1a3e74a752c97481bd44e0032e72bfb680832675..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Induction_Demo.thy
+++ /dev/null
@@ -1,27 +0,0 @@
-theory Induction_Demo
-imports Main
-begin
-
-fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"itrev [] ys = ys" |
-"itrev (x#xs) ys = itrev xs (x#ys)"
-
-lemma "itrev xs [] = rev xs"
-apply(induction xs)
-apply(auto)
-done
-
-
-subsection "Computation Induction"
-
-fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"sep a [] = []" |
-"sep a [x] = [x]" |
-"sep a (x#y#zs) = x # a # sep a (y#zs)"
-
-lemma "map f (sep a xs) = sep (f a) (map f xs)"
-apply(induction a xs rule: sep.induct)
-apply auto
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Inductive_Demo.thy b/lectures/lec10-isabelle/Demos/Inductive_Demo.thy
deleted file mode 100644
index 59278a9386ddb667f68fa1f0f19f0fec84498388..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Inductive_Demo.thy
+++ /dev/null
@@ -1,80 +0,0 @@
-theory Inductive_Demo
-imports Main
-begin
-
-subsection "Inductive definition of the even numbers"
-
-inductive ev :: "nat \<Rightarrow> bool" where
-ev0: "ev 0" |
-evSS: "ev n \<Longrightarrow> ev (Suc(Suc n))"
-
-thm ev0 evSS
-thm ev.intros
-
-text \<open>Using the introduction rules:\<close>
-
-lemma "ev (Suc(Suc(Suc(Suc 0))))"
-
-done
-
-thm evSS[OF evSS[OF ev0]]
-
-text \<open>A recursive definition of evenness:\<close>
-
-fun evn :: "nat \<Rightarrow> bool" where
-"evn 0 = True" |
-"evn (Suc 0) = False" |
-"evn (Suc(Suc n)) = evn n"
-
-text \<open>A simple example of rule induction:\<close>
-
-lemma "ev n \<Longrightarrow> evn n"
-apply(induction rule: ev.induct)
-
-done
-
-text \<open>An induction on the computation of evn:\<close>
-
-lemma "evn n \<Longrightarrow> ev n"
-apply(induction n rule: evn.induct)
-
-done
-
-text \<open>No problem with termination because the premises are always smaller
-than the conclusion:\<close>
-
-declare ev.intros[simp,intro]
-
-text \<open>A shorter proof:\<close>
-
-lemma "evn n \<Longrightarrow> ev n"
-apply(induction n rule: evn.induct)
-apply(simp_all)
-done
-
-text \<open>The power of arith:\<close>
-
-lemma "ev n \<Longrightarrow> \<exists>k. n = 2*k"
-apply(induction rule: ev.induct)
- apply simp
-apply arith
-done
-
-
-subsection "Inductive definition of the reflexive transitive closure"
-
-inductive
-  star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-for r where
-refl:  "star r x x" |
-step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-
-lemma star_trans:
-  "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-apply(induction rule: star.induct)
-apply(assumption)
-apply(rename_tac u x y)
-
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Isar_Demo.thy b/lectures/lec10-isabelle/Demos/Isar_Demo.thy
deleted file mode 100644
index 0926d42d74bf1b800f36668bdf37e2b0872c5d14..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Isar_Demo.thy
+++ /dev/null
@@ -1,279 +0,0 @@
-theory Isar_Demo
-imports Complex_Main
-begin
-
-section "An introductory example"
-
-lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
-proof
-  assume 0: "surj f"
-  from 0 have 1: "\<forall>A. \<exists>a. A = f a" by(simp add: surj_def)
-  from 1 have 2: "\<exists>a. {x. x \<notin> f x} = f a" by blast
-  from 2 show "False" by blast
-qed
-
-text \<open>A bit shorter:\<close>
-
-lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
-proof
-  assume 0: "surj f"
-  from 0 have 1: "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
-  from 1 show "False" by blast
-qed
-
-subsection \<open>"this", "then", "hence" and "thus\<close>
-
-text \<open>Avoid labels, use "this"\<close>
-
-lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
-proof
-  assume "surj f"
-  from this have "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
-  from this show "False" by blast
-qed
-
-text \<open>"then" = "from this"\<close>
-
-lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
-proof
-  assume "surj f"
-  then have "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
-  then show "False" by blast
-qed
-
-text \<open>"hence" = "then have", "thus" = "then show"\<close>
-
-lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
-proof
-  assume "surj f"
-  hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
-  thus "False" by blast
-qed
-
-
-subsection \<open>Structured statements: "fixes", "assumes", "shows"\<close>
-
-lemma
-  fixes f :: "'a \<Rightarrow> 'a set"
-  assumes s: "surj f"
-  shows "False"
-proof -  (* no automatic proof step! *)
-  have "\<exists> a. {x. x \<notin> f x} = f a" using s
-    by(auto simp: surj_def)
-  thus "False" by blast
-qed
-
-
-section "Proof patterns"
-
-lemma "P \<longleftrightarrow> Q"
-proof
-  assume "P"
-  show "Q" sorry
-next
-  assume "Q"
-  show "P" sorry
-qed
-
-lemma "A = (B::'a set)"
-proof
-  show "A \<subseteq> B" sorry
-next
-  show "B \<subseteq> A" sorry
-qed
-
-lemma "A \<subseteq> B"
-proof
-  fix a
-  assume "a \<in> A"
-  show "a \<in> B" sorry
-qed
-
-text "Contradiction"\<section>
-
-lemma P
-proof (rule ccontr)
-  assume "\<not>P"
-  show "False" sorry
-qed
-
-text "Case distinction"
-
-lemma "R"
-proof cases
-  assume "P"
-  show "R" sorry
-next
-  assume "\<not> P"
-  show "R" sorry
-qed
-
-lemma "R"
-proof -
-  have "P \<or> Q" sorry
-  then show "R"
-  proof
-    assume "P"
-    show "R" sorry
-  next
-    assume "Q"
-    show "R" sorry
-  qed
-qed
-
-
-text \<open>"obtain" example\<close>
-
-lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"
-proof
-  assume "surj f"
-  hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)
-  then obtain a where "{x. x \<notin> f x} = f a" by blast
-  hence "a \<notin> f a \<longleftrightarrow> a \<in> f a" by blast
-  thus "False" by blast
-qed
-
-
-text \<open>Interactive exercise:\<close>
-
-lemma assumes "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
-sorry
-
-
-subsection \<open>(In)Equation Chains\<close>
-
-lemma "(0::real) \<le> x^2 + y^2 - 2*x*y"
-proof -
-  have "0 \<le> (x - y)^2" by simp
-  also have "\<dots> = x^2 + y^2 - 2*x*y"
-    by(simp add: numeral_eq_Suc algebra_simps)
-  finally show "0 \<le> x^2 + y^2 - 2*x*y" .
-qed
-
-text \<open>Interactive exercise:\<close>
-
-lemma
-  fixes x y :: real
-  assumes "x \<ge> y" "y > 0"
-  shows "(x - y) ^ 2 \<le> x^2 - y^2"
-proof -
-  have "(x - y) ^ 2 = x^2 + y^2 - 2*x*y"
-    by(simp add: numeral_eq_Suc algebra_simps)
-  show "(x - y) ^ 2 \<le> x^2 - y^2" sorry
-qed
-
-
-section "Streamlining proofs"
-
-subsection "Pattern matching and ?-variables"
-
-text \<open>Show \<open>\<exists>\<close>\<close>
-
-lemma "\<exists> xs. length xs = 0" (is "\<exists> xs. ?P xs")
-proof
-  show "?P([])" by simp
-qed
-
-text \<open>Multiple EX easier with forward proof:\<close>
-
-lemma "\<exists> x y :: int. x < z & z < y" (is "\<exists> x y. ?P x y")
-proof -
-  have "?P (z - 1) (z + 1)" by arith
-  thus ?thesis by blast
-qed
-
-
-subsection "Quoting facts"
-
-lemma assumes "x < (0::int)" shows "x*x > 0"
-proof -
-  from `x<0` show ?thesis by(metis mult_neg_neg)
-qed
-
-
-subsection "Example: Top Down Proof Development"
-
-lemma "\<exists>ys zs. xs = ys @ zs \<and>
-          (length ys = length zs \<or> length ys = length zs + 1)"
-sorry
-
-
-
-section "Solutions to interactive exercises"
-
-lemma assumes "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
-proof
-  fix b
-  from assms obtain a where 0: "\<forall>y. P a y" by blast
-  show "\<exists>x. P x b"
-  proof
-    show "P a b" using 0 by blast
-  qed
-qed
-
-lemma fixes x y :: real assumes "x \<ge> y" "y > 0"
-shows "(x - y) ^ 2 \<le> x^2 - y^2"
-proof -
-  have "(x - y) ^ 2 = x^2 + y^2 - 2*x*y"
-    by(simp add: numeral_eq_Suc algebra_simps)
-  also have "\<dots> \<le> x^2 + y^2 - 2*y*y"
-    using assms by(simp)
-  also have "\<dots> = x^2 - y^2"
-    by(simp add: numeral_eq_Suc)
-  finally show ?thesis .
-qed
-
-subsection "Example: Top Down Proof Development"
-
-text \<open>The key idea: case distinction on length:\<close>
-
-lemma "\<exists>ys zs. xs = ys @ zs \<and> (length ys = length zs \<or> length ys = length zs + 1)"
-proof cases
-  assume "EX n. length xs = n+n"
-  show ?thesis sorry
-next
-  assume "\<not> (EX n. length xs = n+n)"
-  show ?thesis sorry
-qed
-
-text \<open>A proof skeleton:\<close>
-
-lemma "\<exists>ys zs. xs = ys @ zs \<and> (length ys = length zs \<or> length ys = length zs + 1)"
-proof cases
-  assume "\<exists>n. length xs = n+n"
-  then obtain n where "length xs = n+n" by blast
-  let ?ys = "take n xs"
-  let ?zs = "take n (drop n xs)"
-  have "xs = ?ys @ ?zs \<and> length ?ys = length ?zs" sorry
-  thus ?thesis by blast
-next
-  assume "\<not> (\<exists>n. length xs = n+n)"
-  then obtain n where "length xs = Suc(n+n)" sorry
-  let ?ys = "take (Suc n) xs"
-  let ?zs = "take n (drop (Suc n) xs)"
-  have "xs = ?ys @ ?zs \<and> length ?ys = length ?zs + 1" sorry
-  then show ?thesis by blast
-qed
-
-text "The complete proof:"
-
-lemma "\<exists>ys zs. xs = ys @ zs \<and> (length ys = length zs \<or> length ys = length zs + 1)"
-proof cases
-  assume "\<exists>n. length xs = n+n"
-  then obtain n where "length xs = n+n" by blast
-  let ?ys = "take n xs"
-  let ?zs = "take n (drop n xs)"
-  have "xs = ?ys @ ?zs \<and> length ?ys = length ?zs"
-    by (simp add: `length xs = n + n`)
-  thus ?thesis by blast
-next
-  assume "\<not> (\<exists>n. length xs = n+n)"
-  hence "\<exists>n. length xs = Suc(n+n)" by arith
-  then obtain n where l: "length xs = Suc(n+n)" by blast
-  let ?ys = "take (Suc n) xs"
-  let ?zs = "take n (drop (Suc n) xs)"
-  have "xs = ?ys @ ?zs \<and> length ?ys = length ?zs + 1" by (simp add: l)
-  thus ?thesis by blast
-qed
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Isar_Induction_Demo.thy b/lectures/lec10-isabelle/Demos/Isar_Induction_Demo.thy
deleted file mode 100644
index 7ade337815dd8ed82f6da2fde460ac603930caa3..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Isar_Induction_Demo.thy
+++ /dev/null
@@ -1,245 +0,0 @@
-theory Isar_Induction_Demo
-imports Main
-begin
-
-section "Case distinction and induction"
-
-subsection "Case distinction"
-
-text \<open>Explicit:\<close>
-
-lemma "length(tl xs) = length xs - 1"
-proof (cases xs)
-  assume "xs = []" thus ?thesis by simp
-next
-  fix y ys assume "xs = y#ys"
-  thus ?thesis by simp
-qed
-
-text \<open>Implicit:\<close>
-
-lemma "length(tl xs) = length xs - 1"
-proof (cases xs)
-print_cases
-  case Nil
-thm Nil
-  thus ?thesis by simp
-next
-  case (Cons y ys)
-thm Cons
-  thus ?thesis by simp
-qed
-
-
-subsection \<open>Structural induction for type @{typ nat}\<close>
-
-text \<open>Explicit:\<close>
-
-lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" (is "?P n")
-proof (induction n)
-  show "?P 0" by simp
-next
-  fix n assume "?P n"
-  thus "?P(Suc n)" by simp
-qed
-
-text \<open>In more detail:\<close>
-
-lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" (is "?P n")
-proof (induction n)
-  show "?P 0" by simp
-next
-  fix n assume IH: "?P n"
-  have "\<Sum>{0..Suc n} = \<Sum>{0..n} + Suc n" by simp
-  also have "\<dots> = n*(n+1) div 2 + Suc n" using IH by simp
-  also have "\<dots> = (Suc n)*((Suc n)+1) div 2" by simp
-  finally show "?P(Suc n)" .
-qed
-
-text \<open>Implicit:\<close>
-
-lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"
-proof (induction n)
-print_cases
-  case 0
-  show ?case by simp
-next
-  case (Suc n)
-thm Suc
-  thus ?case by simp
-qed
-
-text \<open>Induction with \<open>\<Longrightarrow>\<close>:\<close>
-
-lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
-proof (induction xs)
-  case Nil thus ?case by simp
-next
-  case (Cons a xs)
-thm Cons.IH (* Induction hypothesis *)
-thm Cons.prems (* Premises of the step case *)
-thm Cons
-  from Cons.prems have "x = a \<or> x : set xs" by simp
-  thus ?case
-  proof
-    assume "x = a"
-    hence "a#xs = [] @ x # xs" by simp
-    thus ?thesis by blast
-  next
-    assume "x : set xs"
-    then obtain ys zs where "xs = ys @ x # zs" using Cons.IH by auto
-    hence "a#xs = (a#ys) @ x # zs" by simp
-    thus ?thesis by blast
-  qed
-qed
-
-
-subsection "Computation induction"
-
-fun div2 :: "nat \<Rightarrow> nat" where
-"div2 0 = 0" |
-"div2 (Suc 0) = 0" |
-"div2 (Suc(Suc n)) = div2 n + 1"
-
-lemma "2 * div2 n \<le> n"
-proof(induction n rule: div2.induct)
-  case 1
-  show ?case by simp
-next
-  case 2
-  show ?case by simp
-next
-  case (3 n)
-  have "2 * div2 (Suc(Suc n)) = 2 * div2 n + 2" by simp
-  also have "\<dots> \<le> n + 2" using "3.IH" by simp
-  also have "\<dots> = Suc(Suc n)" by simp
-  finally show ?case .
-qed
-
-text \<open>Note that \<open>3.IH\<close> is not a valid name, it needs double quotes: \<open>"3.IH"\<close>.\<close>
-
-
-fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"sep a (x # y # zs) = x # a # sep a (y # zs)" |
-"sep a xs = xs"
-
-thm sep.simps
-
-lemma "map f (sep a xs) = sep (f a) (map f xs)"
-proof (induction a xs rule: sep.induct)
-print_cases
-  case (1 a x y zs)
-  thus ?case by simp
-next
-  case ("2_1" a)
-  show ?case by simp
-next
-  case ("2_2" a v)
-  show ?case by simp
-qed
-
-
-
-subsection "Rule induction"
-
-
-inductive ev :: "nat => bool" where
-ev0:  "ev 0" |
-evSS:  "ev n \<Longrightarrow> ev(Suc(Suc n))"
-
-declare ev.intros [simp]
-
-
-lemma "ev n \<Longrightarrow> \<exists>k. n = 2*k"
-proof (induction rule: ev.induct)
-  case ev0 show ?case by simp
-next
-  case evSS thus ?case by arith
-qed
-
-
-lemma "ev n \<Longrightarrow> \<exists>k. n = 2*k"
-proof (induction rule: ev.induct)
-  case ev0 show ?case by simp
-next
-  case (evSS m)
-thm evSS
-thm evSS.IH
-thm evSS.hyps
-  from evSS.IH obtain k where "m = 2*k" by blast
-  hence "Suc(Suc m) = 2*(k+1)" by simp
-  thus "\<exists>k. Suc(Suc m) = 2*k" by blast
-qed
-
-
-subsection "Inductive definition of the reflexive transitive closure"
-
-consts step :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<rightarrow>" 55)
-
-inductive steps :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<rightarrow>*" 55) where
-refl: "x \<rightarrow>* x" |
-step: "\<lbrakk> x \<rightarrow> y; y \<rightarrow>* z \<rbrakk> \<Longrightarrow> x \<rightarrow>* z"
-
-declare refl[simp, intro]
-
-text "Explicit and by hand:"
-
-lemma "x \<rightarrow>* y  \<Longrightarrow>  y \<rightarrow>* z \<Longrightarrow> x \<rightarrow>* z"
-proof(induction rule: steps.induct)
-  fix x assume "x \<rightarrow>* z"
-  thus "x \<rightarrow>* z" . (* by assumption *)
-next
-  fix x' x y :: 'a
-  assume "x' \<rightarrow> x" and "x \<rightarrow>* y"
-  assume IH: "y \<rightarrow>* z \<Longrightarrow> x \<rightarrow>* z"
-  assume "y \<rightarrow>* z"
-  show "x' \<rightarrow>* z" by(rule step[OF `x' \<rightarrow> x` IH[OF `y\<rightarrow>*z`]])
-qed
-
-text \<open>Implicit and automatic:\<close>
-
-lemma "x \<rightarrow>* y  \<Longrightarrow>  y \<rightarrow>* z \<Longrightarrow> x \<rightarrow>* z"
-proof(induction rule: steps.induct)
-  case refl thus ?case .
-next
-  case (step x' x y)
-  (* x' x y not used in proof text, just for demo *)
-thm step
-thm step.IH
-thm step.hyps
-thm step.prems
-  show ?case
-    by (metis step.hyps(1) step.IH step.prems steps.step)
-qed
-
-
-subsection "Rule inversion"
-
-
-lemma assumes "ev n" shows "ev(n - 2)"
-proof-
-  from `ev n` show "ev(n - 2)"
-  proof cases
-    case ev0
-thm ev0
-    then show ?thesis by simp
-  next
-    case (evSS k)
-thm evSS
-    then show ?thesis by simp
-  qed
-qed
-
-
-text \<open>Impossible cases are proved automatically:\<close>
-
-lemma "\<not> ev(Suc 0)"
-proof
-  assume "ev(Suc 0)"
-  then show False
-  proof cases
-  qed
-qed
-
-
-end
diff --git a/lectures/lec10-isabelle/Demos/List_Demo.thy b/lectures/lec10-isabelle/Demos/List_Demo.thy
deleted file mode 100644
index a0a494252ea87e14c79f8728adff653b3f181776..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/List_Demo.thy
+++ /dev/null
@@ -1,29 +0,0 @@
-theory List_Demo
-imports Main
-begin
-
-datatype 'a list = Nil | Cons "'a" "'a list"
-
-term "Nil"
-
-declare [[names_short]]
-
-fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"app Nil ys = ys" |
-"app (Cons x xs) ys = Cons x (app xs ys)"
-
-fun rev :: "'a list \<Rightarrow> 'a list" where
-"rev Nil = Nil" |
-"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
-
-value "rev(Cons True (Cons False Nil))"
-
-value "rev(Cons a (Cons b Nil))"
-
-theorem rev_rev: "rev (rev xs) = xs"
-apply (induction xs)
-apply (auto)
-done
-
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Nat_Demo.thy b/lectures/lec10-isabelle/Demos/Nat_Demo.thy
deleted file mode 100644
index 105ca0571fdd7562a11d53f345e927eb475885bd..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Nat_Demo.thy
+++ /dev/null
@@ -1,14 +0,0 @@
-theory Nat_Demo
-imports Main
-begin
-
-fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-"add 0 n = n" |
-"add (Suc m) n = Suc(add m n)"
-
-lemma add_02: "add m 0 = m"
-apply(induction m)
-apply(auto)
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Overview_Demo.thy b/lectures/lec10-isabelle/Demos/Overview_Demo.thy
deleted file mode 100644
index 8e3dac9fbca6ee91cccfc36e58b3f7502bf35f1d..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Overview_Demo.thy
+++ /dev/null
@@ -1,41 +0,0 @@
-theory Overview_Demo
-imports Main
-begin
-
-(* A simple comment *)
-
-text \<open>This is also a comment but it generates nice \LaTeX-text!\<close>
-
-text \<open>Note that variables and constants (eg True, &) are displayed differently.\<close>
-
-term "True"
-term "False"
-term "true"
-term "True & False"
-term "True & false"
-
-value "True & False"
-value "True & P"
-
-(* To display types in jedit: press ctrl (Mac: cmd) and hover over text.
-   To view the definition of a constant: press ctrl (Mac: cmd) and click on the text.
-*)
-
-text \<open>Warning: "+" and numbers are overloaded:\<close>
-
-term "n + n = 0"
-term "(n::nat) + n = 0"
-
-(*Try this:
-
-term "True + False"
-
-Terms must be type correct!*)
-
-text \<open>Type inference:\<close>
-
-term "f (g x) y"
-term "h (%x. f(g x))"
-term "%x. x + x"
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Simp_Demo.thy b/lectures/lec10-isabelle/Demos/Simp_Demo.thy
deleted file mode 100644
index fcab9e73601ef18e587af8802b09bf59758ecee3..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Simp_Demo.thy
+++ /dev/null
@@ -1,75 +0,0 @@
-theory Simp_Demo
-imports Main
-begin
-
-section "How to simplify"
-
-text \<open>No assumption:\<close>
-
-lemma "ys @ [] = []"
-apply(simp)
-oops (* abandon proof *)
-
-text \<open>Simplification in assumption:\<close>
-
-lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
-apply(simp)
-done
-
-text \<open>Using additional rules:\<close>
-
-lemma "(a+b)*(a-b) = a*a - b*(b::int)"
-apply(simp add: algebra_simps)
-done
-
-text \<open>Giving a lemma the simp-attribute:\<close>
-
-declare algebra_simps [simp]
-
-
-subsection "Rewriting with definitions"
-
-definition sq :: "nat \<Rightarrow> nat" where
-"sq n = n*n"
-
-lemma "sq(n*n) = sq(n)*sq(n)"
-apply(simp add: sq_def) (* Definition of function is implicitly called f_def *)
-done
-
-subsection "Case distinctions"
-
-text \<open>Automatic:\<close>
-
-lemma "(A & B) = (if A then B else False)"
-apply(simp)
-done
-
-lemma "if A then B else C"
-apply(simp)
-oops
-
-text \<open>By hand (for case):\<close>
-
-lemma "1 \<le> (case ns of [] \<Rightarrow> 1 | n#_ \<Rightarrow> Suc n)"
-apply(simp split: list.split)
-done
-
-subsection "Arithmetic"
-
-text \<open>A bit of linear arithmetic (no multiplication) is automatic:\<close>
-
-lemma "\<lbrakk> (x::nat) \<le> y+z;  z+x < y \<rbrakk> \<Longrightarrow> x < y"
-apply(simp)
-done
-
-
-subsection "Tracing"
-
-lemma "rev[x] = []"
-using [[simp_trace]] apply(simp)
-oops
-
-text \<open>Method ``auto'' can be modified almost like ``simp'':
- instead of ``add'' use ``simp add''.\<close>
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Single_Step_Demo.thy b/lectures/lec10-isabelle/Demos/Single_Step_Demo.thy
deleted file mode 100644
index 3f9e77a36095fcbd5b3f0b663fe05baea362995b..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Single_Step_Demo.thy
+++ /dev/null
@@ -1,33 +0,0 @@
-theory Single_Step_Demo
-imports Main
-begin
-
-text \<open>"thm" is a command that displays one or more named theorems:\<close>
-thm conjI impI iffI notI
-
-text \<open>Instantiation of theorems: "of"\<close>
-
-text \<open>Positional:\<close>
-thm conjI[of "A" "B"]
-thm conjI[of "A"]
-thm conjI[of _ "B"]
-
-text \<open>By name:\<close>
-thm conjI[where ?Q = "B"]
-
-text \<open>Composition of theorems: "OF"\<close>
-
-thm refl[of "a"]
-thm conjI[OF refl[of "a"] refl[of "b"]]
-thm conjI[OF refl[of "a"]]
-thm conjI[OF _ refl[of "b"]]
-
-
-text \<open>A simple backward proof:\<close>
-lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> A \<and> B"
-apply(rule conjI)
-apply assumption
-apply assumption
-done
-
-end
diff --git a/lectures/lec10-isabelle/Demos/Tree_Demo.thy b/lectures/lec10-isabelle/Demos/Tree_Demo.thy
deleted file mode 100644
index d80960fc10e90a2a92f9a55349a270c8bd12641b..0000000000000000000000000000000000000000
--- a/lectures/lec10-isabelle/Demos/Tree_Demo.thy
+++ /dev/null
@@ -1,31 +0,0 @@
-theory Tree_Demo
-imports Main
-begin
-
-datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree"
-
-lemma "Leaf ~= Node l x r"
-apply auto
-done
-
-fun mirror :: "'a tree \<Rightarrow> 'a tree" where
-"mirror Leaf = Leaf" |
-"mirror (Node l x r) = Node (mirror r) x (mirror l)"
-
-value "mirror(Node (Node Leaf a Leaf) b t)"
-
-lemma mirror_mirror[simp]: "mirror(mirror t) = t"
-apply(induction t)
-apply auto
-done
-
-text \<open>An example of fun: beyond one equation per constructor\<close>
-
-fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"sep a [] = []" |
-"sep a [x] = [x]" |
-"sep a (x#y#zs) = x # a # sep a (y#zs)"
-
-value "sep a [x,y,z]"
-
-end
diff --git a/lectures/lec10-isabelle/lecture10-isabelle.pdf b/lectures/lec10-isabelle/lecture10-isabelle.pdf
deleted file mode 100644
index 31eb73d3f36d731fff8c1a7690bc34205e88dbbe..0000000000000000000000000000000000000000
Binary files a/lectures/lec10-isabelle/lecture10-isabelle.pdf and /dev/null differ