Theory C-Meet

theory "C-Meet"
imports C "HOLCF-Meet"
begin

instantiation C :: Finite_Meet_cpo begin
  fixrec C_meet :: "C → C → C"
    where "C_meet⋅(C⋅a)⋅(C⋅b) = C⋅(C_meet⋅a⋅b)"
  
  lemma[simp]: "C_meet⋅⊥⋅y = ⊥" "C_meet⋅x⋅⊥ = ⊥" by (fixrec_simp, cases x, fixrec_simp+)  

  instance
  apply standard
  proof(intro exI conjI strip)
    fix x y
    {
      fix t
      have "(t ⊑ C_meet⋅x⋅y) = (t ⊑ x ∧ t ⊑ y)"
      proof (induct t rule:C.take_induct)
        fix n
        show "(C_take n⋅t ⊑ C_meet⋅x⋅y) = (C_take n⋅t ⊑ x ∧ C_take n⋅t ⊑ y)"
        proof (induct n arbitrary: t x y rule:nat_induct)
          case 0 thus ?case by auto
          next
          case (Suc n t x y)
            with C.nchotomy[of t] C.nchotomy[of x] C.nchotomy[of y]
            show ?case by fastforce
        qed
     qed auto
    } note * = this
    show "C_meet⋅x⋅y ⊑ x" using * by auto
    show "C_meet⋅x⋅y ⊑ y" using * by auto
    fix z
    assume "z ⊑ x" and "z ⊑ y"
    thus "z ⊑ C_meet⋅x⋅y" using * by auto
qed
end

lemma C_meet_is_meet: "(z ⊑ C_meet⋅x⋅y) = (z ⊑ x ∧ z ⊑ y)"
proof (induct z rule:C.take_induct)
  fix n
  show "(C_take n⋅z ⊑ C_meet⋅x⋅y) = (C_take n⋅z ⊑ x ∧ C_take n⋅z ⊑ y)"
  proof (induct n arbitrary: z x y rule:nat_induct)
    case 0 thus ?case by auto
    next
    case (Suc n z x y) thus ?case
      apply -
      apply (cases z, simp)
      apply (cases x, simp)
      apply (cases y, simp)
      apply (fastforce simp add: cfun_below_iff)
      done
  qed
qed auto

instance C :: cont_binary_meet
proof (standard, goal_cases)
  have [simp]:"⋀ x y. x ⊓ y = C_meet⋅x⋅y"
    using C_meet_is_meet
    by (blast intro: is_meetI)
  case 1 thus ?case
    by (simp add: ch2ch_Rep_cfunR contlub_cfun_arg contlub_cfun_fun)
qed

lemma [simp]: "C⋅r ⊓ r = r"
  by (auto intro: is_meetI simp add: below_C)

lemma [simp]: "r ⊓ C⋅r = r"
  by (auto intro: is_meetI simp add: below_C)

lemma [simp]: "C⋅r ⊓ C⋅r' = C⋅(r ⊓ r')"
  apply (rule is_meetI)
  apply (metis below_refl meet_below1 monofun_cfun_arg)
  apply (metis below_refl meet_below2 monofun_cfun_arg)
  apply (case_tac a)
  apply auto
  by (metis meet_above_iff)

end