products/sources/formale sprachen/Isabelle/HOL/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: intro_noop.v   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.1 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff