author  haftmann 
Sat, 25 May 2013 15:44:29 +0200  
changeset 52141  eff000cab70f 
parent 51893  596baae88a88 
child 52660  7f7311d04727 
permissions  rwrr 
49509
163914705f8d
renamed toplevel theory from "Codatatype" to "BNF"
blanchet
parents:
49463
diff
changeset

1 
(* Title: HOL/BNF/BNF_Comp.thy 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

2 
Author: Dmitriy Traytel, TU Muenchen 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

3 
Copyright 2012 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

4 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

5 
Composition of bounded natural functors. 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

6 
*) 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

7 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

8 
header {* Composition of Bounded Natural Functors *} 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

9 

7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

10 
theory BNF_Comp 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

11 
imports Basic_BNFs 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

12 
begin 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

13 

49312  14 
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})" 
15 
by (rule ext) simp 

16 

17 
lemma Union_natural: "Union o image (image f) = image f o Union" 

18 
by (rule ext) (auto simp only: o_apply) 

19 

20 
lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A" 

21 
by (unfold o_assoc) 

22 

23 
lemma comp_single_set_bd: 

24 
assumes fbd_Card_order: "Card_order fbd" and 

25 
fset_bd: "\<And>x. fset x \<le>o fbd" and 

26 
gset_bd: "\<And>x. gset x \<le>o gbd" 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset

27 
shows "\<Union>(fset ` gset x) \<le>o gbd *c fbd" 
49312  28 
apply (subst sym[OF SUP_def]) 
29 
apply (rule ordLeq_transitive) 

30 
apply (rule card_of_UNION_Sigma) 

31 
apply (subst SIGMA_CSUM) 

32 
apply (rule ordLeq_transitive) 

33 
apply (rule card_of_Csum_Times') 

34 
apply (rule fbd_Card_order) 

35 
apply (rule ballI) 

36 
apply (rule fset_bd) 

37 
apply (rule ordLeq_transitive) 

38 
apply (rule cprod_mono1) 

39 
apply (rule gset_bd) 

40 
apply (rule ordIso_imp_ordLeq) 

41 
apply (rule ordIso_refl) 

42 
apply (rule Card_order_cprod) 

43 
done 

44 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset

45 
lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)" 
49312  46 
by simp 
47 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset

48 
lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A" 
49312  49 
by simp 
50 

51 
lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F" 

52 
by (rule ext) (auto simp add: collect_def) 

53 

54 
lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" 

55 
by blast 

56 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset

57 
lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" 
49312  58 
by blast 
59 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset

60 
lemma comp_set_bd_Union_o_collect: "\<Union>\<Union>((\<lambda>f. f x) ` X) \<le>o hbd \<Longrightarrow> (Union \<circ> collect X) x \<le>o hbd" 
49312  61 
by (unfold o_apply collect_def SUP_def) 
62 

63 
lemma wpull_cong: 

64 
"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2" 

65 
by simp 

66 

67 
lemma Id_def': "Id = {(a,b). a = b}" 

68 
by auto 

69 

70 
lemma Gr_fst_snd: "(Gr R fst)^1 O Gr R snd = R" 

71 
unfolding Gr_def by auto 

72 

49512  73 
lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^1 O Gr A g = (Gr B f)^1 O Gr B g" 
49463  74 
by simp 
75 

51893
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset

76 
lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^1 OO Grp (Collect (split R)) snd = R" 
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset

77 
unfolding Grp_def fun_eq_iff relcompp.simps by auto 
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset

78 

596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset

79 
lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^1 OO Grp A g = (Grp B f)^1 OO Grp B g" 
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset

80 
by simp 
596baae88a88
got rid of the set based relatoruse (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset

81 

49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset

82 
ML_file "Tools/bnf_comp_tactics.ML" 
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset

83 
ML_file "Tools/bnf_comp.ML" 
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset

84 

48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset

85 
end 