author  blanchet 
Mon, 20 Jan 2014 18:24:56 +0100  
changeset 55062  6d3fad6f01c9 
parent 55059  ef2e0fb783c6 
child 55066  4e5ddf3162ac 
permissions  rwrr 
55059  1 
(* Title: HOL/BNF_FP_Base.thy 
53311  2 
Author: Lorenz Panny, TU Muenchen 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

3 
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

4 
Author: Jasmin Blanchette, TU Muenchen 
53311  5 
Copyright 2012, 2013 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

6 

55059  7 
Shared fixed point operations on bounded natural functors. 
49308
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 

53311  10 
header {* Shared Fixed Point Operations on Bounded Natural Functors *} 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

11 

53311  12 
theory BNF_FP_Base 
55062  13 
imports Nitpick BNF_Comp Ctr_Sugar 
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP  this will be essential for bootstrapping
blanchet
parents:
diff
changeset

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

15 

49590  16 
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" 
17 
by auto 

18 

49591
91b228e26348
generate highlevel "coinduct" and "strong_coinduct" properties
blanchet
parents:
49590
diff
changeset

19 
lemma eq_sym_Unity_conv: "(x = (() = ())) = x" 
49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

20 
by blast 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

21 

53903  22 
lemma unit_case_Unity: "(case u of () \<Rightarrow> f) = f" 
49312  23 
by (cases u) (hypsubst, rule unit.cases) 
24 

49539
be6cbf960aa7
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
blanchet
parents:
49510
diff
changeset

25 
lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p" 
be6cbf960aa7
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
blanchet
parents:
49510
diff
changeset

26 
by simp 
be6cbf960aa7
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)
blanchet
parents:
49510
diff
changeset

27 

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

30 

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

32 
by clarify 

33 

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

35 
by auto 

36 

49683  37 
lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x" 
49312  38 
unfolding o_def fun_eq_iff by simp 
39 

40 
lemma o_bij: 

49683  41 
assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id" 
49312  42 
shows "bij f" 
43 
unfolding bij_def inj_on_def surj_def proof safe 

44 
fix a1 a2 assume "f a1 = f a2" 

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

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

47 
next 

48 
fix b 

49 
have "b = f (g b)" 

50 
using fg unfolding fun_eq_iff by simp 

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

52 
qed 

53 

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

55 

56 
lemma sum_case_step: 

49683  57 
"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" 
58 
"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" 

49312  59 
by auto 
60 

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

62 
by simp 

63 

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

65 
by blast 

66 

67 
lemma obj_sumE_f: 

68 
"\<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" 

52660  69 
by (rule allI) (metis sumE) 
49312  70 

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

72 
by (cases s) auto 

73 

74 
lemma sum_case_if: 

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

76 
by simp 

77 

49428
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

78 
lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)" 
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

79 
by blast 
93f158d59ead
handle the general case with more than two levels of nesting when discharging induction prem prems
blanchet
parents:
49427
diff
changeset

80 

49585
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

81 
lemma UN_compreh_eq_eq: 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

82 
"\<Union>{y. \<exists>x\<in>A. y = {}} = {}" 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

83 
"\<Union>{y. \<exists>x\<in>A. y = {x}} = A" 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

84 
by blast+ 
5c4a12550491
generate highlevel "maps", "sets", and "rels" properties
blanchet
parents:
49539
diff
changeset

85 

51745
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset

86 
lemma Inl_Inr_False: "(Inl x = Inr y) = False" 
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset

87 
by simp 
a06a3c777add
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
blanchet
parents:
51740
diff
changeset

88 

49429
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

89 
lemma prod_set_simps: 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

90 
"fsts (x, y) = {x}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

91 
"snds (x, y) = {y}" 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

92 
unfolding fsts_def snds_def by simp+ 
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

93 

64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

94 
lemma sum_set_simps: 
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

95 
"setl (Inl x) = {x}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

96 
"setl (Inr x) = {}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

97 
"setr (Inl x) = {}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

98 
"setr (Inr x) = {x}" 
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49430
diff
changeset

99 
unfolding sum_set_defs by simp+ 
49429
64ac3471005a
cleaner way of dealing with the set functions of sums and products
blanchet
parents:
49428
diff
changeset

100 

49642
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

101 
lemma prod_rel_simp: 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

102 
"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'" 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

103 
unfolding prod_rel_def by simp 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

104 

9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

105 
lemma sum_rel_simps: 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

106 
"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'" 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

107 
"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'" 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

108 
"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False" 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

109 
"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False" 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

110 
unfolding sum_rel_def by simp+ 
9f884142334c
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
blanchet
parents:
49636
diff
changeset

111 

52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset

112 
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" 
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset

113 
by blast 
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52349
diff
changeset

114 

52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

115 
lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

116 
unfolding o_def fun_eq_iff by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

117 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

118 
lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

119 
unfolding o_def fun_eq_iff by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

120 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

121 
lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

122 
unfolding o_def fun_eq_iff by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

123 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

124 
lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

125 
unfolding o_def fun_eq_iff by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

126 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

127 
lemma convol_o: "<f, g> o h = <f o h, g o h>" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

128 
unfolding convol_def by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

129 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

130 
lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

131 
unfolding convol_def by auto 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

132 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

133 
lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

134 
unfolding map_pair_o_convol id_o o_id .. 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

135 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

136 
lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

137 
unfolding o_def by (auto split: sum.splits) 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

138 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

139 
lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

140 
unfolding o_def by (auto split: sum.splits) 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

141 

2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

142 
lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x" 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

143 
unfolding sum_case_o_sum_map id_o o_id .. 
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52731
diff
changeset

144 

52731  145 
lemma fun_rel_def_butlast: 
146 
"(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))" 

147 
unfolding fun_rel_def .. 

148 

53105
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

149 
lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)" 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

150 
by auto 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

151 

ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

152 
lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

153 
by auto 
ec38e9f4352f
simpler (forward) derivation of strong (upto equality) coinduction properties
traytel
parents:
52913
diff
changeset

154 

53308  155 
lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)" 
156 
unfolding Grp_def id_apply by blast 

157 

158 
lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv> 

159 
(\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)" 

160 
unfolding Grp_def by rule auto 

161 

55062  162 
ML_file "Tools/BNF/bnf_fp_util.ML" 
163 
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" 

164 
ML_file "Tools/BNF/bnf_fp_def_sugar.ML" 

165 
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" 

166 
ML_file "Tools/BNF/bnf_fp_n2m.ML" 

167 
ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" 

168 
ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML" 

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

169 

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

170 
end 