author  blanchet 
Fri, 14 Sep 2012 12:09:27 +0200  
changeset 49368  df359ce891ac 
parent 49335  096967bf3940 
child 49372  c62165188971 
permissions  rwrr 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Codatatype/BNF_FP.thy 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

2 
Author: Dmitriy Traytel, TU Muenchen 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

4 
Copyright 2012 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

5 

6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

6 
Composition of bounded natural functors. 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

7 
*) 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

8 

6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

9 
header {* Composition of Bounded Natural Functors *} 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

10 

6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

11 
theory BNF_FP 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

12 
imports BNF_Comp BNF_Wrap 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

13 
keywords 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

14 
"defaults" 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

15 
begin 
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

16 

49312  17 
lemma case_unit: "(case u of () => f) = f" 
18 
by (cases u) (hypsubst, rule unit.cases) 

19 

49335  20 
lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" 
21 
by simp 

22 

23 
lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" 

24 
by clarify 

25 

26 
lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" 

27 
by auto 

28 

49368  29 
lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" 
30 
by simp 

49312  31 

49368  32 
lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" 
33 
by clarsimp 

49312  34 

35 
lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a" 

36 
by simp 

37 

38 
lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D" 

39 
by simp 

40 

41 
definition convol ("<_ , _>") where 

42 
"<f , g> \<equiv> %a. (f a, g a)" 

43 

44 
lemma fst_convol: 

45 
"fst o <f , g> = f" 

46 
apply(rule ext) 

47 
unfolding convol_def by simp 

48 

49 
lemma snd_convol: 

50 
"snd o <f , g> = g" 

51 
apply(rule ext) 

52 
unfolding convol_def by simp 

53 

54 
lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x" 

55 
unfolding o_def fun_eq_iff by simp 

56 

57 
lemma o_bij: 

58 
assumes gf: "g o f = id" and fg: "f o g = id" 

59 
shows "bij f" 

60 
unfolding bij_def inj_on_def surj_def proof safe 

61 
fix a1 a2 assume "f a1 = f a2" 

62 
hence "g ( f a1) = g (f a2)" by simp 

63 
thus "a1 = a2" using gf unfolding fun_eq_iff by simp 

64 
next 

65 
fix b 

66 
have "b = f (g b)" 

67 
using fg unfolding fun_eq_iff by simp 

68 
thus "EX a. b = f a" by blast 

69 
qed 

70 

71 
lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp 

72 

73 
lemma sum_case_step: 

74 
"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" 

75 
"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" 

76 
by auto 

77 

78 
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

79 
by simp 

80 

81 
lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P" 

82 
by blast 

83 

49325  84 
lemma obj_sumE_f': 
85 
"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f x \<longrightarrow> P" 

86 
by (cases x) blast+ 

87 

49312  88 
lemma obj_sumE_f: 
89 
"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P" 

49325  90 
by (rule allI) (rule obj_sumE_f') 
49312  91 

92 
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

93 
by (cases s) auto 

94 

49325  95 
lemma obj_sum_step': 
96 
"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> s = f (Inr x) \<longrightarrow> P" 

97 
by (cases x) blast+ 

98 

49312  99 
lemma obj_sum_step: 
49325  100 
"\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P" 
101 
by (rule allI) (rule obj_sum_step') 

49312  102 

103 
lemma sum_case_if: 

104 
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" 

105 
by simp 

106 

49368  107 
lemma UN_compreh_bex: 
108 
"\<Union>{y. \<exists>x \<in> A. y = {}} = {}" 

109 
"\<Union>{y. \<exists>x \<in> A. y = {x}} = A" 

110 
by blast+ 

111 

112 
lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C" 

113 
apply (rule exI) 

114 
apply (rule conjI) 

115 
apply (rule bexI) 

116 
apply (rule refl) 

117 
apply assumption 

118 
apply assumption 

119 
done 

120 

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

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

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

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

124 

49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

125 
end 