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
 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 \ '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 \ xtor = xtor \ f \ 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: "(\x. P (xtor x)) \ 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: "(\x y. vimage2p id_bnf id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ 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 \ xtor u = w" ``` blanchet@62321 ` 39` ``` unfolding xtor_def .. ``` blanchet@62321 ` 40` blanchet@58353 ` 41` ```lemma Inl_def_alt: "Inl \ (\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 \ (\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 \ (\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 \ 'a" where ``` blanchet@58377 ` 51` ``` "ctor_rec x = x" ``` blanchet@58377 ` 52` blanchet@58377 ` 53` ```lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((id_bnf \ g \ 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 \ f \ xtor = s \ (id_bnf \ g \ id_bnf) \ 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 \ 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 \ g = ctor_rec (f \ (id_bnf \ g \ 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 \ (\b. p = (a, b))" ``` traytel@58916 ` 69` ``` by (cases p) auto ``` traytel@58916 ` 70` traytel@58916 ` 71` ```lemma eq_snd_iff: "b = snd p \ (\a. p = (a, b))" ``` traytel@58916 ` 72` ``` by (cases p) auto ``` traytel@58916 ` 73` traytel@58916 ` 74` ```lemma ex_neg_all_pos: "((\x. P x) \ Q) \ (\x. P x \ Q)" ``` wenzelm@61169 ` 75` ``` by standard blast+ ``` traytel@58916 ` 76` traytel@58916 ` 77` ```lemma hypsubst_in_prems: "(\x. y = x \ z = f x \ P) \ (z = f y \ 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 \ projl (map_sum f g s) = f (projl s)" ``` traytel@58916 ` 86` ``` "\ isl s \ 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 \ projl s \ setl s" ``` traytel@58916 ` 91` ``` "\ isl s \ projr s \ 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 \ ``` traytel@58916 ` 95` ``` (isl a \ isl b \ R1 (projl a) (projl b)) \ ``` traytel@58916 ` 96` ``` (\ isl a \ \ isl b \ 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) \ 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 ```