src/HOL/Basic_BNF_Least_Fixpoints.thy
author blanchet
Fri Sep 19 13:27:04 2014 +0200 (2014-09-19)
changeset 58390 b74d8470b98e
parent 58377 c6f93b8d2d8e
child 58391 fe0fc8aee49a
permissions -rw-r--r--
keep obsolete interpretations in Main, to avoid merge trouble
blanchet@58352
     1
(*  Title:      HOL/Basic_BNF_Least_Fixpoints.thy
blanchet@58352
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@58352
     3
    Copyright   2014
blanchet@58352
     4
blanchet@58352
     5
Registration of basic types as BNF least fixpoints (datatypes).
blanchet@58352
     6
*)
blanchet@58352
     7
blanchet@58352
     8
theory Basic_BNF_Least_Fixpoints
blanchet@58352
     9
imports BNF_Least_Fixpoint
blanchet@58352
    10
begin
blanchet@58352
    11
blanchet@58352
    12
definition xtor :: "'a \<Rightarrow> 'a" where
blanchet@58352
    13
  "xtor x = x"
blanchet@58352
    14
blanchet@58352
    15
lemma xtor_map: "f (xtor x) = xtor (f x)"
blanchet@58352
    16
  unfolding xtor_def by (rule refl)
blanchet@58352
    17
blanchet@58352
    18
lemma xtor_set: "f (xtor x) = f x"
blanchet@58353
    19
  unfolding xtor_def by (rule refl)
blanchet@58352
    20
blanchet@58352
    21
lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
blanchet@58352
    22
  unfolding xtor_def by (rule refl)
blanchet@58352
    23
blanchet@58352
    24
lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z"
blanchet@58352
    25
  unfolding xtor_def by assumption
blanchet@58352
    26
blanchet@58352
    27
lemma xtor_xtor: "xtor (xtor x) = x"
blanchet@58352
    28
  unfolding xtor_def by (rule refl)
blanchet@58352
    29
blanchet@58352
    30
lemmas xtor_inject = xtor_rel[of "op ="]
blanchet@58352
    31
blanchet@58353
    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"
blanchet@58353
    33
  unfolding xtor_def vimage2p_def id_bnf_def by default
blanchet@58352
    34
blanchet@58353
    35
lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
blanchet@58353
    36
  unfolding xtor_def id_bnf_def by (rule reflexive)
blanchet@58352
    37
blanchet@58353
    38
lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))"
blanchet@58353
    39
  unfolding xtor_def id_bnf_def by (rule reflexive)
blanchet@58352
    40
blanchet@58353
    41
lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
blanchet@58353
    42
  unfolding xtor_def id_bnf_def by (rule reflexive)
blanchet@58352
    43
blanchet@58377
    44
definition ctor_rec :: "'a \<Rightarrow> 'a" where
blanchet@58377
    45
  "ctor_rec x = x"
blanchet@58377
    46
blanchet@58377
    47
lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
blanchet@58377
    48
  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
blanchet@58377
    49
blanchet@58377
    50
lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
blanchet@58377
    51
  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
blanchet@58377
    52
blanchet@58377
    53
lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
blanchet@58377
    54
  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
blanchet@58377
    55
blanchet@58352
    56
ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
blanchet@58352
    57
blanchet@58390
    58
ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
blanchet@58377
    59
blanchet@58353
    60
hide_const (open) xtor ctor_rec
blanchet@58353
    61
blanchet@58353
    62
hide_fact (open)
blanchet@58353
    63
  xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
blanchet@58377
    64
  ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
blanchet@58353
    65
blanchet@58352
    66
end