1(* Title: HOL/Basic_BNF_LFPs.thy 2 Author: Jasmin Blanchette, TU Muenchen 3 Copyright 2014 4 5Registration of basic types as BNF least fixpoints (datatypes). 6*) 7 8theory Basic_BNF_LFPs 9imports BNF_Least_Fixpoint 10begin 11 12definition xtor :: "'a \<Rightarrow> 'a" where 13 "xtor x = x" 14 15lemma xtor_map: "f (xtor x) = xtor (f x)" 16 unfolding xtor_def by (rule refl) 17 18lemma xtor_map_unique: "u \<circ> xtor = xtor \<circ> f \<Longrightarrow> u = f" 19 unfolding o_def xtor_def . 20 21lemma xtor_set: "f (xtor x) = f x" 22 unfolding xtor_def by (rule refl) 23 24lemma xtor_rel: "R (xtor x) (xtor y) = R x y" 25 unfolding xtor_def by (rule refl) 26 27lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z" 28 unfolding xtor_def by assumption 29 30lemma xtor_xtor: "xtor (xtor x) = x" 31 unfolding xtor_def by (rule refl) 32 33lemmas xtor_inject = xtor_rel[of "(=)"] 34 35lemma 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 38lemma xtor_iff_xtor: "u = xtor w \<longleftrightarrow> xtor u = w" 39 unfolding xtor_def .. 40 41lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))" 42 unfolding xtor_def id_bnf_def by (rule reflexive) 43 44lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))" 45 unfolding xtor_def id_bnf_def by (rule reflexive) 46 47lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))" 48 unfolding xtor_def id_bnf_def by (rule reflexive) 49 50definition ctor_rec :: "'a \<Rightarrow> 'a" where 51 "ctor_rec x = x" 52 53lemma 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 56lemma 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 59lemma 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 62lemma 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 65lemma 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 68lemma eq_fst_iff: "a = fst p \<longleftrightarrow> (\<exists>b. p = (a, b))" 69 by (cases p) auto 70 71lemma eq_snd_iff: "b = snd p \<longleftrightarrow> (\<exists>a. p = (a, b))" 72 by (cases p) auto 73 74lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)" 75 by standard blast+ 76 77lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)" 78 by standard blast+ 79 80lemma isl_map_sum: 81 "isl (map_sum f g s) = isl s" 82 by (cases s) simp_all 83 84lemma 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 89lemma 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 94lemma 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 99lemma isl_transfer: "rel_fun (rel_sum A B) (=) isl isl" 100 unfolding rel_fun_def rel_sum_sel by simp 101 102lemma 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 105ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" 106 107declare prod.size [no_atp] 108 109hide_const (open) xtor ctor_rec 110 111hide_fact (open) 112 xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec 113 ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt 114 115end 116