# Theory Domain

Up to index of Isabelle/HOLCF

theory Domain
imports Ssum Sprod Up One Tr Fixrec
begin

    (*  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

### Continuous isomorphisms

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)

### Casedist

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)

### Setting up the package