Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: PacemakerRT.launch Sprache: Lisp

Original von: Isabelle^©

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

section \<open>Internal domain package proofs done manually\<close>

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 \<rightarrow> tr")
   and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")

*)

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

subsection \<open>Step 1: Define the new type combinators\<close>

text \<open>Start with the one-step non-recursive version\<close>

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\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"

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

text \<open>Individual type combinators are projected from the fixed point.\<close>

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 \<open>Unfold rules for each combinator.\<close>

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 \<open>Step 2: Define types, prove class instances\<close>

text \<open>Use \<open>pcpodef\<close> with the appropriate type combinator.\<close>

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 \<open>Prove rep instance using lemma \<open>typedef_rep_class\<close>.\<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 \<open>Prove DEFL rules using lemma \<open>typedef_DEFL\<close>.\<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 \<open>Prove DEFL equations using type combinator unfold lemmas.\<close>

lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
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)\<^sub>\)"
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)\<^sub>\)"
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule baz_defl_unfold)

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

subsection \<open>Step 3: Define rep and abs functions\<close>

text \<open>Define them all using \<open>prj\<close> and \<open>emb\<close>!\<close>

definition foo_rep :: "'a foo \ one \ ('a\<^sub>\ \ ('a bar)\<^sub>\)"
where "foo_rep \ prj oo emb"

definition foo_abs :: "one \ ('a\<^sub>\ \ ('a bar)\<^sub>\) \ 'a foo"
where "foo_abs \ prj oo emb"

definition bar_rep :: "'a bar \ ('a baz \ tr)\<^sub>\"
where "bar_rep \ prj oo emb"

definition bar_abs :: "('a baz \ tr)\<^sub>\ \ 'a bar"
where "bar_abs \ prj oo emb"

definition baz_rep :: "'a baz \ ('a foo convex_pd \ tr)\<^sub>\"
where "baz_rep \ prj oo emb"

definition baz_abs :: "('a foo convex_pd \ tr)\<^sub>\ \ 'a baz"
where "baz_abs \ prj oo emb"

text \<open>Prove isomorphism rules.\<close>

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 \<open>Prove isodefl rules using \<open>isodefl_coerce\<close>.\<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 \<open>Step 4: Define map functions, prove isodefl property\<close>

text \<open>Start with the one-step non-recursive version.\<close>

text \<open>Note that the type of the map function depends on which
variables are used in positive and negative positions.\<close>

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\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
          oo foo_rep
    ,
      bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
    ,
      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
    )))"

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

text \<open>Individual map functions are projected from the fixed point.\<close>

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 \<open>Prove isodefl rules for all map functions simultaneously.\<close>

lemma isodefl_foo_bar_baz:
  assumes isodefl_d: "isodefl d t"
  shows
  "isodefl (foo_map\d) (foo_defl\t) \
  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>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 \<open>Prove map ID lemmas, using isodefl_DEFL_imp_ID\<close>

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 \<open>Step 5: Define take functions, prove lub-take lemmas\<close>

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\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
          oo foo_rep
    , bar_abs oo
        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
    , baz_abs oo
        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
    ))"

lemma foo_bar_baz_takeF_beta:
  "foo_bar_baz_takeF\p =
    ( foo_abs oo
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
          oo foo_rep
    , bar_abs oo
        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
    , baz_abs oo
        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>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\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(bar_take n))) oo foo_rep"
  "bar_take (Suc n) =
    bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep"
  "baz_take (Suc n) =
    baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>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\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> '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

¤ Dauer der Verarbeitung: 0.58 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.