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