src/HOL/Basic_BNF_LFPs.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 62335 e85c42f4f30a child 62863 e0b894bba6ff permissions -rw-r--r--
generalize more theorems to support enat and ennreal
 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` blanchet@58352 ` 18` ```lemma xtor_set: "f (xtor x) = f x" ``` blanchet@58353 ` 19` ``` unfolding xtor_def by (rule refl) ``` blanchet@58352 ` 20` blanchet@58352 ` 21` ```lemma xtor_rel: "R (xtor x) (xtor y) = R x y" ``` blanchet@58352 ` 22` ``` unfolding xtor_def by (rule refl) ``` blanchet@58352 ` 23` blanchet@58352 ` 24` ```lemma xtor_induct: "(\x. P (xtor x)) \ P z" ``` blanchet@58352 ` 25` ``` unfolding xtor_def by assumption ``` blanchet@58352 ` 26` blanchet@58352 ` 27` ```lemma xtor_xtor: "xtor (xtor x) = x" ``` blanchet@58352 ` 28` ``` unfolding xtor_def by (rule refl) ``` blanchet@58352 ` 29` blanchet@58352 ` 30` ```lemmas xtor_inject = xtor_rel[of "op ="] ``` blanchet@58352 ` 31` blanchet@58353 ` 32` ```lemma xtor_rel_induct: "(\x y. vimage2p id_bnf id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR" ``` wenzelm@61169 ` 33` ``` unfolding xtor_def vimage2p_def id_bnf_def .. ``` blanchet@58352 ` 34` blanchet@62321 ` 35` ```lemma xtor_iff_xtor: "u = xtor w \ xtor u = w" ``` blanchet@62321 ` 36` ``` unfolding xtor_def .. ``` blanchet@62321 ` 37` blanchet@58353 ` 38` ```lemma Inl_def_alt: "Inl \ (\a. xtor (id_bnf (Inl a)))" ``` blanchet@58353 ` 39` ``` unfolding xtor_def id_bnf_def by (rule reflexive) ``` blanchet@58352 ` 40` blanchet@58353 ` 41` ```lemma Inr_def_alt: "Inr \ (\a. xtor (id_bnf (Inr a)))" ``` blanchet@58353 ` 42` ``` unfolding xtor_def id_bnf_def by (rule reflexive) ``` blanchet@58352 ` 43` blanchet@58353 ` 44` ```lemma Pair_def_alt: "Pair \ (\a b. xtor (id_bnf (a, b)))" ``` blanchet@58353 ` 45` ``` unfolding xtor_def id_bnf_def by (rule reflexive) ``` blanchet@58352 ` 46` blanchet@58377 ` 47` ```definition ctor_rec :: "'a \ 'a" where ``` blanchet@58377 ` 48` ``` "ctor_rec x = x" ``` blanchet@58377 ` 49` blanchet@58377 ` 50` ```lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((id_bnf \ g \ id_bnf) x)" ``` blanchet@58377 ` 51` ``` unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) ``` blanchet@58377 ` 52` blanchet@58377 ` 53` ```lemma ctor_rec_def_alt: "f = ctor_rec (f \ id_bnf)" ``` blanchet@58377 ` 54` ``` unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) ``` blanchet@58377 ` 55` blanchet@58377 ` 56` ```lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (id_bnf \ g \ id_bnf))" ``` blanchet@58377 ` 57` ``` unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) ``` blanchet@58377 ` 58` traytel@58916 ` 59` ```lemma eq_fst_iff: "a = fst p \ (\b. p = (a, b))" ``` traytel@58916 ` 60` ``` by (cases p) auto ``` traytel@58916 ` 61` traytel@58916 ` 62` ```lemma eq_snd_iff: "b = snd p \ (\a. p = (a, b))" ``` traytel@58916 ` 63` ``` by (cases p) auto ``` traytel@58916 ` 64` traytel@58916 ` 65` ```lemma ex_neg_all_pos: "((\x. P x) \ Q) \ (\x. P x \ Q)" ``` wenzelm@61169 ` 66` ``` by standard blast+ ``` traytel@58916 ` 67` traytel@58916 ` 68` ```lemma hypsubst_in_prems: "(\x. y = x \ z = f x \ P) \ (z = f y \ P)" ``` wenzelm@61169 ` 69` ``` by standard blast+ ``` traytel@58916 ` 70` traytel@58916 ` 71` ```lemma isl_map_sum: ``` traytel@58916 ` 72` ``` "isl (map_sum f g s) = isl s" ``` traytel@58916 ` 73` ``` by (cases s) simp_all ``` traytel@58916 ` 74` traytel@58916 ` 75` ```lemma map_sum_sel: ``` traytel@58916 ` 76` ``` "isl s \ projl (map_sum f g s) = f (projl s)" ``` traytel@58916 ` 77` ``` "\ isl s \ projr (map_sum f g s) = g (projr s)" ``` traytel@58916 ` 78` ``` by (case_tac [!] s) simp_all ``` traytel@58916 ` 79` traytel@58916 ` 80` ```lemma set_sum_sel: ``` traytel@58916 ` 81` ``` "isl s \ projl s \ setl s" ``` traytel@58916 ` 82` ``` "\ isl s \ projr s \ setr s" ``` traytel@58916 ` 83` ``` by (case_tac [!] s) (auto intro: setl.intros setr.intros) ``` traytel@58916 ` 84` traytel@58916 ` 85` ```lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \ ``` traytel@58916 ` 86` ``` (isl a \ isl b \ R1 (projl a) (projl b)) \ ``` traytel@58916 ` 87` ``` (\ isl a \ \ isl b \ R2 (projr a) (projr b)))" ``` traytel@58916 ` 88` ``` by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all ``` traytel@58916 ` 89` traytel@58916 ` 90` ```lemma isl_transfer: "rel_fun (rel_sum A B) (op =) isl isl" ``` traytel@58916 ` 91` ``` unfolding rel_fun_def rel_sum_sel by simp ``` traytel@58916 ` 92` traytel@58916 ` 93` ```lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \ R2 (snd p) (snd q))" ``` traytel@58916 ` 94` ``` by (force simp: rel_prod.simps elim: rel_prod.cases) ``` traytel@58916 ` 95` blanchet@58352 ` 96` ```ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" ``` blanchet@58352 ` 97` blanchet@58390 ` 98` ```ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" ``` blanchet@58377 ` 99` blanchet@62335 ` 100` ```lemma size_bool[code]: "size (b :: bool) = 0" ``` blanchet@58391 ` 101` ``` by (cases b) auto ``` blanchet@58391 ` 102` blanchet@58391 ` 103` ```declare prod.size[no_atp] ``` blanchet@58391 ` 104` blanchet@59819 ` 105` ```lemmas size_nat = size_nat_def ``` blanchet@58391 ` 106` blanchet@58353 ` 107` ```hide_const (open) xtor ctor_rec ``` blanchet@58353 ` 108` blanchet@58353 ` 109` ```hide_fact (open) ``` blanchet@58353 ` 110` ``` xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec ``` blanchet@58377 ` 111` ``` ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt ``` blanchet@58353 ` 112` blanchet@58352 ` 113` ```end ```