equal
deleted
inserted
replaced
15 val setup: theory -> theory |
15 val setup: theory -> theory |
16 end |
16 end |
17 |
17 |
18 structure NominalPackage : NOMINAL_PACKAGE = |
18 structure NominalPackage : NOMINAL_PACKAGE = |
19 struct |
19 struct |
|
20 |
|
21 val Finites_emptyI = thm "Finites.emptyI"; |
|
22 val finite_Diff = thm "finite_Diff"; |
|
23 val finite_Un = thm "finite_Un"; |
|
24 val Un_iff = thm "Un_iff"; |
|
25 val In0_eq = thm "In0_eq"; |
|
26 val In1_eq = thm "In1_eq"; |
|
27 val In0_not_In1 = thm "In0_not_In1"; |
|
28 val In1_not_In0 = thm "In1_not_In0"; |
|
29 val Un_assoc = thm "Un_assoc"; |
|
30 val Collect_disj_eq = thm "Collect_disj_eq"; |
|
31 val empty_def = thm "empty_def"; |
20 |
32 |
21 open DatatypeAux; |
33 open DatatypeAux; |
22 open NominalAtoms; |
34 open NominalAtoms; |
23 |
35 |
24 (** FIXME: DatatypePackage should export this function **) |
36 (** FIXME: DatatypePackage should export this function **) |
1002 if null dts then Const ("{}", HOLogic.mk_setT atomT) |
1014 if null dts then Const ("{}", HOLogic.mk_setT atomT) |
1003 else foldr1 (HOLogic.mk_binop "op Un") (map supp args2)))) |
1015 else foldr1 (HOLogic.mk_binop "op Un") (map supp args2)))) |
1004 (fn _ => |
1016 (fn _ => |
1005 simp_tac (HOL_basic_ss addsimps (supp_def :: |
1017 simp_tac (HOL_basic_ss addsimps (supp_def :: |
1006 Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un :: |
1018 Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un :: |
1007 symmetric empty_def :: Finites.emptyI :: simp_thms @ |
1019 symmetric empty_def :: Finites_emptyI :: simp_thms @ |
1008 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1) |
1020 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1) |
1009 in |
1021 in |
1010 (supp_thm, |
1022 (supp_thm, |
1011 Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq |
1023 Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq |
1012 (fresh c, |
1024 (fresh c, |