7 |
7 |
8 lemma fset_exhaust[case_names fempty finsert, cases type: fset]: |
8 lemma fset_exhaust[case_names fempty finsert, cases type: fset]: |
9 shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
9 shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
10 by (lifting list.exhaust) |
10 by (lifting list.exhaust) |
11 |
11 |
12 (* PROBLEM: these lemmas needs to be restated, since *) |
12 lemma list_rel_find_element: |
13 (* concat.simps(1) and concat.simps(2) contain the *) |
13 assumes a: "x \<in> set a" |
14 (* type variables ?'a1.0 (which are turned into frees *) |
14 and b: "list_rel R a b" |
15 (* 'a_1 *) |
15 shows "\<exists>y. (y \<in> set b \<and> R x y)" |
16 |
16 proof - |
17 lemma concat1: |
17 have "length a = length b" using b by (rule list_rel_len) |
18 shows "concat [] \<approx> []" |
18 then show ?thesis using a b proof (induct a b rule: list_induct2) |
19 by (simp) |
19 case Nil |
20 |
20 show ?case using Nil.prems by simp |
21 lemma concat2: |
21 next |
22 shows "concat (x # xs) \<approx> x @ concat xs" |
22 case (Cons x xs y ys) |
23 by (simp) |
23 show ?case using Cons by auto |
24 |
24 qed |
25 lemma concat_rsp: |
25 qed |
26 "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y" |
26 |
27 apply (induct x y arbitrary: x' y' rule: list_induct2') |
27 lemma concat_rsp_pre: |
|
28 "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y; \<exists>x\<in>set x. xa \<in> set x\<rbrakk> \<Longrightarrow> |
|
29 \<exists>x\<in>set y. xa \<in> set x" |
|
30 apply clarify |
|
31 apply (frule list_rel_find_element[of _ "x"]) |
|
32 apply assumption |
|
33 apply clarify |
|
34 apply (subgoal_tac "ya \<in> set y'") |
|
35 prefer 2 |
28 apply simp |
36 apply simp |
29 defer defer |
37 apply (frule list_rel_find_element[of _ "y'"]) |
30 apply (simp only: concat.simps) |
38 apply assumption |
31 sorry |
39 apply auto |
|
40 done |
32 |
41 |
33 lemma [quot_respect]: |
42 lemma [quot_respect]: |
34 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
43 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
35 apply (simp only: fun_rel_def) |
44 apply (simp only: fun_rel_def) |
36 apply clarify |
45 apply clarify |
37 apply (rule concat_rsp) |
46 apply (simp (no_asm)) |
|
47 apply rule |
|
48 apply rule |
|
49 apply (erule concat_rsp_pre) |
38 apply assumption+ |
50 apply assumption+ |
|
51 apply (rule concat_rsp_pre) |
|
52 prefer 4 |
|
53 apply assumption |
|
54 apply (rule list_rel_symp[OF list_eq_equivp]) |
|
55 apply assumption |
|
56 apply (rule equivp_symp[OF list_eq_equivp]) |
|
57 apply assumption |
|
58 apply (rule list_rel_symp[OF list_eq_equivp]) |
|
59 apply assumption |
39 done |
60 done |
40 |
61 |
41 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
62 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
42 by (metis nil_rsp list_rel.simps(1) pred_compI) |
63 by (metis nil_rsp list_rel.simps(1) pred_compI) |
43 |
64 |
44 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
65 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
45 apply (rule eq_reflection) |
66 by (rule eq_reflection) auto |
46 apply auto |
|
47 done |
|
48 |
67 |
49 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
68 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
50 unfolding list_eq.simps |
69 unfolding list_eq.simps |
51 apply(simp only: set_map set_in_eq) |
70 by (simp only: set_map set_in_eq) |
52 done |
|
53 |
71 |
54 lemma quotient_compose_list_pre: |
72 lemma quotient_compose_list_pre: |
55 "(list_rel op \<approx> OOO op \<approx>) r s = |
73 "(list_rel op \<approx> OOO op \<approx>) r s = |
56 ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and> |
74 ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and> |
57 abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
75 abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
104 lemma quotient_compose_list[quot_thm]: |
122 lemma quotient_compose_list[quot_thm]: |
105 shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>)) |
123 shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>)) |
106 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
124 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
107 unfolding Quotient_def comp_def |
125 unfolding Quotient_def comp_def |
108 apply (rule)+ |
126 apply (rule)+ |
109 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
127 apply (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) |
110 apply (rule) |
128 apply (rule) |
111 apply (rule) |
129 apply (rule) |
112 apply (rule) |
130 apply (rule) |
113 apply (rule list_rel_refl) |
131 apply (rule list_rel_refl) |
114 apply (metis equivp_def fset_equivp) |
132 apply (metis equivp_def fset_equivp) |