1open HolKernel boolLib bossLib lcsymtacs
2     listTheory rich_listTheory arithmeticTheory
3
4val _ = new_theory"balancedParens"
5
6val _ = Datatype`alpha = a | b`; (* a = "(", b = ")"  *)
7
8fun met h = metis_tac([APPEND,APPEND_ASSOC]@h)
9
10val (S_rules,S_ind,S_cases) = Hol_reln`
11  S [] ���
12  (S w ��� S ([a] ++ w ++ [b])) ���
13  (S w1 ��� S w2 ��� S (w1++w2))`
14
15val Snil = Q.store_thm("Snil[simp]",
16  `S []`, rw[Once S_cases]);
17
18val (T_rules,T_ind,T_cases) = Hol_reln`
19  T [] ���
20  (T w1 ��� T w2 ��� T (w1 ++ [a] ++ w2 ++ [b]))`
21
22val TS = Q.store_thm("TS",
23  `���w. T w ��� S w`,
24  Induct_on`T` >> met[S_rules])
25
26val Tnil = Q.store_thm("Tnil[simp]",
27  `T []`, rw[Once T_cases])
28
29val Tapp = Q.store_thm("Tapp",
30  `���w2. T w2 ��� ���w1. T w1 ��� T (w1 ++ w2)`,
31  Induct_on`T` >> simp[T_rules])
32
33val ST = Q.store_thm("ST",
34  `���w. S w ��� T w`,
35  Induct_on`S` >> met[T_rules,Tapp])
36
37val T_iff_S = Q.store_thm("T_iff_S",
38  `T w ��� S w`, metis_tac[TS,ST]);
39
40val balanced_def = Define`
41  (balanced [] 0 ��� T) ���
42  (balanced (a::xs) n ��� balanced xs (SUC n)) ���
43  (balanced (b::xs) (SUC n) ��� balanced xs n) ���
44  (balanced _ _ ��� F)`
45val _ = export_rewrites["balanced_def"]
46val balanced_ind = theorem"balanced_ind"
47
48val balanced_append = Q.store_thm("balanced_append",
49  `���w1 n1. balanced w1 n1 ��� ���w2 n2. balanced w2 n2 ��� balanced (w1++w2) (n1+n2)`,
50  ho_match_mp_tac balanced_ind >>
51  rw[] >> fs[] >- (
52    res_tac >> fsrw_tac[ARITH_ss][ADD1] ) >>
53  REWRITE_TAC[ADD_CLAUSES] >>
54  simp[])
55
56val S_balanced = Q.store_thm("S_balanced",
57  `���w. S w ��� balanced w 0`,
58  Induct_on`S` >>
59  simp[] >> conj_tac >- (
60    SUBST1_TAC(DECIDE``1 = 0+1``) >>
61    rpt strip_tac >> irule balanced_append >>
62    REWRITE_TAC[ONE] >> simp[] ) >>
63  metis_tac[balanced_append,DECIDE``0+0=0``])
64
65val Sins = Q.store_thm("Sins",
66  `���w. S w ��� ���w1 w2. (w = w1 ++ w2) ��� S(w1++[a;b]++w2)`,
67  Induct_on`S`>>
68  rw[APPEND_EQ_APPEND,APPEND_EQ_CONS] >> fs[] >>
69  met[S_rules])
70
71val balanced_S = Q.store_thm("balanced_S",
72  `���w n. balanced w n ��� S (REPLICATE n a ++ w)`,
73  ho_match_mp_tac balanced_ind >>
74  asm_simp_tac std_ss [REPLICATE_GENLIST] >> rw[] >> fs[]
75  >- (fs[GENLIST,SNOC_APPEND] >> met[]) >>
76  imp_res_tac Sins >>
77  first_x_assum(qspec_then`w`mp_tac) >> simp[] >>
78  simp[GENLIST,SNOC_APPEND] >> met[])
79
80val balanced_iff_S = Q.store_thm("balanced_iff_S",
81  `balanced w 0 ��� S w`,
82  metis_tac[balanced_S,S_balanced,REPLICATE,APPEND])
83
84val _ = export_theory()
85