1open HolKernel Parse BasicProvers simpLib Datatype
2
3val _ = new_theory "recordEnumSimpsB"
4
5local open recordEnumSimpsLib recordEnumSimpsATheory in end;
6
7val enum_lemma1 = Q.store_thm("enum_lemma1",
8  ���C2 <> C3���,
9  simp_tac (srw_ss()) []);
10
11val enum_lemma2 = Q.store_thm("enum_lemma2",
12  ���D10 <> D11���,
13  simp_tac (srw_ss()) []);
14
15val recd_lemma1 = Q.store_thm("recd_lemma1",
16  ���(r with fld1 := 3).fld1 = 3���,
17  simp_tac (srw_ss()) []);
18
19val recd_lemma2 = Q.store_thm("recd_lemma2",
20  ���(r with fld1 := 3).fld2 = r.fld2���,
21  simp_tac (srw_ss()) []);
22
23val normal_lemma = Q.store_thm("normal_lemma",
24  ���E1 n <> E3���,
25  computeLib.EVAL_TAC);
26
27Theorem fields_of_test:
28  ^(#accessor (Lib.assoc "fld2" (TypeBase.fields_of ���:'a Record���)))
29    <| fld1 := 3; fld2 := K 3 : 'a -> num |>
30=
31  K 3
32Proof
33  simp_tac (srw_ss()) []
34QED
35
36val _ = export_theory();
37