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