src/HOL/Basic_BNF_LFPs.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62335 e85c42f4f30a
child 62863 e0b894bba6ff
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Basic_BNF_LFPs.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_LFPs
     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 ..
    34 
    35 lemma xtor_iff_xtor: "u = xtor w \<longleftrightarrow> xtor u = w"
    36   unfolding xtor_def ..
    37 
    38 lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
    39   unfolding xtor_def id_bnf_def by (rule reflexive)
    40 
    41 lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))"
    42   unfolding xtor_def id_bnf_def by (rule reflexive)
    43 
    44 lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
    45   unfolding xtor_def id_bnf_def by (rule reflexive)
    46 
    47 definition ctor_rec :: "'a \<Rightarrow> 'a" where
    48   "ctor_rec x = x"
    49 
    50 lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
    51   unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    52 
    53 lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
    54   unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    55 
    56 lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
    57   unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    58 
    59 lemma eq_fst_iff: "a = fst p \<longleftrightarrow> (\<exists>b. p = (a, b))"
    60   by (cases p) auto
    61 
    62 lemma eq_snd_iff: "b = snd p \<longleftrightarrow> (\<exists>a. p = (a, b))"
    63   by (cases p) auto
    64 
    65 lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
    66   by standard blast+
    67 
    68 lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)"
    69   by standard blast+
    70 
    71 lemma isl_map_sum:
    72   "isl (map_sum f g s) = isl s"
    73   by (cases s) simp_all
    74 
    75 lemma map_sum_sel:
    76   "isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)"
    77   "\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)"
    78   by (case_tac [!] s) simp_all
    79 
    80 lemma set_sum_sel:
    81   "isl s \<Longrightarrow> projl s \<in> setl s"
    82   "\<not> isl s \<Longrightarrow> projr s \<in> setr s"
    83   by (case_tac [!] s) (auto intro: setl.intros setr.intros)
    84 
    85 lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and>
    86   (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
    87   (\<not> isl a \<longrightarrow> \<not> isl b \<longrightarrow> R2 (projr a) (projr b)))"
    88   by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all
    89 
    90 lemma isl_transfer: "rel_fun (rel_sum A B) (op =) isl isl"
    91   unfolding rel_fun_def rel_sum_sel by simp
    92 
    93 lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))"
    94   by (force simp: rel_prod.simps elim: rel_prod.cases)
    95 
    96 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    97 
    98 ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
    99 
   100 lemma size_bool[code]: "size (b :: bool) = 0"
   101   by (cases b) auto
   102 
   103 declare prod.size[no_atp]
   104 
   105 lemmas size_nat = size_nat_def
   106 
   107 hide_const (open) xtor ctor_rec
   108 
   109 hide_fact (open)
   110   xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
   111   ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
   112 
   113 end