src/HOL/Basic_BNF_Least_Fixpoints.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58391 fe0fc8aee49a
child 58916 229765cc3414
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Basic_BNF_Least_Fixpoints.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2014
     4 
     5 Registration of basic types as BNF least fixpoints (datatypes).
     6 *)
     7 
     8 theory Basic_BNF_Least_Fixpoints
     9 imports BNF_Least_Fixpoint
    10 begin
    11 
    12 definition xtor :: "'a \<Rightarrow> 'a" where
    13   "xtor x = x"
    14 
    15 lemma xtor_map: "f (xtor x) = xtor (f x)"
    16   unfolding xtor_def by (rule refl)
    17 
    18 lemma xtor_set: "f (xtor x) = f x"
    19   unfolding xtor_def by (rule refl)
    20 
    21 lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
    22   unfolding xtor_def by (rule refl)
    23 
    24 lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z"
    25   unfolding xtor_def by assumption
    26 
    27 lemma xtor_xtor: "xtor (xtor x) = x"
    28   unfolding xtor_def by (rule refl)
    29 
    30 lemmas xtor_inject = xtor_rel[of "op ="]
    31 
    32 lemma xtor_rel_induct: "(\<And>x y. vimage2p id_bnf id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
    33   unfolding xtor_def vimage2p_def id_bnf_def by default
    34 
    35 lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
    36   unfolding xtor_def id_bnf_def by (rule reflexive)
    37 
    38 lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))"
    39   unfolding xtor_def id_bnf_def by (rule reflexive)
    40 
    41 lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
    42   unfolding xtor_def id_bnf_def by (rule reflexive)
    43 
    44 definition ctor_rec :: "'a \<Rightarrow> 'a" where
    45   "ctor_rec x = x"
    46 
    47 lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
    48   unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    49 
    50 lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
    51   unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    52 
    53 lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
    54   unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    55 
    56 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    57 
    58 ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
    59 
    60 lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    61   by (cases b) auto
    62 
    63 declare prod.size[no_atp]
    64 
    65 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    66   by (induct n) simp_all
    67 
    68 hide_const (open) xtor ctor_rec
    69 
    70 hide_fact (open)
    71   xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
    72   ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
    73 
    74 end