equal
deleted
inserted
replaced
|
1 (* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *) |
1 theory Myhill_2 |
2 theory Myhill_2 |
2 imports Myhill_1 "~~/src/HOL/Library/List_Prefix" |
3 imports Myhill_1 "~~/src/HOL/Library/List_Prefix" |
3 begin |
4 begin |
4 |
5 |
5 section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *} |
6 section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *} |
54 where "x \<in> X" "y \<in> Y" "tag x = tag y" |
55 where "x \<in> X" "y \<in> Y" "tag x = tag y" |
55 unfolding quotient_def Image_def image_def tag_eq_def |
56 unfolding quotient_def Image_def image_def tag_eq_def |
56 by (simp) (blast) |
57 by (simp) (blast) |
57 with X_in Y_in |
58 with X_in Y_in |
58 have "X = Y" |
59 have "X = Y" |
59 unfolding quotient_def tag_eq_def by auto |
60 unfolding quotient_def tag_eq_def by auto |
60 } |
61 } |
61 then show "inj_on ?f ?A" unfolding inj_on_def by auto |
62 then show "inj_on ?f ?A" unfolding inj_on_def by auto |
62 qed |
63 qed |
63 ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD) |
64 ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD) |
64 qed |
65 qed |
322 |
323 |
323 lemma finite_set_has_max2: |
324 lemma finite_set_has_max2: |
324 "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max" |
325 "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max" |
325 apply(induct rule:finite.induct) |
326 apply(induct rule:finite.induct) |
326 apply(simp) |
327 apply(simp) |
327 by (metis (full_types) all_not_in_conv insert_iff linorder_linear order_trans) |
328 by (metis (hide_lams, no_types) all_not_in_conv insert_iff linorder_le_cases order_trans) |
328 |
329 |
329 lemma finite_strict_prefix_set: |
330 lemma finite_strict_prefix_set: |
330 shows "finite {xa. xa < (x::'a list)}" |
331 shows "finite {xa. xa < (x::'a list)}" |
331 apply (induct x rule:rev_induct, simp) |
332 apply (induct x rule:rev_induct, simp) |
332 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
333 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |