author  blanchet 
Wed, 12 Sep 2012 10:35:56 +0200  
changeset 49325  340844cbf7af 
parent 49312  c874ff5658dc 
child 49335  096967bf3940 
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 

20 
(* FIXME: needed? *) 

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

22 

23 
(* FIXME: needed? *) 

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

25 

26 
(* FIXME: needed? *) 

27 
lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True" 

28 
by presburger 

29 

30 
(* FIXME: needed? *) 

31 
lemma all_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)" 

32 
by presburger 

33 

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

35 
by simp 

36 

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

38 
by simp 

39 

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

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

42 

43 
lemma fst_convol: 

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

45 
apply(rule ext) 

46 
unfolding convol_def by simp 

47 

48 
lemma snd_convol: 

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

50 
apply(rule ext) 

51 
unfolding convol_def by simp 

52 

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

54 
unfolding o_def fun_eq_iff by simp 

55 

56 
lemma o_bij: 

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

58 
shows "bij f" 

59 
unfolding bij_def inj_on_def surj_def proof safe 

60 
fix a1 a2 assume "f a1 = f a2" 

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

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

63 
next 

64 
fix b 

65 
have "b = f (g b)" 

66 
using fg unfolding fun_eq_iff by simp 

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

68 
qed 

69 

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

71 

72 
lemma sum_case_step: 

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

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

75 
by auto 

76 

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

78 
by simp 

79 

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

81 
by blast 

82 

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

85 
by (cases x) blast+ 

86 

49312  87 
lemma obj_sumE_f: 
88 
"\<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  89 
by (rule allI) (rule obj_sumE_f') 
49312  90 

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

92 
by (cases s) auto 

93 

49325  94 
lemma obj_sum_step': 
95 
"\<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" 

96 
by (cases x) blast+ 

97 

49312  98 
lemma obj_sum_step: 
49325  99 
"\<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" 
100 
by (rule allI) (rule obj_sum_step') 

49312  101 

102 
lemma sum_case_if: 

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

104 
by simp 

105 

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

106 
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

107 
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

108 
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

109 

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

110 
end 