Theory ISQ_Proof

section ‹ Proof Support for Quantities ›

theory ISQ_Proof
  imports ISQ_Quantities
begin

named_theorems si_transfer

definition magQ :: "'a['u::dim_type, 's::unit_system] ⇒ 'a" (‹⟦_⟧⇩Q›) where
[si_def]: "magQ x = mag (fromQ x)"

definition dimQ :: "'a['u::dim_type, 's::unit_system] ⇒ Dimension" where
[si_def]: "dimQ x = dim (fromQ x)"

lemma quant_eq_iff_mag_eq [si_eq]:
  "x = y ⟷ ⟦x⟧⇩Q = ⟦y⟧⇩Q"
  by (auto simp add: magQ_def, transfer, simp add: eq_unit)

lemma quant_eqI [si_transfer]:
  "⟦x⟧⇩Q = ⟦y⟧⇩Q ⟹ x = y"
  by (simp add: quant_eq_iff_mag_eq)

lemma quant_equiv_iff [si_eq]:
  fixes x :: "'a['u⇩1::dim_type, 's::unit_system]" and y :: "'a['u⇩2::dim_type, 's::unit_system]"
  shows "x ≅⇩Q y ⟷ ⟦x⟧⇩Q = ⟦y⟧⇩Q ∧ QD('u⇩1) = QD('u⇩2)"
proof -
  have "∀t ta. (ta::'a['u⇩2, 's]) = t ∨ mag (fromQ ta) ≠ mag (fromQ t)"
    by (simp add: magQ_def quant_eq_iff_mag_eq)
  then show ?thesis
    by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQ_def)
qed

lemma quant_equivI [si_transfer]:
  fixes x :: "'a['u⇩1::dim_type, 's::unit_system]" and y :: "'a['u⇩2::dim_type, 's::unit_system]"
  assumes "QD('u⇩1) = QD('u⇩2)" "QD('u⇩1) = QD('u⇩2) ⟹ ⟦x⟧⇩Q = ⟦y⟧⇩Q"
  shows "x ≅⇩Q y"
  using assms quant_equiv_iff by blast
  
lemma quant_le_iff_magn_le [si_eq]:
  "x ≤ y ⟷ ⟦x⟧⇩Q ≤ ⟦y⟧⇩Q"
  by (auto simp add: magQ_def; (transfer, simp))

lemma quant_leI [si_transfer]:
  "⟦x⟧⇩Q ≤ ⟦y⟧⇩Q ⟹ x ≤ y"
  by (simp add: quant_le_iff_magn_le)

lemma quant_less_iff_magn_less [si_eq]:
  "x < y ⟷ ⟦x⟧⇩Q < ⟦y⟧⇩Q"
  by (auto simp add: magQ_def; (transfer, simp))

lemma quant_lessI [si_transfer]:
  "⟦x⟧⇩Q < ⟦y⟧⇩Q ⟹ x < y"
  by (simp add: quant_less_iff_magn_less)

lemma magQ_zero [si_eq]: "⟦0⟧⇩Q = 0"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_one [si_eq]: "⟦1⟧⇩Q = 1"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_plus [si_eq]: "⟦x + y⟧⇩Q = ⟦x⟧⇩Q + ⟦y⟧⇩Q"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_minus [si_eq]: "⟦x - y⟧⇩Q = ⟦x⟧⇩Q - ⟦y⟧⇩Q"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_uminus [si_eq]: "⟦- x⟧⇩Q = - ⟦x⟧⇩Q"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_scaleQ [si_eq]: "⟦x *⇩Q y⟧⇩Q = x * ⟦y⟧⇩Q"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_qtimes [si_eq]: "⟦x ❙⋅ y⟧⇩Q = ⟦x⟧⇩Q ⋅ ⟦y⟧⇩Q"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_qinverse [si_eq]: "⟦x⇧-⇧𝟭⟧⇩Q = inverse ⟦x⟧⇩Q"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_qdivivide [si_eq]: "⟦(x::('a::field)[_,_]) ❙/ y⟧⇩Q = ⟦x⟧⇩Q / ⟦y⟧⇩Q"
  by (simp add: magQ_def, transfer, simp add: field_class.field_divide_inverse)

lemma magQ_numeral [si_eq]: "⟦numeral n⟧⇩Q = numeral n"
  apply (induct n, simp_all add: si_def)
  apply (metis magQ_def magQ_one)
  apply (metis magQ_def magQ_plus numeral_code(2))
  apply (metis magQ_def magQ_one magQ_plus numeral_code(3))
  done

lemma magQ_coerce [si_eq]: 
  fixes q :: "'a['d⇩1::dim_type, 's::unit_system]" and t :: "'d⇩2::dim_type itself"
  assumes "QD('d⇩1) = QD('d⇩2)"
  shows "⟦coerceQuantT t q⟧⇩Q = ⟦q⟧⇩Q"
  by (simp add: coerceQuantT_def magQ_def assms, metis assms qequiv.rep_eq updown_eq_iff)

lemma dimQ [simp]: "dimQ(x :: 'a['d::dim_type, 's::unit_system]) = QD('d)"
  by (simp add: dimQ_def, transfer, simp)

text ‹ The following tactic breaks an SI conjecture down to numeric and unit properties ›

method si_simp uses add =
  (rule_tac si_transfer; simp add: add si_eq field_simps)

text ‹ The next tactic additionally compiles the semantics of the underlying units ›

method si_calc uses add = 
  (si_simp add: add; simp add: si_def add)

lemma "QD(N ⋅ Θ ⋅ N) = QD(Θ ⋅ N⇧2)" by (simp add: si_eq si_def)
  
end