(* Title: HOLCF/Domain.thy ID: $Id: Domain.thy,v 1.8 2005/07/08 00:41:35 huffman Exp $ Author: Brian Huffman *) header {* Domain package *} theory Domain imports Ssum Sprod Up One Tr Fixrec (* files ("domain/library.ML") ("domain/syntax.ML") ("domain/axioms.ML") ("domain/theorems.ML") ("domain/extender.ML") ("domain/interface.ML") *) begin defaultsort pcpo subsection {* Continuous isomorphisms *} text {* A locale for continuous isomorphisms *} locale iso = fixes abs :: "'a -> 'b" fixes rep :: "'b -> 'a" assumes abs_iso [simp]: "rep·(abs·x) = x" assumes rep_iso [simp]: "abs·(rep·y) = y" lemma (in iso) swap: "iso rep abs" by (rule iso.intro [OF rep_iso abs_iso]) lemma (in iso) abs_strict: "abs·⊥ = ⊥" proof - have "⊥ \<sqsubseteq> rep·⊥" .. hence "abs·⊥ \<sqsubseteq> abs·(rep·⊥)" by (rule monofun_cfun_arg) hence "abs·⊥ \<sqsubseteq> ⊥" by simp thus ?thesis by (rule UU_I) qed lemma (in iso) rep_strict: "rep·⊥ = ⊥" by (rule iso.abs_strict [OF swap]) lemma (in iso) abs_defin': "abs·z = ⊥ ==> z = ⊥" proof - assume A: "abs·z = ⊥" have "z = rep·(abs·z)" by simp also have "… = rep·⊥" by (simp only: A) also note rep_strict finally show "z = ⊥" . qed lemma (in iso) rep_defin': "rep·z = ⊥ ==> z = ⊥" by (rule iso.abs_defin' [OF swap]) lemma (in iso) abs_defined: "z ≠ ⊥ ==> abs·z ≠ ⊥" by (erule contrapos_nn, erule abs_defin') lemma (in iso) rep_defined: "z ≠ ⊥ ==> rep·z ≠ ⊥" by (erule contrapos_nn, erule rep_defin') lemma (in iso) iso_swap: "(x = abs·y) = (rep·x = y)" proof assume "x = abs·y" hence "rep·x = rep·(abs·y)" by simp thus "rep·x = y" by simp next assume "rep·x = y" hence "abs·(rep·x) = abs·y" by simp thus "x = abs·y" by simp qed subsection {* Casedist *} lemma ex_one_defined_iff: "(∃x. P x ∧ x ≠ ⊥) = P ONE" apply safe apply (rule_tac p=x in oneE) apply simp apply simp apply force done lemma ex_up_defined_iff: "(∃x. P x ∧ x ≠ ⊥) = (∃x. P (up·x))" apply safe apply (rule_tac p=x in upE) apply simp apply fast apply (force intro!: up_defined) done lemma ex_sprod_defined_iff: "(∃y. P y ∧ y ≠ ⊥) = (∃x y. (P (:x, y:) ∧ x ≠ ⊥) ∧ y ≠ ⊥)" apply safe apply (rule_tac p=y in sprodE) apply simp apply fast apply (force intro!: spair_defined) done lemma ex_sprod_up_defined_iff: "(∃y. P y ∧ y ≠ ⊥) = (∃x y. P (:up·x, y:) ∧ y ≠ ⊥)" apply safe apply (rule_tac p=y in sprodE) apply simp apply (rule_tac p=x in upE) apply simp apply fast apply (force intro!: spair_defined) done lemma ex_ssum_defined_iff: "(∃x. P x ∧ x ≠ ⊥) = ((∃x. P (sinl·x) ∧ x ≠ ⊥) ∨ (∃x. P (sinr·x) ∧ x ≠ ⊥))" apply (rule iffI) apply (erule exE) apply (erule conjE) apply (rule_tac p=x in ssumE) apply simp apply (rule disjI1, fast) apply (rule disjI2, fast) apply (erule disjE) apply (force intro: sinl_defined) apply (force intro: sinr_defined) done lemma exh_start: "p = ⊥ ∨ (∃x. p = x ∧ x ≠ ⊥)" by auto lemmas ex_defined_iffs = ex_ssum_defined_iff ex_sprod_up_defined_iff ex_sprod_defined_iff ex_up_defined_iff ex_one_defined_iff text {* Rules for turning exh into casedist *} lemma exh_casedist0: "[|R; R ==> P|] ==> P" (* like make_elim *) by auto lemma exh_casedist1: "((P ∨ Q ==> R) ==> S) ≡ ([|P ==> R; Q ==> R|] ==> S)" by rule auto lemma exh_casedist2: "(∃x. P x ==> Q) ≡ (!!x. P x ==> Q)" by rule auto lemma exh_casedist3: "(P ∧ Q ==> R) ≡ (P ==> Q ==> R)" by rule auto lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 subsection {* Setting up the package *} ML {* val iso_intro = thm "iso.intro"; val iso_abs_iso = thm "iso.abs_iso"; val iso_rep_iso = thm "iso.rep_iso"; val iso_abs_strict = thm "iso.abs_strict"; val iso_rep_strict = thm "iso.rep_strict"; val iso_abs_defin' = thm "iso.abs_defin'"; val iso_rep_defin' = thm "iso.rep_defin'"; val iso_abs_defined = thm "iso.abs_defined"; val iso_rep_defined = thm "iso.rep_defined"; val iso_iso_swap = thm "iso.iso_swap"; val exh_start = thm "exh_start"; val ex_defined_iffs = thms "ex_defined_iffs"; val exh_casedist0 = thm "exh_casedist0"; val exh_casedists = thms "exh_casedists"; *} end
lemma swap:
iso abs rep ==> iso rep abs
lemma abs_strict:
iso abs rep ==> abs·UU = UU
lemma rep_strict:
iso abs rep ==> rep·UU = UU
lemma abs_defin':
[| iso abs rep; abs·z = UU |] ==> z = UU
lemma rep_defin':
[| iso abs rep; rep·z = UU |] ==> z = UU
lemma abs_defined:
[| iso abs rep; z ≠ UU |] ==> abs·z ≠ UU
lemma rep_defined:
[| iso abs rep; z ≠ UU |] ==> rep·z ≠ UU
lemma iso_swap:
iso abs rep ==> (x = abs·y) = (rep·x = y)
lemma ex_one_defined_iff:
(∃x. P x ∧ x ≠ UU) = P ONE
lemma ex_up_defined_iff:
(∃x. P x ∧ x ≠ UU) = (∃x. P (up·x))
lemma ex_sprod_defined_iff:
(∃y. P y ∧ y ≠ UU) = (∃x y. (P (:x, y:) ∧ x ≠ UU) ∧ y ≠ UU)
lemma ex_sprod_up_defined_iff:
(∃y. P y ∧ y ≠ UU) = (∃x y. P (:up·x, y:) ∧ y ≠ UU)
lemma ex_ssum_defined_iff:
(∃x. P x ∧ x ≠ UU) = ((∃x. P (sinl·x) ∧ x ≠ UU) ∨ (∃x. P (sinr·x) ∧ x ≠ UU))
lemma exh_start:
p = UU ∨ (∃x. p = x ∧ x ≠ UU)
lemmas ex_defined_iffs:
(∃x. P x ∧ x ≠ UU) = ((∃x. P (sinl·x) ∧ x ≠ UU) ∨ (∃x. P (sinr·x) ∧ x ≠ UU))
(∃y. P y ∧ y ≠ UU) = (∃x y. P (:up·x, y:) ∧ y ≠ UU)
(∃y. P y ∧ y ≠ UU) = (∃x y. (P (:x, y:) ∧ x ≠ UU) ∧ y ≠ UU)
(∃x. P x ∧ x ≠ UU) = (∃x. P (up·x))
(∃x. P x ∧ x ≠ UU) = P ONE
lemmas ex_defined_iffs:
(∃x. P x ∧ x ≠ UU) = ((∃x. P (sinl·x) ∧ x ≠ UU) ∨ (∃x. P (sinr·x) ∧ x ≠ UU))
(∃y. P y ∧ y ≠ UU) = (∃x y. P (:up·x, y:) ∧ y ≠ UU)
(∃y. P y ∧ y ≠ UU) = (∃x y. (P (:x, y:) ∧ x ≠ UU) ∧ y ≠ UU)
(∃x. P x ∧ x ≠ UU) = (∃x. P (up·x))
(∃x. P x ∧ x ≠ UU) = P ONE
lemma exh_casedist0:
[| R; R ==> P |] ==> P
lemma exh_casedist1:
((P ∨ Q ==> R) ==> S) == ([| P ==> R; Q ==> R |] ==> S)
lemma exh_casedist2:
(∃x. P x ==> Q) == (!!x. P x ==> Q)
lemma exh_casedist3:
(P ∧ Q ==> R) == ([| P; Q |] ==> R)
lemmas exh_casedists:
((P ∨ Q ==> R) ==> S) == ([| P ==> R; Q ==> R |] ==> S)
(∃x. P x ==> Q) == (!!x. P x ==> Q)
(P ∧ Q ==> R) == ([| P; Q |] ==> R)
lemmas exh_casedists:
((P ∨ Q ==> R) ==> S) == ([| P ==> R; Q ==> R |] ==> S)
(∃x. P x ==> Q) == (!!x. P x ==> Q)
(P ∧ Q ==> R) == ([| P; Q |] ==> R)