theory week10A_demo
imports Aux
begin

section{* Standard Proof Automation *}


subsection{* Simplification & Co *}

lemma "length(xs @ xs) = 2 * length xs"
by simp

text{* May need additional lemmas: *}

lemma "(xs @ ys) ! (length xs) = ys!0"
by(simp add: nth_append)

text{* Beyond simp: *}

lemma "\<lbrakk> \<forall>xs\<in>A. length xs \<le> 3;  \<forall>xs\<in>B. length xs \<ge> 2 \<rbrakk>
  \<Longrightarrow> \<forall>xs \<in> A \<inter> B. length xs \<in> {2,3}"
apply simp
try_methods
sorry


subsection{* Logic & sets *}

lemma "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
by blast

lemma "(\<Union>i \<in> I \<inter> J. M i) \<subseteq> (\<Union>i\<in>I. M i) \<inter> (\<Union>i\<in>J. M i)"
by blast


subsection{* Arithmetic *}

lemma "\<forall> (k::nat) > 119. \<exists> i j. k = 9*i + 16*j"
by arith

lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
by algebra


subsection{* Transitive closure *}

lemma "R^* \<subseteq> (R \<union> S)^*"
by regexp

text{* But there is always a limit: *}

lemma "(R \<inter> S)^* \<subseteq> R^*"
try_methods
sledgehammer
by (metis inf_le1 rtrancl_mono)
sorry


section {* Sledgehammer *}

lemma "xs = Nil \<or> xs = Cons (hd xs) (tl xs)"
try_methods (* fails *)
sledgehammer
sorry

lemma "y = x * k \<Longrightarrow> gcd (x\<Colon>int) y = abs x"
sledgehammer
sledgehammer [spass, isar_proof]
sorry

lemma "xs = ys @ xs @ ys \<Longrightarrow> ys = []"
sledgehammer
sorry


section {* Quickcheck *}

lemma "rev (xs @ ys) = rev xs @ rev ys"
oops

lemma "map (f o g) xs = map g (map f xs)"
oops


subsection {* Quantifiers *}

text {* Typical student errors:
  Existential and Universal Quantifiers can be swapped...
  ... but not this way. *}

lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
oops

lemma "(\<forall>x :: nat. \<exists>y :: nat. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
(*quickcheck -- fails, because the natural numbers are infinite *)
(*nitpick only finds a potential one *)
oops


subsection {* Inequalities on reals *}

(* we switch off support for printing functions, but obtain a faster execution for the next examples *)
declare [[quickcheck_full_support = false]]

text {*
  An example about inequalities on real numbers:
*}


lemma "\<lbrakk> (a::real) > 0; b > 0; c > 0;
         a * a \<le> b * (c + 1); b \<le> 4 * c \<rbrakk>
       \<Longrightarrow> (a - 1) * (a - 1) < b * c"
oops

text {*
  So, it does not hold, for arbitrary positive rational numbers.
  In the context, the lemma was used, the user actually knew that a >= 1.
*}
lemma "\<lbrakk> (a::real) \<ge> 1; b > 0; c > 0;
         a * a \<le> b * (c + 1); b \<le> 4 * c \<rbrakk>
       \<Longrightarrow> (a - 1) * (a - 1) < b * c"
oops

text {* But let us now explore what the exact constraints and bounds are:
First, we drop the constraints b > 0  and c > 0.
*}

lemma "\<lbrakk> (a::real) \<ge> 1;
         a * a \<le> b * (c + 1); b \<le> 4 * c \<rbrakk>
       \<Longrightarrow> (a - 1) * (a - 1) < b * c"
oops

text {*
Secondly, we determine an exact bound for a. 1/2 was a counterexample beforehand -- is there
another larger one?
*}

lemma "\<lbrakk> (a::real) > 1/2;
         a * a \<le> b * (c + 1); b \<le> 4 * c \<rbrakk>
       \<Longrightarrow> (a - 1) * (a - 1) < b * c"
oops

text {* But is there a counterexample with a > 3/4 ?? *}

lemma "\<lbrakk> (a::real) > 3/4;
         a * a \<le> b * (c + 1); b \<le> 4 * c \<rbrakk>
       \<Longrightarrow> (a - 1) * (a - 1) < b * c"
oops

text {* Is 3/4 a tight bound for a? Let's try. *}

lemma "\<lbrakk> (a::real) \<ge> 3/4;
         a * a \<le> b * (c + 1); b \<le> 4 * c \<rbrakk>
       \<Longrightarrow> (a - 1) * (a - 1) < b * c"
quickcheck
quickcheck[size = 10]
oops

text{* More numeric curiosities: *}

definition prime :: "nat \<Rightarrow> bool" where
"prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m<p. p mod m = 0 \<longrightarrow> m = 1))"

lemma "prime(n^2 + n + 41)"
quickcheck
oops

lemma "\<forall>n<40. prime(n^2 + n + 41)"
by eval

declare [[quickcheck_full_support = true]]


subsection {* Narrowing-based Quickcheck *}

text {*
  The example with quantifiers from before:
  With symbolic execution we can actually find
  a counterexample even on infinite domains.
*}

lemma "(\<forall>x::nat. \<exists>y::nat. P x y) \<longrightarrow> (\<exists>y'. \<forall>x'. P x' y')"
(*quickcheck -- fails, because the natural numbers are infinite *)
(*nitpick only finds a potential one *)
quickcheck[narrowing, size = 6]
oops

text {* Some times it just helps to have another evaluation strategy:
Lazy evaluation instead of eager evaluation.
*}

lemma
  "length (dropWhile P xs) < length xs \<Longrightarrow>
   \<not> P (xs ! length (takeWhile P xs))"
quickcheck[exhaustive]
quickcheck[narrowing]
oops

(*
quickcheck[exhaustive] fails, because it has a strict evaluation.
So even for P = \<lambda>_. True, it will evaluate its argument, which leads to an run time exception with nth -- hence we soundly assume we don't know anything about this evaluation.
The narrowing-based quickcheck uses lazy evaluation, evaluates to False without evaluation of its argument.
*)


text {* a slightly flawed delete operation on Red-Black-Trees *}

(* replaced balance_left by balance_right in del_from_left x (Branch B lt z v rt) y s b *)
fun
  del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
  del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
  del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
  "del x Empty = Empty" |
  "del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))" |
  "del_from_left x (Branch RBT_Impl.B lt z v rt) y s b = balance_right (del x (Branch RBT_Impl.B lt z v rt)) y s b" |
  "del_from_left x a y s b = Branch RBT_Impl.R (del x a) y s b" |
  "del_from_right x a y s (Branch RBT_Impl.B lt z v rt) = balance_right a y s (del x (Branch RBT_Impl.B lt z v rt))" | 
  "del_from_right x a y s b = Branch RBT_Impl.R a y s (del x b)"

definition delete where
  delete_def: "delete k t = paint RBT_Impl.B (del k t)"

theorem delete_is_rbt:
  "is_rbt (t :: (int,int)rbt) \<Longrightarrow> is_rbt (delete k t)"
quickcheck[narrowing] (* compare with exhaustive and random *)
oops

section {* Nitpick *}

lemma "(R \<union> S)^* = R^* \<union> S^*"
nitpick
oops

lemma "acyclic R \<Longrightarrow> acyclic S \<Longrightarrow> acyclic(R \<union> S)"
nitpick
oops

lemma "append xs ys = xs \<longleftrightarrow> ys = Nil"
nitpick
oops

lemma "lappend xs ys = xs \<longleftrightarrow> ys = LNil"
nitpick
oops

end