Quelle  Domain_Proofs.thy

(*  Title:      HOL/HOLCF/ex/Domain_Proofs.thy
  Author: Brian Huffman
*)

section ‹Internal domain package proofs done manually›

theory Domain_Proofs
imports HOLCF
begin

(*
 
 The definitions and proofs below are for the following recursive
 datatypes:
 
 domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
  and 'a bar = Bar (lazy "'a baz → tr")
  and 'a baz = Baz (lazy "'a foo convex_pd → tr")
 
*)

(********************************************************************)

subsection ‹Step 1: Define the new type combinators›

text ‹Start with the one-step non-recursive version›

definition
  foo_bar_baz_deflF ::
    "udom defl → udom defl × udom defl × udom defl → udom defl × udom defl × udom defl"
where
  "foo_bar_baz_deflF = (Λ a. Abs_cfun (λ(t1, t2, t3).
    ( ssum_defl⋅DEFL(one)⋅(sprod_defl⋅(u_defl⋅a)⋅(u_defl⋅t2))
    , u_defl⋅(sfun_defl⋅(u_defl⋅t3)⋅DEFL(tr))
    , u_defl⋅(sfun_defl⋅(u_defl⋅(convex_defl⋅t1))⋅DEFL(tr)))))"

lemma foo_bar_baz_deflF_beta:
  "foo_bar_baz_deflF⋅a⋅t =
    ( ssum_defl⋅DEFL(one)⋅(sprod_defl⋅(u_defl⋅a)⋅(u_defl⋅(fst (snd t))))
    , u_defl⋅(sfun_defl⋅(u_defl⋅(snd (snd t)))⋅DEFL(tr))
    , u_defl⋅(sfun_defl⋅(u_defl⋅(convex_defl⋅(fst t)))⋅DEFL(tr)))"
unfolding foo_bar_baz_deflF_def
by (simp add: split_def)

text ‹Individual type combinators are projected from the fixed point.›

definition foo_defl :: "udom defl → udom defl"
where "foo_defl = (Λ a. fst (fix⋅(foo_bar_baz_deflF⋅a)))"

definition bar_defl :: "udom defl → udom defl"
where "bar_defl = (Λ a. fst (snd (fix⋅(foo_bar_baz_deflF⋅a))))"

definition baz_defl :: "udom defl → udom defl"
where "baz_defl = (Λ a. snd (snd (fix⋅(foo_bar_baz_deflF⋅a))))"

lemma defl_apply_thms:
  "foo_defl⋅a = fst (fix⋅(foo_bar_baz_deflF⋅a))"
  "bar_defl⋅a = fst (snd (fix⋅(foo_bar_baz_deflF⋅a)))"
  "baz_defl⋅a = snd (snd (fix⋅(foo_bar_baz_deflF⋅a)))"
unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all

text ‹Unfold rules for each combinator.›

lemma foo_defl_unfold:
  "foo_defl⋅a = ssum_defl⋅DEFL(one)⋅(sprod_defl⋅(u_defl⋅a)⋅(u_defl⋅(bar_defl⋅a)))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)

lemma bar_defl_unfold: "bar_defl⋅a = u_defl⋅(sfun_defl⋅(u_defl⋅(baz_defl⋅a))⋅DEFL(tr))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)

lemma baz_defl_unfold: "baz_defl⋅a = u_defl⋅(sfun_defl⋅(u_defl⋅(convex_defl⋅(foo_defl⋅a)))⋅DEFL(tr))"
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)

text "The automation for the previous steps will be quite similar to
how the fixrec package works."

(********************************************************************)

subsection ‹Step 2: Define types, prove class instances›

text ‹Use ‹pcpodef› with the appropriate type combinator.›

pcpodef 'a foo = "defl_set (foo_defl⋅DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)

pcpodef 'a bar = "defl_set (bar_defl⋅DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)

pcpodef 'a baz = "defl_set (baz_defl⋅DEFL('a))"
by (rule defl_set_bottom, rule adm_defl_set)

text ‹Prove rep instance using lemma ‹typedef_rep_class›.\<close>

instantiation foo :: ("domain") "domain"
begin

definition emb_foo :: "'a foo → udom"
where "emb_foo ≡ (Λ x. Rep_foo x)"

definition prj_foo :: "udom → 'a foo"
where "prj_foo ≡ (Λ y. Abs_foo (cast⋅(foo_defl⋅DEFL('a))⋅y))"

definition defl_foo :: "'a foo itself ==> udom defl"
where "defl_foo ≡ λa. foo_defl⋅DEFL('a)"

definition
  "(liftemb :: 'a foo u → udom u) ≡ u_map⋅emb"

definition
  "(liftprj :: udom u → 'a foo u) ≡ u_map⋅prj"

definition
  "liftdefl ≡ λ(t::'a foo itself). liftdefl_of⋅DEFL('a foo)"

instance
apply (rule typedef_domain_class)
apply (rule type_definition_foo)
apply (rule below_foo_def)
apply (rule emb_foo_def)
apply (rule prj_foo_def)
apply (rule defl_foo_def)
apply (rule liftemb_foo_def)
apply (rule liftprj_foo_def)
apply (rule liftdefl_foo_def)
done

end

instantiation bar :: ("domain") "domain"
begin

definition emb_bar :: "'a bar → udom"
where "emb_bar ≡ (Λ x. Rep_bar x)"

definition prj_bar :: "udom → 'a bar"
where "prj_bar ≡ (Λ y. Abs_bar (cast⋅(bar_defl⋅DEFL('a))⋅y))"

definition defl_bar :: "'a bar itself ==> udom defl"
where "defl_bar ≡ λa. bar_defl⋅DEFL('a)"

definition
  "(liftemb :: 'a bar u → udom u) ≡ u_map⋅emb"

definition
  "(liftprj :: udom u → 'a bar u) ≡ u_map⋅prj"

definition
  "liftdefl ≡ λ(t::'a bar itself). liftdefl_of⋅DEFL('a bar)"

instance
apply (rule typedef_domain_class)
apply (rule type_definition_bar)
apply (rule below_bar_def)
apply (rule emb_bar_def)
apply (rule prj_bar_def)
apply (rule defl_bar_def)
apply (rule liftemb_bar_def)
apply (rule liftprj_bar_def)
apply (rule liftdefl_bar_def)
done

end

instantiation baz :: ("domain") "domain"
begin

definition emb_baz :: "'a baz → udom"
where "emb_baz ≡ (Λ x. Rep_baz x)"

definition prj_baz :: "udom → 'a baz"
where "prj_baz ≡ (Λ y. Abs_baz (cast⋅(baz_defl⋅DEFL('a))⋅y))"

definition defl_baz :: "'a baz itself ==> udom defl"
where "defl_baz ≡ λa. baz_defl⋅DEFL('a)"

definition
  "(liftemb :: 'a baz u → udom u) ≡ u_map⋅emb"

definition
  "(liftprj :: udom u → 'a baz u) ≡ u_map⋅prj"

definition
  "liftdefl ≡ λ(t::'a baz itself). liftdefl_of⋅DEFL('a baz)"

instance
apply (rule typedef_domain_class)
apply (rule type_definition_baz)
apply (rule below_baz_def)
apply (rule emb_baz_def)
apply (rule prj_baz_def)
apply (rule defl_baz_def)
apply (rule liftemb_baz_def)
apply (rule liftprj_baz_def)
apply (rule liftdefl_baz_def)
done

end

text ‹Prove DEFL rules using lemma ‹typedef_DEFL›.\<close>

lemma DEFL_foo: "DEFL('a foo) = foo_defl⋅DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_foo_def)
done

lemma DEFL_bar: "DEFL('a bar) = bar_defl⋅DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_bar_def)
done

lemma DEFL_baz: "DEFL('a baz) = baz_defl⋅DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_baz_def)
done

text ‹Prove DEFL equations using type combinator unfold lemmas.›

lemma DEFL_foo': "DEFL('a foo) = DEFL(one ⊕ 'a🪙⊥ ⊗ ('a bar)🪙⊥)"
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule foo_defl_unfold)

lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz → tr)🪙⊥)"
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule bar_defl_unfold)

lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd → tr)🪙⊥)"
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule baz_defl_unfold)

(********************************************************************)

subsection ‹Step 3: Define rep and abs functions›

text ‹Define them all using ‹prj› and ‹emb›!›

definition foo_rep :: "'a foo → one ⊕ ('a🪙⊥ ⊗ ('a bar)🪙⊥)"
where "foo_rep ≡ prj oo emb"

definition foo_abs :: "one ⊕ ('a🪙⊥ ⊗ ('a bar)🪙⊥) → 'a foo"
where "foo_abs ≡ prj oo emb"

definition bar_rep :: "'a bar → ('a baz → tr)🪙⊥"
where "bar_rep ≡ prj oo emb"

definition bar_abs :: "('a baz → tr)🪙⊥ → 'a bar"
where "bar_abs ≡ prj oo emb"

definition baz_rep :: "'a baz → ('a foo convex_pd → tr)🪙⊥"
where "baz_rep ≡ prj oo emb"

definition baz_abs :: "('a foo convex_pd → tr)🪙⊥ → 'a baz"
where "baz_abs ≡ prj oo emb"

text ‹Prove isomorphism rules.›

lemma foo_abs_iso: "foo_rep⋅(foo_abs⋅x) = x"
by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])

lemma foo_rep_iso: "foo_abs⋅(foo_rep⋅x) = x"
by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])

lemma bar_abs_iso: "bar_rep⋅(bar_abs⋅x) = x"
by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])

lemma bar_rep_iso: "bar_abs⋅(bar_rep⋅x) = x"
by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])

lemma baz_abs_iso: "baz_rep⋅(baz_abs⋅x) = x"
by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])

lemma baz_rep_iso: "baz_abs⋅(baz_rep⋅x) = x"
by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])

text ‹Prove isodefl rules using ‹isodefl_coerce›.\<close>

lemma isodefl_foo_abs:
  "isodefl d t ==> isodefl (foo_abs oo d oo foo_rep) t"
by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])

lemma isodefl_bar_abs:
  "isodefl d t ==> isodefl (bar_abs oo d oo bar_rep) t"
by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])

lemma isodefl_baz_abs:
  "isodefl d t ==> isodefl (baz_abs oo d oo baz_rep) t"
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])

(********************************************************************)

subsection ‹Step 4: Define map functions, prove isodefl property›

text ‹Start with the one-step non-recursive version.›

text ‹Note that the type of the map function depends on which
 variables are used in positive and negative positions.›

definition
  foo_bar_baz_mapF ::
    "('a → 'b) →
     ('a foo → 'b foo) × ('a bar → 'b bar) × ('b baz → 'a baz) →
     ('a foo → 'b foo) × ('a bar → 'b bar) × ('b baz → 'a baz)"
where
  "foo_bar_baz_mapF = (Λ f. Abs_cfun (λ(d1, d2, d3).
    (
      foo_abs oo
        ssum_map⋅ID⋅(sprod_map⋅(u_map⋅f)⋅(u_map⋅d2))
          oo foo_rep
    ,
      bar_abs oo u_map⋅(cfun_map⋅d3⋅ID) oo bar_rep
    ,
      baz_abs oo u_map⋅(cfun_map⋅(convex_map⋅d1)⋅ID) oo baz_rep
    )))"

lemma foo_bar_baz_mapF_beta:
  "foo_bar_baz_mapF⋅f⋅d =
    (
      foo_abs oo
        ssum_map⋅ID⋅(sprod_map⋅(u_map⋅f)⋅(u_map⋅(fst (snd d))))
          oo foo_rep
    ,
      bar_abs oo u_map⋅(cfun_map⋅(snd (snd d))⋅ID) oo bar_rep
    ,
      baz_abs oo u_map⋅(cfun_map⋅(convex_map⋅(fst d))⋅ID) oo baz_rep
    )"
unfolding foo_bar_baz_mapF_def
by (simp add: split_def)

text ‹Individual map functions are projected from the fixed point.›

definition foo_map :: "('a → 'b) → ('a foo → 'b foo)"
where "foo_map = (Λ f. fst (fix⋅(foo_bar_baz_mapF⋅f)))"

definition bar_map :: "('a → 'b) → ('a bar → 'b bar)"
where "bar_map = (Λ f. fst (snd (fix⋅(foo_bar_baz_mapF⋅f))))"

definition baz_map :: "('a → 'b) → ('b baz → 'a baz)"
where "baz_map = (Λ f. snd (snd (fix⋅(foo_bar_baz_mapF⋅f))))"

lemma map_apply_thms:
  "foo_map⋅f = fst (fix⋅(foo_bar_baz_mapF⋅f))"
  "bar_map⋅f = fst (snd (fix⋅(foo_bar_baz_mapF⋅f)))"
  "baz_map⋅f = snd (snd (fix⋅(foo_bar_baz_mapF⋅f)))"
unfolding foo_map_def bar_map_def baz_map_def by simp_all

text ‹Prove isodefl rules for all map functions simultaneously.›

lemma isodefl_foo_bar_baz:
  assumes isodefl_d: "isodefl d t"
  shows
  "isodefl (foo_map⋅d) (foo_defl⋅t) ∧
  isodefl (bar_map⋅d) (bar_defl⋅t) ∧
  isodefl (baz_map⋅d) (baz_defl⋅t)"
unfolding map_apply_thms defl_apply_thms
 apply (rule parallel_fix_ind)
   apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
  apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
 apply (simp only: foo_bar_baz_mapF_beta
                   foo_bar_baz_deflF_beta
                   fst_conv snd_conv)
 apply (elim conjE)
 apply (intro
  conjI
  isodefl_foo_abs
  isodefl_bar_abs
  isodefl_baz_abs
  domain_isodefl
  isodefl_ID_DEFL isodefl_LIFTDEFL
  isodefl_d
 )
 apply assumption+
done

lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]

text ‹Prove map ID lemmas, using isodefl_DEFL_imp_ID›

lemma foo_map_ID: "foo_map⋅ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_foo)
apply (rule isodefl_foo)
apply (rule isodefl_ID_DEFL)
done

lemma bar_map_ID: "bar_map⋅ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_bar)
apply (rule isodefl_bar)
apply (rule isodefl_ID_DEFL)
done

lemma baz_map_ID: "baz_map⋅ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_baz)
apply (rule isodefl_baz)
apply (rule isodefl_ID_DEFL)
done

(********************************************************************)

subsection ‹Step 5: Define take functions, prove lub-take lemmas›

definition
  foo_bar_baz_takeF ::
    "('a foo → 'a foo) × ('a bar → 'a bar) × ('a baz → 'a baz) →
     ('a foo → 'a foo) × ('a bar → 'a bar) × ('a baz → 'a baz)"
where
  "foo_bar_baz_takeF = (Λ p.
    ( foo_abs oo
        ssum_map⋅ID⋅(sprod_map⋅(u_map⋅ID)⋅(u_map⋅(fst (snd p))))
          oo foo_rep
    , bar_abs oo
        u_map⋅(cfun_map⋅(snd (snd p))⋅ID) oo bar_rep
    , baz_abs oo
        u_map⋅(cfun_map⋅(convex_map⋅(fst p))⋅ID) oo baz_rep
    ))"

lemma foo_bar_baz_takeF_beta:
  "foo_bar_baz_takeF⋅p =
    ( foo_abs oo
        ssum_map⋅ID⋅(sprod_map⋅(u_map⋅ID)⋅(u_map⋅(fst (snd p))))
          oo foo_rep
    , bar_abs oo
        u_map⋅(cfun_map⋅(snd (snd p))⋅ID) oo bar_rep
    , baz_abs oo
        u_map⋅(cfun_map⋅(convex_map⋅(fst p))⋅ID) oo baz_rep
    )"
unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp)

definition
  foo_take :: "nat ==> 'a foo → 'a foo"
where
  "foo_take = (λn. fst (iterate n⋅foo_bar_baz_takeF⋅⊥))"

definition
  bar_take :: "nat ==> 'a bar → 'a bar"
where
  "bar_take = (λn. fst (snd (iterate n⋅foo_bar_baz_takeF⋅⊥)))"

definition
  baz_take :: "nat ==> 'a baz → 'a baz"
where
  "baz_take = (λn. snd (snd (iterate n⋅foo_bar_baz_takeF⋅⊥)))"

lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take"
unfolding foo_take_def bar_take_def baz_take_def
by (intro ch2ch_fst ch2ch_snd chain_iterate)+

lemma take_0_thms: "foo_take 0 = ⊥" "bar_take 0 = ⊥" "baz_take 0 = ⊥"
unfolding foo_take_def bar_take_def baz_take_def
by (simp only: iterate_0 fst_strict snd_strict)+

lemma take_Suc_thms:
  "foo_take (Suc n) =
    foo_abs oo ssum_map⋅ID⋅(sprod_map⋅(u_map⋅ID)⋅(u_map⋅(bar_take n))) oo foo_rep"
  "bar_take (Suc n) =
    bar_abs oo u_map⋅(cfun_map⋅(baz_take n)⋅ID) oo bar_rep"
  "baz_take (Suc n) =
    baz_abs oo u_map⋅(cfun_map⋅(convex_map⋅(foo_take n))⋅ID) oo baz_rep"
unfolding foo_take_def bar_take_def baz_take_def
by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+

lemma lub_take_lemma:
  "(⊔n. foo_take n, ⊔n. bar_take n, ⊔n. baz_take n)
    = (foo_map⋅(ID::'a → 'a), bar_map⋅(ID::'a → 'a), baz_map⋅(ID::'a → 'a))"
apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
apply (simp only: map_apply_thms prod.collapse)
apply (simp only: fix_def2)
apply (rule lub_eq)
apply (rule nat.induct)
apply (simp only: iterate_0 Pair_strict take_0_thms)
apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
                  foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
done

lemma lub_foo_take: "(⊔n. foo_take n) = ID"
apply (rule trans [OF _ foo_map_ID])
using lub_take_lemma
apply (elim Pair_inject)
apply assumption
done

lemma lub_bar_take: "(⊔n. bar_take n) = ID"
apply (rule trans [OF _ bar_map_ID])
using lub_take_lemma
apply (elim Pair_inject)
apply assumption
done

lemma lub_baz_take: "(⊔n. baz_take n) = ID"
apply (rule trans [OF _ baz_map_ID])
using lub_take_lemma
apply (elim Pair_inject)
apply assumption
done

end