Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Basic_BNFs.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Basic_BNFs.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2012

Registration of basic types as bounded natural functors.
*)

section \<open>Registration of Basic Types as Bounded Natural Functors\<close>

theory Basic_BNFs
imports BNF_Def
begin

inductive_set setl :: "'a + 'b \ 'a set" for s :: "'a + 'b" where
  "s = Inl x \ x \ setl s"
inductive_set setr :: "'a + 'b \ 'b set" for s :: "'a + 'b" where
  "s = Inr x \ x \ setr s"

lemma sum_set_defs[code]:
  "setl = (\x. case x of Inl z \ {z} | _ \ {})"
  "setr = (\x. case x of Inr z \ {z} | _ \ {})"
  by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits)

lemma rel_sum_simps[code, simp]:
  "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
  "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
  "rel_sum R1 R2 (Inr a2) (Inl b1) = False"
  "rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
  by (auto intro: rel_sum.intros elim: rel_sum.cases)

inductive
   pred_sum :: "('a \ bool) \ ('b \ bool) \ 'a + 'b \ bool" for P1 P2
where
  "P1 a \ pred_sum P1 P2 (Inl a)"
| "P2 b \ pred_sum P1 P2 (Inr b)"

lemma pred_sum_inject[code, simp]:
  "pred_sum P1 P2 (Inl a) \ P1 a"
  "pred_sum P1 P2 (Inr b) \ P2 b"
  by (simp add: pred_sum.simps)+

bnf "'a + 'b"
  map: map_sum
  sets: setl setr
  bd: natLeq
  wits: Inl Inr
  rel: rel_sum
  pred: pred_sum
proof -
  show "map_sum id id = id" by (rule map_sum.id)
next
  fix f1 :: "'o \ 's" and f2 :: "'p \ 't" and g1 :: "'s \ 'q" and g2 :: "'t \ 'r"
  show "map_sum (g1 \ f1) (g2 \ f2) = map_sum g1 g2 \ map_sum f1 f2"
    by (rule map_sum.comp[symmetric])
next
  fix x and f1 :: "'o \ 'q" and f2 :: "'p \ 'r" and g1 g2
  assume a1: "\z. z \ setl x \ f1 z = g1 z" and
         a2: "\z. z \ setr x \ f2 z = g2 z"
  thus "map_sum f1 f2 x = map_sum g1 g2 x"
  proof (cases x)
    case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1))
  next
    case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2))
  qed
next
  fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r"
  show "setl \ map_sum f1 f2 = image f1 \ setl"
    by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
next
  fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r"
  show "setr \ map_sum f1 f2 = image f2 \ setr"
    by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
next
  show "card_order natLeq" by (rule natLeq_card_order)
next
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
  fix x :: "'o + 'p"
  show "|setl x| \o natLeq"
    apply (rule ordLess_imp_ordLeq)
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    by (simp add: sum_set_defs(1) split: sum.split)
next
  fix x :: "'o + 'p"
  show "|setr x| \o natLeq"
    apply (rule ordLess_imp_ordLeq)
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
    by (simp add: sum_set_defs(2) split: sum.split)
next
  fix R1 R2 S1 S2
  show "rel_sum R1 R2 OO rel_sum S1 S2 \ rel_sum (R1 OO S1) (R2 OO S2)"
    by (force elim: rel_sum.cases)
next
  fix R S
  show "rel_sum R S = (\x y.
    \<exists>z. (setl z \<subseteq> {(x, y). R x y} \<and> setr z \<subseteq> {(x, y). S x y}) \<and>
    map_sum fst fst z = x \<and> map_sum snd snd z = y)"
  unfolding sum_set_defs relcompp.simps conversep.simps fun_eq_iff
  by (fastforce elim: rel_sum.cases split: sum.splits)
qed (auto simp: sum_set_defs fun_eq_iff pred_sum.simps split: sum.splits)

inductive_set fsts :: "'a \ 'b \ 'a set" for p :: "'a \ 'b" where
  "fst p \ fsts p"
inductive_set snds :: "'a \ 'b \ 'b set" for p :: "'a \ 'b" where
  "snd p \ snds p"

lemma prod_set_defs[code]: "fsts = (\p. {fst p})" "snds = (\p. {snd p})"
  by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases)

inductive
  rel_prod :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" for R1 R2
where
  "\R1 a b; R2 c d\ \ rel_prod R1 R2 (a, c) (b, d)"

inductive
  pred_prod :: "('a \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" for P1 P2
where
  "\P1 a; P2 b\ \ pred_prod P1 P2 (a, b)"

lemma rel_prod_inject [code, simp]:
  "rel_prod R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d"
  by (auto intro: rel_prod.intros elim: rel_prod.cases)

lemma pred_prod_inject [code, simp]:
  "pred_prod P1 P2 (a, b) \ P1 a \ P2 b"
  by (auto intro: pred_prod.intros elim: pred_prod.cases)

lemma rel_prod_conv:
  "rel_prod R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)"
  by (rule ext, rule ext) auto

definition
  pred_fun :: "('a \ bool) \ ('b \ bool) \ ('a \ 'b) \ bool"
where
  "pred_fun A B = (\f. \x. A x \ B (f x))"

lemma pred_funI: "(\x. A x \ B (f x)) \ pred_fun A B f"
  unfolding pred_fun_def by simp

bnf "'a \ 'b"
  map: map_prod
  sets: fsts snds
  bd: natLeq
  rel: rel_prod
  pred: pred_prod
proof (unfold prod_set_defs)
  show "map_prod id id = id" by (rule map_prod.id)
next
  fix f1 f2 g1 g2
  show "map_prod (g1 \ f1) (g2 \ f2) = map_prod g1 g2 \ map_prod f1 f2"
    by (rule map_prod.comp[symmetric])
next
  fix x f1 f2 g1 g2
  assume "\z. z \ {fst x} \ f1 z = g1 z" "\z. z \ {snd x} \ f2 z = g2 z"
  thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
next
  fix f1 f2
  show "(\x. {fst x}) \ map_prod f1 f2 = image f1 \ (\x. {fst x})"
    by (rule ext, unfold o_apply) simp
next
  fix f1 f2
  show "(\x. {snd x}) \ map_prod f1 f2 = image f2 \ (\x. {snd x})"
    by (rule ext, unfold o_apply) simp
next
  show "card_order natLeq" by (rule natLeq_card_order)
next
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
  fix x
  show "|{fst x}| \o natLeq"
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
next
  fix x
  show "|{snd x}| \o natLeq"
    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
next
  fix R1 R2 S1 S2
  show "rel_prod R1 R2 OO rel_prod S1 S2 \ rel_prod (R1 OO S1) (R2 OO S2)" by auto
next
  fix R S
  show "rel_prod R S = (\x y.
    \<exists>z. ({fst z} \<subseteq> {(x, y). R x y} \<and> {snd z} \<subseteq> {(x, y). S x y}) \<and>
      map_prod fst fst z = x \<and> map_prod snd snd z = y)"
  unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff
  by auto
qed auto

bnf "'a \ 'b"
  map: "(\)"
  sets: range
  bd: "natLeq +c |UNIV :: 'a set|"
  rel: "rel_fun (=)"
  pred: "pred_fun (\_. True)"
proof
  fix f show "id \ f = id f" by simp
next
  fix f g show "(\) (g \ f) = (\) g \ (\) f"
  unfolding comp_def[abs_def] ..
next
  fix x f g
  assume "\z. z \ range x \ f z = g z"
  thus "f \ x = g \ x" by auto
next
  fix f show "range \ (\) f = (`) f \ range"
    by (auto simp add: fun_eq_iff)
next
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
  apply (rule card_order_csum)
  apply (rule natLeq_card_order)
  by (rule card_of_card_order_on)
(*  *)
  show "cinfinite (natLeq +c ?U)"
    apply (rule cinfinite_csum)
    apply (rule disjI1)
    by (rule natLeq_cinfinite)
next
  fix f :: "'d => 'a"
  have "|range f| \o | (UNIV::'d set) |" (is "_ \o ?U") by (rule card_of_image)
  also have "?U \o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
  finally show "|range f| \o natLeq +c ?U" .
next
  fix R S
  show "rel_fun (=) R OO rel_fun (=) S \ rel_fun (=) (R OO S)" by (auto simp: rel_fun_def)
next
  fix R
  show "rel_fun (=) R = (\x y.
    \<exists>z. range z \<subseteq> {(x, y). R x y} \<and> fst \<circ> z = x \<and> snd \<circ> z = y)"
  unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric])
qed (auto simp: pred_fun_def)

end

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.