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