src/HOL/Basic_BNF_LFPs.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 63045 c50c764aab10 child 67332 cb96edae56ef permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
```     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_map_unique: "u \<circ> xtor = xtor \<circ> f \<Longrightarrow> u = f"
```
```    19   unfolding o_def xtor_def .
```
```    20
```
```    21 lemma xtor_set: "f (xtor x) = f x"
```
```    22   unfolding xtor_def by (rule refl)
```
```    23
```
```    24 lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
```
```    25   unfolding xtor_def by (rule refl)
```
```    26
```
```    27 lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z"
```
```    28   unfolding xtor_def by assumption
```
```    29
```
```    30 lemma xtor_xtor: "xtor (xtor x) = x"
```
```    31   unfolding xtor_def by (rule refl)
```
```    32
```
```    33 lemmas xtor_inject = xtor_rel[of "op ="]
```
```    34
```
```    35 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"
```
```    36   unfolding xtor_def vimage2p_def id_bnf_def ..
```
```    37
```
```    38 lemma xtor_iff_xtor: "u = xtor w \<longleftrightarrow> xtor u = w"
```
```    39   unfolding xtor_def ..
```
```    40
```
```    41 lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
```
```    42   unfolding xtor_def id_bnf_def by (rule reflexive)
```
```    43
```
```    44 lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))"
```
```    45   unfolding xtor_def id_bnf_def by (rule reflexive)
```
```    46
```
```    47 lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
```
```    48   unfolding xtor_def id_bnf_def by (rule reflexive)
```
```    49
```
```    50 definition ctor_rec :: "'a \<Rightarrow> 'a" where
```
```    51   "ctor_rec x = x"
```
```    52
```
```    53 lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
```
```    54   unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
```
```    55
```
```    56 lemma ctor_rec_unique: "g = id \<Longrightarrow> f \<circ> xtor = s \<circ> (id_bnf \<circ> g \<circ> id_bnf) \<Longrightarrow> f = ctor_rec s"
```
```    57   unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
```
```    58
```
```    59 lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
```
```    60   unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
```
```    61
```
```    62 lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
```
```    63   unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
```
```    64
```
```    65 lemma ctor_rec_transfer: "rel_fun (rel_fun (vimage2p id_bnf id_bnf R) S) (rel_fun R S) ctor_rec ctor_rec"
```
```    66   unfolding rel_fun_def vimage2p_def id_bnf_def ctor_rec_def by simp
```
```    67
```
```    68 lemma eq_fst_iff: "a = fst p \<longleftrightarrow> (\<exists>b. p = (a, b))"
```
```    69   by (cases p) auto
```
```    70
```
```    71 lemma eq_snd_iff: "b = snd p \<longleftrightarrow> (\<exists>a. p = (a, b))"
```
```    72   by (cases p) auto
```
```    73
```
```    74 lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
```
```    75   by standard blast+
```
```    76
```
```    77 lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)"
```
```    78   by standard blast+
```
```    79
```
```    80 lemma isl_map_sum:
```
```    81   "isl (map_sum f g s) = isl s"
```
```    82   by (cases s) simp_all
```
```    83
```
```    84 lemma map_sum_sel:
```
```    85   "isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)"
```
```    86   "\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)"
```
```    87   by (case_tac [!] s) simp_all
```
```    88
```
```    89 lemma set_sum_sel:
```
```    90   "isl s \<Longrightarrow> projl s \<in> setl s"
```
```    91   "\<not> isl s \<Longrightarrow> projr s \<in> setr s"
```
```    92   by (case_tac [!] s) (auto intro: setl.intros setr.intros)
```
```    93
```
```    94 lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and>
```
```    95   (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
```
```    96   (\<not> isl a \<longrightarrow> \<not> isl b \<longrightarrow> R2 (projr a) (projr b)))"
```
```    97   by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all
```
```    98
```
```    99 lemma isl_transfer: "rel_fun (rel_sum A B) (op =) isl isl"
```
```   100   unfolding rel_fun_def rel_sum_sel by simp
```
```   101
```
```   102 lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))"
```
```   103   by (force simp: rel_prod.simps elim: rel_prod.cases)
```
```   104
```
```   105 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
```
```   106
```
```   107 ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
```
```   108
```
```   109 lemma size_bool[code]: "size (b :: bool) = 0"
```
```   110   by (cases b) auto
```
```   111
```
```   112 declare prod.size[no_atp]
```
```   113
```
```   114 lemmas size_nat = size_nat_def
```
```   115
```
```   116 hide_const (open) xtor ctor_rec
```
```   117
```
```   118 hide_fact (open)
```
```   119   xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
```
```   120   ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
```
```   121
```
```   122 end
```