Theory Utils

theory Utils
imports
  Main
  ReadShow
  "HOL-Library.Finite_Map"
  "HOL-Eisbach.Eisbach"
begin

section ‹Some Basic Lemmas for Finite Maps›

lemma fmfinite: "finite ({(ad, x). fmlookup y ad = Some x})"
proof -
  have "{(ad, x). fmlookup y ad = Some x} ⊆ dom (fmlookup y) × ran (fmlookup y)"
  proof
    fix x assume "x ∈ {(ad, x). fmlookup y ad = Some x}"
    then have "fmlookup y (fst x) = Some (snd x)" by auto
    then have "fst x ∈ dom (fmlookup y)" and "snd x ∈ ran (fmlookup y)" using Map.ranI by (blast,metis)
    then show "x ∈ dom (fmlookup y) × ran (fmlookup y)" by (simp add: mem_Times_iff)
  qed
  thus ?thesis by (simp add: finite_ran finite_subset)
qed

lemma fmlookup_finite:
  fixes f :: "'a ⇒ 'a"
    and y :: "('a, 'b) fmap"
  assumes "inj_on (λ(ad, x). (f ad, x)) {(ad, x). (fmlookup y ∘ f) ad = Some x}"
  shows "finite {(ad, x). (fmlookup y ∘ f) ad = Some x}"
proof (cases rule: inj_on_finite[OF assms(1), of "{(ad, x)|ad x. (fmlookup y) ad = Some x}"])
  case 1
  then show ?case by auto
next
  case 2
  then have *: "finite {(ad, x) |ad x. fmlookup y ad = Some x}" using fmfinite[of y] by simp
  show ?case using finite_image_set[OF *, of "λ(ad, x). (ad, x)"] by simp
qed

lemma balance_inj: "inj_on (λ(ad, x). (ad + z::String.literal,x)) {(ad, x). (fmlookup y ∘ f) ad = Some x}"
proof
  fix v v' assume asm1: "v ∈ {(ad, x). (fmlookup y ∘ f) ad = Some x}" and asm2: "v' ∈ {(ad, x). (fmlookup y ∘ f) ad = Some x}"
  and *:"(case v of (ad, x) ⇒ (ad + z,x)) = (case v' of (ad, x) ⇒ (ad + z,x))"
  then obtain ad ad' x x' where **: "v = (ad,x)" and ***: "v'=(ad',x')" by auto
  moreover from * ** *** have "ad + z = ad' + z" by simp
  with * ** have "ad = ad'" using String_Cancel[of ad z ad' ] by simp
  moreover from asm1 asm2 ** *** have "(fmlookup y ∘ f) ad = Some x" and "(fmlookup y ∘ f) ad' = Some x'" by auto
  with calculation(3) have "x=x'" by simp
  ultimately show "v=v'" by simp
qed

section ‹Some Basic Proof Methods›

method solve methods m = (m ; fail)

named_theorems intros
declare conjI[intros] impI[intros] allI[intros] ballI[intros]
method intros = (rule intros; intros?)

named_theorems elims
method elims = ((rule intros | erule elims); elims?)
declare conjE[elims]

end