theory Exercise09
  imports Main
begin

text \<open>Many of the types and algorithms exist already in the
  standard Isabelle library. We hide existing constants and develop
  everything from scratch.\<close>

hide_const plus times 

(* this is a comment *)

text \<open>Proofs from the lecture\<close>

datatype Nat = Zero | Succ Nat

fun plus :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat" where
  "plus Zero y = y" 
| "plus (Succ x) y = Succ (plus x y)" 


fun times :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat" where
  "times Zero y = Zero" 
| "times (Succ x) y = plus y (times x y)" 

(* we prove the lemma and via [simp] tell Isabelle to always use it for simplification *)
lemma Zero_right_neutral[simp]: "plus x Zero = x" 
  by (induction x) simp_all

(* the next property we do not add for global simplifications, i.e., no [simp] attribute *)
lemma plus_right_Succ: "plus x (Succ y) = Succ (plus x y)" 
  by (induction x arbitrary: y) simp_all

(* the next lemma is in a style where we locally step through the proof by 
   a sequence of apply-commands, finalized with "done" *)
lemma plus_comm: "plus x y = plus y x" 
proof (induction x arbitrary: y)
  (* click in the output window in the blue part to get an outline after the induction method *)
  case Zero
  then show ?case by simp
next
  case (Succ x y)
  (* IH is made available via "then show", "using Succ.IH" or "simp add: Succ.IH" *)
  (* one can inspect it via thm *)
  thm Succ.IH
  show ?case 
    apply simp
    apply (simp add: Succ.IH) (* locally use IH *)
    apply (simp add: plus_right_Succ) (* locally use lemma in this proof-step *)
    done (* close proof via done *)
qed 

(* we now perform a proof by a sequence of equalities with explicit intermediate terms;
   such a proof might be necessary, if unrestricted simplification does too much *)
lemma plus_comm2: "plus x y = plus y x" 
proof (induction x arbitrary: y)
  case (Succ x y)
  have "plus (Succ x) y = Succ (plus x y)" by simp (* initial equation *)
  also have "\<dots> = Succ (plus y x)" using Succ.IH by simp (* further equation with "also have" *)
  also have "\<dots> = plus y (Succ x)" by (simp add: plus_right_Succ)
  finally show ?case by simp (* "finally" combines all equations by transitivity *)
qed simp_all (* remaining cases (here: Zero) are solved by simp_all *)




section \<open>Exercise 1\<close>

text \<open>Prove the following lemma. If you require some intermediate lemma of the form 
  "times x (Succ y) = ...", then do NOT add a [simp] attribute.\<close>
lemma times_comm: "times x y = times y x" sorry



section \<open>Exercise 2\<close>

fun sum_nums :: "Nat \<Rightarrow> Nat" where
  "sum_nums Zero = Zero" 
| "sum_nums (Succ x) = plus (Succ x) (sum_nums x)" 

text \<open>Prove the following lemma.\<close>

lemma gauss: "times (sum_nums x) (Succ (Succ Zero)) = times x (Succ x)"
proof (induction x)
  case (Succ x)
  let ?two = "Succ (Succ Zero)" (* a local abbreviation *)
  have "times (sum_nums (Succ x)) ?two = times (plus (Succ x) (sum_nums x)) ?two" by simp
  (* adjust the (number of) intermediate expressions as you like *)
  also have "\<dots> = some_intermediate_expression_1" sorry
  also have "\<dots> = some_intermediate_expression_2" sorry
  also have "\<dots> = some_intermediate_expression_3" sorry
  also have "\<dots> = times (Succ x) (Succ (Succ x))" sorry
  finally show ?case by simp
qed simp

end