theory week07B_demo
imports
  Complex_Main 
  "~~/src/HOL/Library/RBT_Impl"
begin

text {* Sledgehammer setup *}
sledgehammer_params [provers = e spass z3 cvc4, timeout = 10]


text {* Quickcheck setup *}
declare [[quickcheck_narrowing_active = false, quickcheck_size = 5]]


section{* Standard Proof Automation *}

subsection{* Simplification & Co *}

lemma "length(xs @ xs) = 2 * length xs"
using [[simp_trace]]
by simp

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
try0
by fastforce


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



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

lemma "(R \<inter> S)^* \<subseteq> R^*"
try0
oops


section {* Sledgehammer *}

lemma "xs = Nil \<or> xs = Cons (hd xs) (tl xs)"
try0
sledgehammer
oops

lemma "y = x * k \<Longrightarrow> gcd (x::int) y = abs x"
sledgehammer
sorry

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

lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
sledgehammer
sorry 

lemma "(X = Y \<inter> Z) = (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
sledgehammer [isar_proof]
(* sledgehammer [isar_proof, compress=3] *)
sorry



section {* Quickcheck *}

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

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


subsection {* Quantifiers *}

text {* Typical beginner 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)"
quickcheck
oops

lemma "(\<forall>x :: nat. \<exists>y :: nat. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
quickcheck
nitpick
(*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"
quickcheck
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"
quickcheck
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"
quickcheck
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"
quickcheck
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"
quickcheck 
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
nitpick
quickcheck[narrowing, size = 6]
oops


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::linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
  del_from_right :: "('a::linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
  del :: "('a::linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
  "del x rbt.Empty = rbt.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 *)
quickcheck
quickcheck[random,size=20]
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

end