equal
deleted
inserted
replaced
22 using Card_order_ctwo by (unfold ctwo_def Field_card_of) |
22 using Card_order_ctwo by (unfold ctwo_def Field_card_of) |
23 |
23 |
24 lemma natLeq_cinfinite: "cinfinite natLeq" |
24 lemma natLeq_cinfinite: "cinfinite natLeq" |
25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
26 |
26 |
27 bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"] |
27 bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"] |
28 apply auto |
28 apply auto |
29 apply (rule natLeq_card_order) |
29 apply (rule natLeq_card_order) |
30 apply (rule natLeq_cinfinite) |
30 apply (rule natLeq_cinfinite) |
31 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
31 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
32 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on) |
32 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on) |
50 done |
50 done |
51 |
51 |
52 lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>" |
52 lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>" |
53 unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto |
53 unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto |
54 |
54 |
55 bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] |
55 bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] |
56 apply (auto simp add: wpull_id) |
56 apply (auto simp add: wpull_id) |
57 apply (rule card_order_csum) |
57 apply (rule card_order_csum) |
58 apply (rule natLeq_card_order) |
58 apply (rule natLeq_card_order) |
59 apply (rule card_of_card_order_on) |
59 apply (rule card_of_card_order_on) |
60 apply (rule cinfinite_csum) |
60 apply (rule cinfinite_csum) |
84 end; |
84 end; |
85 |
85 |
86 structure Basic_BNFs : BASIC_BNFS = |
86 structure Basic_BNFs : BASIC_BNFS = |
87 struct |
87 struct |
88 |
88 |
89 val ID_bnf = the (BNF_Def.bnf_of @{context} "ID"); |
89 val ID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.ID"); |
90 val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID"); |
90 val DEADID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.DEADID"); |
91 |
91 |
92 val rel_def = BNF_Def.rel_def_of_bnf ID_bnf; |
92 val rel_def = BNF_Def.rel_def_of_bnf ID_bnf; |
93 val ID_rel_def = rel_def RS sym; |
93 val ID_rel_def = rel_def RS sym; |
94 val ID_pred_def = Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym; |
94 val ID_pred_def = Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym; |
95 |
95 |
102 definition sum_setr :: "'a + 'b \<Rightarrow> 'b set" where |
102 definition sum_setr :: "'a + 'b \<Rightarrow> 'b set" where |
103 "sum_setr x = (case x of Inr z => {z} | _ => {})" |
103 "sum_setr x = (case x of Inr z => {z} | _ => {})" |
104 |
104 |
105 lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def] |
105 lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def] |
106 |
106 |
107 bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] |
107 bnf_def sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] |
108 proof - |
108 proof - |
109 show "sum_map id id = id" by (rule sum_map.id) |
109 show "sum_map id id = id" by (rule sum_map.id) |
110 next |
110 next |
111 fix f1 f2 g1 g2 |
111 fix f1 f2 g1 g2 |
112 show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" |
112 show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" |
238 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where |
238 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where |
239 "snds x = {snd x}" |
239 "snds x = {snd x}" |
240 |
240 |
241 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] |
241 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] |
242 |
242 |
243 bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] |
243 bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] |
244 proof (unfold prod_set_defs) |
244 proof (unfold prod_set_defs) |
245 show "map_pair id id = id" by (rule map_pair.id) |
245 show "map_pair id id = id" by (rule map_pair.id) |
246 next |
246 next |
247 fix f1 f2 g1 g2 |
247 fix f1 f2 g1 g2 |
248 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
248 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
356 qed |
356 qed |
357 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce |
357 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce |
358 ultimately show ?thesis using card_of_ordLeq by fast |
358 ultimately show ?thesis using card_of_ordLeq by fast |
359 qed |
359 qed |
360 |
360 |
361 bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" |
361 bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" |
362 ["%c x::'b::type. c::'a::type"] |
362 ["%c x::'b::type. c::'a::type"] |
363 proof |
363 proof |
364 fix f show "id \<circ> f = id f" by simp |
364 fix f show "id \<circ> f = id f" by simp |
365 next |
365 next |
366 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |
366 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |