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