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)", without using "case" *)
lemma "length (tl xs) = length xs - 1"
proof(cases xs)
oops

(* isar style, using case *)
lemma "length (tl xs) = length xs - 1"
proof(cases xs)
oops

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, without using "case" *)
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" (is "?P n") for n :: nat
proof(induct n)
oops

(* isar style, using case *)
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" for n::nat
proof(induct n)
oops



lemma "n < n*n + 1" for n::nat
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 "x + y = d + (c::nat)"
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 blah
proof -
  fix a b
  have "a < (b::nat)" sorry
  also
  have "b < a" sorry
  finally
  show blah .
qed


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

thm notE
declare notE [trans]

lemma foo
proof -
  have "\<not>P" sorry
  also
  have "P" sorry
  finally
  show foo .
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)\<^sup>2 \<le> 2*(a\<^sup>2 + b\<^sup>2)" for a :: int
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