|
1 theory Dlist imports |
|
2 "HOL-Library.Confluent_Quotient" |
|
3 begin |
|
4 |
|
5 context begin |
|
6 |
|
7 qualified definition dlist_eq where "dlist_eq = BNF_Def.vimage2p remdups remdups (=)" |
|
8 |
|
9 lemma equivp_dlist_eq: "equivp dlist_eq" |
|
10 unfolding dlist_eq_def by(rule equivp_vimage2p)(rule identity_equivp) |
|
11 |
|
12 quotient_type 'a dlist = "'a list" / dlist_eq |
|
13 by (rule equivp_dlist_eq) |
|
14 |
|
15 qualified inductive double :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
|
16 "double (xs @ ys) (xs @ x # ys)" if "x \<in> set ys" |
|
17 |
|
18 qualified lemma strong_confluentp_double: "strong_confluentp double" |
|
19 proof |
|
20 fix xs ys zs :: "'a list" |
|
21 assume ys: "double xs ys" and zs: "double xs zs" |
|
22 consider (left) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ y # bs @ cs" "zs = as @ bs @ z # cs" "y \<in> set (bs @ cs)" "z \<in> set cs" |
|
23 | (right) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ bs @ y # cs" "zs = as @ z # bs @ cs" "y \<in> set cs" "z \<in> set (bs @ cs)" |
|
24 proof - |
|
25 show thesis using ys zs |
|
26 by(clarsimp simp add: double.simps append_eq_append_conv2)(auto intro: that) |
|
27 qed |
|
28 then show "\<exists>us. double\<^sup>*\<^sup>* ys us \<and> double\<^sup>=\<^sup>= zs us" |
|
29 proof cases |
|
30 case left |
|
31 let ?us = "as @ y # bs @ z # cs" |
|
32 have "double ys ?us" "double zs ?us" using left |
|
33 by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+ |
|
34 then show ?thesis by blast |
|
35 next |
|
36 case right |
|
37 let ?us = "as @ z # bs @ y # cs" |
|
38 have "double ys ?us" "double zs ?us" using right |
|
39 by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+ |
|
40 then show ?thesis by blast |
|
41 qed |
|
42 qed |
|
43 |
|
44 qualified lemma double_Cons1 [simp]: "double xs (x # xs)" if "x \<in> set xs" |
|
45 using double.intros[of x xs "[]"] that by simp |
|
46 |
|
47 qualified lemma double_Cons_same [simp]: "double xs ys \<Longrightarrow> double (x # xs) (x # ys)" |
|
48 by(auto simp add: double.simps Cons_eq_append_conv) |
|
49 |
|
50 qualified lemma doubles_Cons_same: "double\<^sup>*\<^sup>* xs ys \<Longrightarrow> double\<^sup>*\<^sup>* (x # xs) (x # ys)" |
|
51 by(induction rule: rtranclp_induct)(auto intro: rtranclp.rtrancl_into_rtrancl) |
|
52 |
|
53 qualified lemma remdups_into_doubles: "double\<^sup>*\<^sup>* (remdups xs) xs" |
|
54 by(induction xs)(auto intro: doubles_Cons_same rtranclp.rtrancl_into_rtrancl) |
|
55 |
|
56 qualified lemma dlist_eq_into_doubles: "dlist_eq \<le> equivclp double" |
|
57 by(auto 4 4 simp add: dlist_eq_def vimage2p_def |
|
58 intro: equivclp_trans converse_rtranclp_into_equivclp rtranclp_into_equivclp remdups_into_doubles) |
|
59 |
|
60 qualified lemma factor_double_map: "double (map f xs) ys \<Longrightarrow> \<exists>zs. dlist_eq xs zs \<and> ys = map f zs" |
|
61 by(auto simp add: double.simps dlist_eq_def vimage2p_def map_eq_append_conv) |
|
62 (metis list.simps(9) map_append remdups.simps(2) remdups_append2) |
|
63 |
|
64 qualified lemma dlist_eq_set_eq: "dlist_eq xs ys \<Longrightarrow> set xs = set ys" |
|
65 by(simp add: dlist_eq_def vimage2p_def)(metis set_remdups) |
|
66 |
|
67 qualified lemma dlist_eq_map_respect: "dlist_eq xs ys \<Longrightarrow> dlist_eq (map f xs) (map f ys)" |
|
68 by(clarsimp simp add: dlist_eq_def vimage2p_def)(metis remdups_map_remdups) |
|
69 |
|
70 qualified lemma confluent_quotient_dlist: |
|
71 "confluent_quotient double dlist_eq dlist_eq dlist_eq dlist_eq dlist_eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set" |
|
72 by(unfold_locales)(auto intro: strong_confluentp_imp_confluentp strong_confluentp_double dest: factor_double_map dlist_eq_into_doubles[THEN predicate2D] dlist_eq_set_eq simp add: list.in_rel list.rel_compp dlist_eq_map_respect equivp_dlist_eq equivp_imp_transp) |
|
73 |
|
74 lift_bnf 'a dlist [wits: "[]"] |
|
75 subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_dlist]) |
|
76 subgoal by(force dest: dlist_eq_set_eq intro: equivp_reflp[OF equivp_dlist_eq]) |
|
77 subgoal by(auto simp add: dlist_eq_def vimage2p_def) |
|
78 done |
|
79 |
|
80 end |
|
81 |
|
82 end |