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