1open HolKernel Parse BasicProvers simpLib Datatype 2 3open recordEnumSimpsLib 4 5val _ = new_theory "recordEnumSimpsA" 6 7val _ = Datatype���Enum1 = C1 | C2 | C3���; 8val _ = Datatype���Enum2 = D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 9 | D11 | D12 | D13 | D14 | D15 | D16 10 ���; 11 12val _ = Datatype���Normal = E1 num | E2 bool | E3���; 13 14val _ = Datatype���Record = <| fld1 : num ; fld2 : 'a -> num |>���; 15 16val enum_lemma1 = Q.store_thm("enum_lemma1", 17 ���C1 <> C2���, 18 simp_tac (srw_ss()) []); 19 20val enum_lemma2 = Q.store_thm("enum_lemma2", 21 ���D1 <> D2���, 22 simp_tac (srw_ss()) []); 23 24val recd_lemma1 = Q.store_thm("recd_lemma1", 25 ���(r with fld1 := 3).fld1 = 3���, 26 simp_tac (srw_ss()) []); 27 28val recd_lemma2 = Q.store_thm("recd_lemma2", 29 ���(r with fld1 := 3).fld2 = r.fld2���, 30 simp_tac (srw_ss()) []); 31 32val normal_lemma = Q.store_thm("normal_lemma", 33 ���E1 n <> E3���, 34 computeLib.EVAL_TAC); 35 36val _ = export_theory(); 37