1structure pairSimps :> pairSimps =
2struct
3
4open Lib Parse simpLib pairTheory PairedLambda;
5
6
7val PAIR_ss = BasicProvers.thy_ssfrag "pair"
8
9val fvar = ``f:'a -> 'b -> bool``;
10val paired_forall_ss =
11    conv_ss
12      {name  = "ELIM_TUPLED_QUANT_CONV (remove paired quantification)",
13       trace = 2,
14       key   = SOME ([],``$! (UNCURRY ^fvar)``),
15       conv  = K (K pairTools.ELIM_TUPLED_QUANT_CONV)}
16
17val paired_exists_ss =
18    conv_ss
19      {name  = "ELIM_TUPLED_QUANT_CONV (remove paired quantification)",
20       trace = 2,
21       key   = SOME ([],``$? (UNCURRY ^fvar)``),
22       conv  = K (K pairTools.ELIM_TUPLED_QUANT_CONV)}
23
24val gen_beta_ss =
25    conv_ss
26      {name  = "GEN_BETA_CONV",
27       trace = 2,
28       key   = SOME ([],``(UNCURRY ^fvar) x``),
29       conv  = K (K PairedLambda.GEN_BETA_CONV)}
30
31
32
33end (* struct *)
34