theory week08A_demo_Isar2 imports Main begin

\<comment> \<open> ----------------------------------------------------------------\<close>

text \<open> Isar, case distinction \<close>

declare length_tl[simp del]

(* isar style, just using "proof (cases xs)", not using case *)
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

(* isar style, using case *)
lemma "length (tl xs) = length xs - 1"
proof(cases xs)
  case Nil
  thus ?thesis by simp
next
  case (Cons y ys)
  from Cons show ?thesis by simp
qed


text \<open> structural induction \<close>

(* apply style *)
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)"
  apply(induct n, simp_all)
  done

(* isar style, not using case *)
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)" (is "?P n")
proof(induct n)
  show "?P 0" by simp
next
  fix n
  assume "?P n"
  thus "?P (Suc n)" by simp
qed

(* isar style, using case *)
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1::nat)"
proof(induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  from Suc show ?case by simp
qed


lemma
  fixes n::nat
  shows "n < n*n + 1"
proof(induct n)
  case 0 show ?case by simp
next
  case (Suc n) thus ?case by simp
qed

text \<open> induction with @{text"\<And>"} or @{text"\<Longrightarrow>"} \<close>

lemma
  assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
  shows "P (n::nat)"
proof(rule A)
  show "\<And>m. m < n \<Longrightarrow> P m"
  proof(induct n)
    case 0
    thus ?case by simp
  next
    case (Suc n)
    show ?case
    proof(cases)
      assume eq: "m = n"
      from A Suc have "P n" by blast
      with eq show "P m" by simp
    next
      assume neq: "m \<noteq> n"
      from Suc neq have "m < n" by arith
      thus "P m" by(rule Suc)
    qed
  qed
qed


\<comment> \<open> ----------------------------------------------------------------\<close>

text \<open> calculational reasoning\<close>

text \<open> "also/finally" \<close>


lemma right_inverse:
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
  fixes inv :: "'a \<Rightarrow> 'a"    ("(_\<^sup>-)" [1000] 999)
  fixes one :: 'a    ("\<one>")

  assumes assoc: "\<And>x y z. (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
  assumes left_inv: "\<And>x. x\<^sup>- \<cdot> x = \<one>"
  assumes left_one: "\<And>x. \<one> \<cdot> x = x"

  shows "x \<cdot> x\<^sup>- = \<one>"
proof -
  have "x \<cdot> x\<^sup>- = \<one> \<cdot> (x \<cdot> x\<^sup>-)" by (simp only: left_one)
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>- \<cdot> x \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (x\<^sup>- \<cdot> x) \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> \<one> \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (\<one> \<cdot> x\<^sup>-)" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>-" by (simp only: left_one)
  also have "\<dots> = \<one>" by (simp only: left_inv)
  finally show ?thesis .
qed


print_trans_rules

text \<open>mixed operators\<close>

lemma "1 < (5::nat)"
proof -
  have "1 < Suc 1" by simp
  also
  have "Suc 1 = 2" by simp
  also
  have "2 \<le> (5::nat)" by simp
  finally
  show ?thesis .
qed

text \<open>substitution\<close>

lemma blah
proof -
  have "2*y + 2*y = (0::nat)" sorry
  also
  have "2*y = x" sorry
  also
  have "(0::nat) \<le> 2*c" sorry
  also
  have "c = d div 2" sorry
  also
  have "d = 2 * x" sorry
  finally
  have "x + x \<le> 2 * x " by simp
oops

print_trans_rules

text \<open>antisymmetry\<close>

lemma blub
proof -
  have "a < (b::nat)" sorry
  also
  have "b < a" sorry
  finally
  show blub .
qed


text \<open>notE as trans\<close>

thm notE
declare notE [trans]

lemma blub
proof -
  have "\<not>P" sorry
  also
  have "P" sorry
  finally
  show blub .
qed


text \<open>monotonicity \<close>

lemma "a+b \<le> 2*a + 2*(b::nat)"
proof -
  have "a + b \<le> 2*a + b" by simp
  also
  have "b \<le> 2*b" by simp
  finally
  show "a+b \<le> 2*a + 2*b" by simp
qed

lemma "a+b \<le> 2*a + 2*(b::nat)"
proof -
  have "a + b \<le> 2*a + b" by simp
  also
  have "b \<le> 2*b" by simp
  also
  have "\<And>x y. x \<le> y \<Longrightarrow> 2 * a + x \<le> 2 * a + y" by simp
  ultimately
  show "a+b \<le> 2*a + 2*(b::nat)" .
qed

declare algebra_simps [simp]
lemma "(a+b::int)\<^sup>2 \<le> 2*(a\<^sup>2 + b\<^sup>2)"
proof -
       have "(a+b)\<^sup>2 \<le> (a+b)\<^sup>2 + (a-b)\<^sup>2" by simp thm numeral_2_eq_2
  also have "(a+b)\<^sup>2 \<le> a\<^sup>2 + b\<^sup>2 + 2*a*b" by (simp add: numeral_2_eq_2)
  also have "(a-b)\<^sup>2 = a\<^sup>2 + b\<^sup>2 - 2*a*b" by (simp add:numeral_2_eq_2)
  finally show ?thesis by simp
qed

\<comment> \<open> ----------------------------------------------------------------\<close>

end