Quellcode-Bibliothek Basic_BNF_LFPs.thy Sprache: Isabelle

(*  Title:      HOL/Basic_BNF_LFPs.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2014

Registration of basic types as BNF least fixpoints (datatypes).
*)

theory Basic_BNF_LFPs
imports BNF_Least_Fixpoint
begin

definition xtor :: "'a \ 'a" where
  "xtor x = x"

lemma xtor_map: "f (xtor x) = xtor (f x)"
  unfolding xtor_def by (rule refl)

lemma xtor_map_unique: "u \ xtor = xtor \ f \ u = f"
  unfolding o_def xtor_def .

lemma xtor_set: "f (xtor x) = f x"
  unfolding xtor_def by (rule refl)

lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
  unfolding xtor_def by (rule refl)

lemma xtor_induct: "(\x. P (xtor x)) \ P z"
  unfolding xtor_def by assumption

lemma xtor_xtor: "xtor (xtor x) = x"
  unfolding xtor_def by (rule refl)

lemmas xtor_inject = xtor_rel[of "(=)"]

lemma xtor_rel_induct: "(\x y. vimage2p id_bnf id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR"
  unfolding xtor_def vimage2p_def id_bnf_def ..

lemma xtor_iff_xtor: "u = xtor w \ xtor u = w"
  unfolding xtor_def ..

lemma Inl_def_alt: "Inl \ (\a. xtor (id_bnf (Inl a)))"
  unfolding xtor_def id_bnf_def by (rule reflexive)

lemma Inr_def_alt: "Inr \ (\a. xtor (id_bnf (Inr a)))"
  unfolding xtor_def id_bnf_def by (rule reflexive)

lemma Pair_def_alt: "Pair \ (\a b. xtor (id_bnf (a, b)))"
  unfolding xtor_def id_bnf_def by (rule reflexive)

definition ctor_rec :: "'a \ 'a" where
  "ctor_rec x = x"

lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((id_bnf \ g \ id_bnf) x)"
  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)

lemma ctor_rec_unique: "g = id \ f \ xtor = s \ (id_bnf \ g \ id_bnf) \ f = ctor_rec s"
  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)

lemma ctor_rec_def_alt: "f = ctor_rec (f \ id_bnf)"
  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)

lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (id_bnf \ g \ id_bnf))"
  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)

lemma ctor_rec_transfer: "rel_fun (rel_fun (vimage2p id_bnf id_bnf R) S) (rel_fun R S) ctor_rec ctor_rec"
  unfolding rel_fun_def vimage2p_def id_bnf_def ctor_rec_def by simp

lemma eq_fst_iff: "a = fst p \ (\b. p = (a, b))"
  by (cases p) auto

lemma eq_snd_iff: "b = snd p \ (\a. p = (a, b))"
  by (cases p) auto

lemma ex_neg_all_pos: "((\x. P x) \ Q) \ (\x. P x \ Q)"
  by standard blast+

lemma hypsubst_in_prems: "(\x. y = x \ z = f x \ P) \ (z = f y \ P)"
  by standard blast+

lemma isl_map_sum:
  "isl (map_sum f g s) = isl s"
  by (cases s) simp_all

lemma map_sum_sel:
  "isl s \ projl (map_sum f g s) = f (projl s)"
  "\ isl s \ projr (map_sum f g s) = g (projr s)"
  by (cases s; simp)+

lemma set_sum_sel:
  "isl s \ projl s \ setl s"
  "\ isl s \ projr s \ setr s"
  by (cases s; auto intro: setl.intros setr.intros)+

lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \
  (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
  (\<not> isl a \<longrightarrow> \<not> isl b \<longrightarrow> R2 (projr a) (projr b)))"
  by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all

lemma isl_transfer: "rel_fun (rel_sum A B) (=) isl isl"
  unfolding rel_fun_def rel_sum_sel by simp

lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \ R2 (snd p) (snd q))"
  by (force simp: rel_prod.simps elim: rel_prod.cases)

ML_file \<open>Tools/BNF/bnf_lfp_basic_sugar.ML\<close>

declare prod.size [no_atp]

hide_const (open) xtor ctor_rec

hide_fact (open)
  xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
  ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt

end

quality100%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.