1open HolKernel Parse boolLib bossLib
2
3open dividesTheory
4
5val _ = new_theory "ward"
6
7val list_exp_def = Define`
8  (list_exp l 0 = []) ���
9  (list_exp l (SUC n) = l ++ list_exp l n)
10`;
11
12
13
14val _ = Hol_datatype `alphabet = a | b | I`
15
16val (thm_rules, thm_ind, thm_cases) = Hol_reln`
17  thm [I] ���
18  (���x y. thm (x ++ y) ��� thm (x ++ [I] ++ y)) ���
19  (���x y. x ++ y ��� [] ��� thm (x ++ [I] ++ y) ��� thm (x ++ y)) ���
20  (���x y. thm (x ++ [I] ++ y) ��� thm (x ++ [a;a;a] ++ y)) ���
21  (���x y. thm (x ++ [a;a;a] ++ y) ��� thm (x ++ [I] ++ y)) ���
22  (���x y. thm (x ++ [I] ++ y) ��� thm (x ++ [b;b;b] ++ y)) ���
23  (���x y. thm (x ++ [b;b;b] ++ y) ��� thm (x ++ [I] ++ y)) ���
24  (���x y. thm (x ++ [a;b;a;b] ++ y) ��� thm (x ++ [b;b;a;a] ++ y)) ���
25  (���x y. thm (x ++ [b;b;a;a] ++ y) ��� thm (x ++ [a;b;a;b] ++ y))
26`
27open lcsymtacs
28val div3_lemma = prove(
29  ``divides 3 (x + 3 + y) ��� divides 3 (x + y)``,
30  `x + 3 + y = x + y + 3` by DECIDE_TAC THEN
31  SRW_TAC [][] THEN
32  EQ_TAC THENL [
33    METIS_TAC [arithmeticTheory.ADD_COMM, DIVIDES_REFL,
34               DIVIDES_ADD_2],
35    METIS_TAC [DIVIDES_REFL, DIVIDES_ADD_1]
36  ])
37
38val ab_DIV3 = store_thm(
39  "ab_DIV3",
40  ``���l. thm l ��� divides 3 (LENGTH (FILTER ((=) a) l)) ���
41                divides 3 (LENGTH (FILTER ((=) b) l))``,
42  Induct_on `thm` THEN SRW_TAC [][listTheory.FILTER_APPEND_DISTRIB,
43                                  div3_lemma]);
44
45val (thmrwt_rules, thmrwt_ind, thmrwt_cases) = Hol_reln`
46  (���x y. (x ++ y ��� []) ��� thmrwt (x ++ [I] ++ y) (x ++ y)) ���
47  (���x y. thmrwt (x ++ [a;a;a] ++ y) (x ++ [I] ++ y)) ���
48  (���x y. thmrwt (x ++ [b;b;b] ++ y) (x ++ [I] ++ y)) ���
49  (���x y. thmrwt (x ++ [a;b;a;b] ++ y) (x ++ [b;b;a;a] ++ y)) ���
50  (���x y. thmrwt (x ++ [b;b;a;a;b;b] ++ y) (x ++ [a;b;a] ++ y)) ���
51  (���x y. thmrwt (x ++ [a;a;b;b;a;a] ++ y) (x ++ [b;a;b] ++ y)) ���
52  (���x y. thmrwt (x ++ [a;a;b;b] ++ y) (x ++ [b;a;b;a] ++ y))
53`;
54
55fun thm i = List.nth(CONJUNCTS thmrwt_rules, i)
56
57val alphanil_t = ``[] : alphabet list``
58
59fun lmkapp l = listSyntax.list_mk_append l handle HOL_ERR _ => alphanil_t
60
61datatype accitem = TM of term | CONSLR of term list
62
63fun strcons acc changedp t =
64    if listSyntax.is_cons t then let
65        val (h, hs_t) = listSyntax.dest_cons t
66      in
67        strcons (h::acc) true hs_t
68      end
69    else (acc, changedp, if listSyntax.is_nil t then NONE else SOME t)
70
71fun stripapp worklist acc =
72    case worklist of
73      [] => let
74        fun foldthis (TM t, acc) = t::acc
75          | foldthis (CONSLR ts, acc) =
76              listSyntax.mk_list (List.rev ts, type_of (hd ts)) :: acc
77      in
78        List.foldl foldthis [] acc
79      end
80    | t::ts => let
81        open listSyntax
82      in
83        if is_append t then let
84            val (l1, l2) = dest_append t
85          in
86            stripapp (l1 :: l2 :: ts) acc
87          end
88        else let
89            val (consbase, accrest) = case acc of
90                                        CONSLR l::rest => (l, rest)
91                                      | _ => ([], acc)
92          in
93            case strcons consbase false t of
94              ([], _, NONE) => stripapp ts acc
95            | (els, _, NONE) => stripapp ts (CONSLR els :: accrest)
96            | (_, false, SOME t') => stripapp ts (TM t'::acc)
97            | (els, true, SOME t') => stripapp (t'::ts) (CONSLR els :: accrest)
98          end
99      end
100
101datatype ('key, 'a) cons_trie =
102         Node of 'a option * ('key,('key,'a) cons_trie) Binarymap.dict
103
104fun find_trie_matches key trie = let
105  fun recurse pfxr acc key (Node (valopt, d)) = let
106    val newacc =
107        case valopt of
108          NONE => acc
109        | SOME r => (List.rev pfxr, r) :: acc
110  in
111    case key of
112      [] => newacc
113    | e::es => let
114      in
115        case Binarymap.peek (d, e) of
116          NONE => newacc
117        | SOME trie' => recurse (e::pfxr) newacc es trie'
118      end
119  end
120in
121  recurse [] [] key trie
122end
123
124fun empty cmp = Node(NONE, Binarymap.mkDict cmp)
125
126fun insert cmp (k,v) (Node(valopt,d)) =
127    case k of
128      [] => Node(SOME v, d)
129    | e::es => let
130      in
131        case Binarymap.peek (d, e) of
132          NONE => let
133            val temp' = insert cmp (es,v) (empty cmp)
134          in
135            Node(valopt, Binarymap.insert(d,e,temp'))
136          end
137        | SOME t' => Node(valopt, Binarymap.insert(d,e,insert cmp(es,v) t'))
138      end
139
140val db = let
141  fun foldthis ((t,v), acc) = let
142    val (els, _) = listSyntax.dest_list t
143  in
144    insert Term.compare (els,v) acc
145  end
146in
147  List.foldl foldthis (empty Term.compare)
148             [(``[I:alphabet]``, (alphanil_t, thm 0)),
149              (``[a;a;a]``,  (``[I:alphabet]``, thm 1)),
150              (``[b;b;b]``, (``[I:alphabet]``, thm 2)),
151              (``[a;b;a;b]``, (``[b;b;a;a]``, thm 3)),
152              (``[b;b;a;a;b;b]``, (``[a;b;a]``, thm 4)),
153              (``[a;a;b;b;a;a]``, (``[b;a;b]``, thm 5)),
154              (``[a;a;b;b]``, (``[b;a;b;a]``, thm 6))]
155end
156
157fun find_cons_matches db els =
158    case els of
159      [] => let
160        val res = find_trie_matches els db
161      in
162        map (fn v => ([],v,[])) res
163      end
164    | t::ts => let
165        val hdres = find_trie_matches els db
166        fun mapthis (v as (k,r)) = ([], v, List.drop(els,length k))
167        val hdres' = map mapthis hdres
168        val tlres = find_cons_matches db ts
169      in
170        (hdres' @ map (fn (p,v,s) => (t::p,v,s)) tlres)
171      end
172val alpha_ty = ``:alphabet``
173fun find_app_matches db app_list = let
174  fun recurse pfxr acc apps =
175    case apps of
176      [] => acc
177    | t::ts => let
178        val els = #1 (listSyntax.dest_list t) handle HOL_ERR _ => []
179        val t_results0 = find_cons_matches db els
180        fun mapthis (p,r,s) = let
181          val p_l = if null p then [] else [listSyntax.mk_list(p, alpha_ty)]
182          val s_l = if null s then [] else [listSyntax.mk_list(s, alpha_ty)]
183        in
184          (List.rev(p_l @ pfxr), r, s_l @ ts)
185        end
186        val results = map mapthis t_results0
187      in
188        recurse (t::pfxr) (acc @ results) ts
189      end
190in
191  recurse [] [] app_list
192end
193
194open listTheory
195
196fun solver (asl, t) = let
197  val nonnil_asms = map ASSUME (filter is_neg asl)
198  fun munge extras p s th =
199      th |> SPECL [lmkapp p, lmkapp s]
200         |> REWRITE_RULE (GSYM APPEND_ASSOC :: APPEND_eq_NIL :: APPEND ::
201                          APPEND_NIL :: NOT_NIL_CONS :: NOT_CONS_NIL ::
202                          extras @ nonnil_asms)
203         |> MATCH_MP relationTheory.RTC_SUBSET
204  val (_,body) = dest_exists t
205in
206  if is_conj body then let
207      val (c1, c2) = dest_conj body
208      val (_, [_, x1, _]) = strip_comb c1
209      val (_, [_, x2, _]) = strip_comb c2
210      val app_args1 = stripapp [x1] []
211      val app_args2 = stripapp [x2] []
212      val possibilities1 = find_app_matches db app_args1
213      val possibilities2 = find_app_matches db app_args2
214      fun nilf t = if listSyntax.is_nil t then [] else [t]
215      fun check (p1, (_, (res1, _)), s1) (p2, (_, (res2, _)), s2) =
216          p1 @ nilf res1 @ s1 = p2 @ nilf res2 @ s2
217      fun checkl t = List.mapPartial (fn t' => if check t t' then SOME (t,t')
218                                               else NONE)
219      fun checkll [] p2 = []
220        | checkll (h::t) p2 = checkl h p2 @ checkll t p2
221      val possibilities = checkll possibilities1 possibilities2
222      val ((pfx1, (_, (res1, th1)), sfx1), (pfx2, (_, (res2, th2)), sfx2)) =
223          hd possibilities
224      fun conclude extras = let
225        val th1' = munge extras pfx1 sfx1 th1
226        val th2' = munge extras pfx2 sfx2 th2
227      in
228        EXISTS_TAC (rand (concl th1')) THEN
229        REWRITE_TAC [GSYM APPEND_ASSOC, APPEND] THEN
230        ACCEPT_TAC (CONJ th1' th2')
231      end
232    in
233      if null nonnil_asms andalso listSyntax.is_nil res1 andalso
234         listSyntax.is_nil res2 andalso List.all is_var pfx1 andalso
235         List.all is_var sfx1
236      then let
237          val eqn = mk_eq(last (pfx1 @ sfx1), alphanil_t)
238        in
239          ASM_CASES_TAC eqn THENL [
240            BasicProvers.VAR_EQ_TAC THEN REWRITE_TAC [APPEND_NIL] THEN
241            solver,
242            conclude [ASSUME (mk_neg eqn)]
243          ]
244        end
245      else conclude []
246    end
247  else let
248      val (_, [_, x, _]) = strip_comb body
249    in
250      EXISTS_TAC x THEN MATCH_ACCEPT_TAC relationTheory.RTC_REFL
251    end
252end (asl,t) handle Empty => raise mk_HOL_ERR "wardScript" "solver" "Empty list"
253(*
254val thmrwt_weak_confluent = store_thm(
255  "thmrwt_weak_confluent",
256  ``���x y. thmrwt x y ��� ���z. thmrwt x z ��� ���u. thmrwt^* y u ��� thmrwt^* z u``,
257  Induct_on `thmrwt` >> rpt conj_tac >-
258    (rpt gen_tac >> strip_tac >> gen_tac >>
259     srw_tac [][SimpL ``(==>)``, Once thmrwt_cases] >>
260     fsrw_tac [][listTheory.APPEND_EQ_APPEND_MID,
261                 listTheory.APPEND_EQ_SING,
262                 listTheory.APPEND_eq_NIL,
263                 listTheory.APPEND_EQ_CONS] >>
264     srw_tac [][] >>
265     fsrw_tac [][listTheory.APPEND_EQ_SING,
266                 listTheory.APPEND_eq_NIL] >>
267     solver)
268   >- (rpt gen_tac >> srw_tac [][SimpL ``(==>)``, Once thmrwt_cases] >>
269       fsrw_tac [][APPEND_EQ_APPEND_MID, APPEND_EQ_SING, APPEND_EQ_CONS] THEN
270       srw_tac [][] >> fsrw_tac [][] >> TRY  solver >>
271       fsrw_tac [][APPEND_EQ_APPEND, APPEND_EQ_CONS] >> srw_tac [][] >>
272       fsrw_tac [][APPEND_EQ_CONS] >> TRY solver
273
274     TRY (metis_tac [relationTheory.RTC_SUBSET, relationTheory.RTC_REFL,
275                     listTheory.APPEND_ASSOC, thmrwt_rules,
276                     listTheory.APPEND_eq_NIL]) >>
277     solver
278     >| [
279       qexists_tac `x' ++ [b;b;a;a] ++ z ++ y` >>
280       conj_tac >| [
281         metis_tac [relationTheory.RTC_SUBSET, listTheory.APPEND_ASSOC,
282                    thmrwt_rules],
283         srw_tac [][relationTheory.RTC_SUBSET, thmrwt_rules]
284       ],
285       qexists_tac `x ++ z' ++ [b;b;a;a] ++ y'` >>
286       conj_tac >- srw_tac [][thmrwt_rules, relationTheory.RTC_SUBSET] >>
287       match_mp_tac relationTheory.RTC_SUBSET >>
288       `x ++ [I] ++ z' ++ [b;b;a;a] ++ y' = x ++ [I] ++ (z' ++ [b;b;a;a] ++ y')`
289          by srw_tac [][] >>
290       pop_assum SUBST1_TAC >>
291       `x ++ z' ++ [b;b;a;a] ++ y' = x ++ (z' ++ [b;b;a;a] ++ y')`
292          by srw_tac [][] >>
293       pop_assum SUBST1_TAC >>
294       match_mp_tac (hd (CONJUNCTS thmrwt_rules)) >> srw_tac [][],
295       pop_assum (MP_TAC o AP_TERM ``MEM I``) >> srw_tac [][],
296*)
297val _ = export_theory()
298