(* 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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
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.
|
