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