1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "hfb";
4
5val _ = Datatype`hfb0 = HF_E | HF_I hfb0 hfb0`
6
7val (hfb0_equiv_rules, hfb0_equiv_ind, hfb0_equiv_cases) = Hol_reln`
8  hfb0_equiv HF_E HF_E ���
9  (���x y b. hfb0_equiv (HF_I x (HF_I y b)) (HF_I y (HF_I x b))) ���
10  (���x1 x2 b1 b2.
11    hfb0_equiv x1 x2 ��� hfb0_equiv b1 b2 ���
12    hfb0_equiv (HF_I x1 b1) (HF_I x2 b2)) ���
13  (���h1 h2 h3. hfb0_equiv h1 h2 ��� hfb0_equiv h2 h3 ��� hfb0_equiv h1 h3)
14`;
15
16val hfb0_refl = Q.store_thm(
17  "hfb0_refl",
18  `���h. hfb0_equiv h h`,
19  Induct >> simp[hfb0_equiv_rules]);
20
21val hfb0_sym = Q.store_thm(
22  "hfb0_sym",
23  `���h1 h2. hfb0_equiv h1 h2 ��� hfb0_equiv h2 h1`,
24  Induct_on `hfb0_equiv` >> metis_tac[hfb0_equiv_rules]);
25
26val hfb0_trans = save_thm(
27  "hfb0_trans",
28  last (CONJUNCTS hfb0_equiv_rules))
29
30
31
32val _ = export_theory();
33