author  blanchet 
Fri, 19 Sep 2014 13:27:04 +0200  
changeset 58390  b74d8470b98e 
parent 58377  c6f93b8d2d8e 
child 58391  fe0fc8aee49a 
permissions  rwrr 
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Basic_BNF_Least_Fixpoints.thy 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

3 
Copyright 2014 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

4 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

5 
Registration of basic types as BNF least fixpoints (datatypes). 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

6 
*) 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

7 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

8 
theory Basic_BNF_Least_Fixpoints 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

9 
imports BNF_Least_Fixpoint 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

10 
begin 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

11 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

12 
definition xtor :: "'a \<Rightarrow> 'a" where 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

13 
"xtor x = x" 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

14 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

15 
lemma xtor_map: "f (xtor x) = xtor (f x)" 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

16 
unfolding xtor_def by (rule refl) 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

17 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

18 
lemma xtor_set: "f (xtor x) = f x" 
58353  19 
unfolding xtor_def by (rule refl) 
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

20 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

21 
lemma xtor_rel: "R (xtor x) (xtor y) = R x y" 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

22 
unfolding xtor_def by (rule refl) 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

23 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

24 
lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z" 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

25 
unfolding xtor_def by assumption 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

26 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

27 
lemma xtor_xtor: "xtor (xtor x) = x" 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

28 
unfolding xtor_def by (rule refl) 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

29 

37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

30 
lemmas xtor_inject = xtor_rel[of "op ="] 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

31 

58353  32 
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" 
33 
unfolding xtor_def vimage2p_def id_bnf_def by default 

58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

34 

58353  35 
lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))" 
36 
unfolding xtor_def id_bnf_def by (rule reflexive) 

58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

37 

58353  38 
lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))" 
39 
unfolding xtor_def id_bnf_def by (rule reflexive) 

58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

40 

58353  41 
lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))" 
42 
unfolding xtor_def id_bnf_def by (rule reflexive) 

58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

43 

58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

44 
definition ctor_rec :: "'a \<Rightarrow> 'a" where 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

45 
"ctor_rec x = x" 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

46 

c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

47 
lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)" 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

48 
unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

49 

c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

50 
lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)" 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

51 
unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

52 

c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

53 
lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))" 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

54 
unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) 
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

55 

58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

56 
ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" 
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

57 

58390
b74d8470b98e
keep obsolete interpretations in Main, to avoid merge trouble
blanchet
parents:
58377
diff
changeset

58 
ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" 
58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

59 

58353  60 
hide_const (open) xtor ctor_rec 
61 

62 
hide_fact (open) 

63 
xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec 

58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset

64 
ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt 
58353  65 

58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset

66 
end 