1structure brackabs :> brackabs = 2struct 3 4open HolKernel boolLib simpLib 5 6structure Parse = struct 7 open Parse 8 val (Type,Term) = parse_from_grammars brackabsTheory.brackabs_grammars 9end 10open Parse 11 12open brackabsTheory reductionEval 13 14 15val eqn_elim = prove( 16 ``(!Y. (X:term == Y) = (Z == Y)) ==> X == Z``, 17 STRIP_TAC THEN POP_ASSUM (Q.SPEC_THEN `Z` MP_TAC) THEN 18 REWRITE_TAC [chap2Theory.lameq_refl]); 19fun brackabs_equiv ths def = let 20 val lameq_t = ``chap2$==`` 21 val th = if is_eq (concl def) then let 22 val (l,r) = dest_eq (concl def) 23 in 24 EQ_MP (AP_TERM (mk_comb(lameq_t, l)) def) 25 (SPEC l (GEN_ALL chap2Theory.lameq_refl)) 26 end 27 else def 28 val list1 = [S_I, K_I, B_I, C_I, fake_eta, B_eta, I_I] 29in 30 th |> SIMP_RULE (bsrw_ss()) (list1 @ ths) 31 |> SIMP_RULE (bsrw_ss()) (B_I_uncond :: list1 @ ths) 32end 33 34 35end (* struct *) 36