author  traytel 
Mon, 15 Jul 2013 15:50:39 +0200  
changeset 52660  7f7311d04727 
parent 52659  58b87aa4dc3b 
child 52731  dacd47a0633f 
permissions  rwrr 
51850
106afdf5806c
renamed a few FPrelated files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51797
diff
changeset

1 
(* Title: HOL/BNF/BNF_FP_Basic.thy 
49308
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 

51740  6 
Basic 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

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

8 

51740  9 
header {* Basic 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

10 

51850
106afdf5806c
renamed a few FPrelated files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51797
diff
changeset

11 
theory BNF_FP_Basic 
51797  12 
imports BNF_Comp BNF_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

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 

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

19 

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

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

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

22 

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

23 
lemma unit_case_Unity: "(case u of () => f) = f" 
49312  24 
by (cases u) (hypsubst, rule unit.cases) 
25 

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

26 
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

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

28 

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

31 

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

33 
by clarify 

34 

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

36 
by auto 

37 

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

41 
lemma o_bij: 

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

45 
fix a1 a2 assume "f a1 = f a2" 

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

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

48 
next 

49 
fix b 

50 
have "b = f (g b)" 

51 
using fg unfolding fun_eq_iff by simp 

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

53 
qed 

54 

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

56 

57 
lemma sum_case_step: 

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

49312  60 
by auto 
61 

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

63 
by simp 

64 

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

66 
by blast 

67 

68 
lemma obj_sumE_f: 

69 
"\<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  70 
by (rule allI) (metis sumE) 
49312  71 

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

73 
by (cases s) auto 

74 

75 
lemma sum_case_if: 

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

77 
by simp 

78 

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

79 
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

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

81 

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

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

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

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

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

86 

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

87 
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

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

89 

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

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

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

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

93 
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

94 

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

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

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

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

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

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

100 
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

101 

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

102 
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

103 
"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

104 
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

105 

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 
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

107 
"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

108 
"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

109 
"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

110 
"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

111 
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

112 

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

113 
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

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

115 

51850
106afdf5806c
renamed a few FPrelated files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51797
diff
changeset

116 
ML_file "Tools/bnf_fp_util.ML" 
49636  117 
ML_file "Tools/bnf_fp_def_sugar_tactics.ML" 
118 
ML_file "Tools/bnf_fp_def_sugar.ML" 

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

119 

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

120 
end 