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