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