1structure ntermLib :> ntermLib =
2struct
3
4open HolKernel boolLib Parse bossLib nomsetTheory ntermTheory simpLib
5
6val user_frag = ref (SSFRAG {dprocs = [], ac = [], rewrs = [],
7                             congs = [], filter = NONE,
8                             name = SOME "permsimps", convs = []})
9
10val user_weakenings = ref ([] : thm list)
11fun add_rwts ths =
12    user_frag := merge_ss [!user_frag, rewrites ths]
13fun add_weakenings ths = user_weakenings := !user_weakenings @ ths
14
15fun congfrag ths = SSFRAG {dprocs = [], ac = [], rewrs = [],
16                           congs = ths, filter = NONE,
17                           name = NONE, convs = []}
18
19fun add_congs ths =
20    user_frag := merge_ss [!user_frag, congfrag ths]
21
22val permeq_sym' = prove(``x == y <=> y == x``, METIS_TAC [permeq_sym])
23
24fun permify ss = simpLib.add_relsimp
25               {trans = permeq_trans,
26                refl = GEN_ALL permeq_refl,
27                weakenings = Sus_eq_perms :: pmact_permeq ::
28                             !user_weakenings,
29                subsets = [],
30                rewrs = [SELECT_permeq_REFL, permof_inverse,
31                         permof_inverse_append,
32                         CONV_RULE (LAND_CONV (ONCE_REWRITE_CONV [permeq_sym']))
33                                   SELECT_permeq_REFL]} ss ++
34           congfrag [permof_REVERSE_monotone,
35                     app_permeq_monotone
36                         |>SPEC_ALL
37                         |>REWRITE_RULE [GSYM AND_IMP_INTRO]] ++
38           !user_frag
39
40val psrw_ss = permify o srw_ss
41
42open LoadableThyData ThmSetData
43
44val {export=export_permrwt,...} =
45    new_exporter "permrwts" (K (add_rwts o map #2))
46val {export=export_permcong,...} =
47    new_exporter "permcongs" (K (add_congs o map #2))
48val {export=export_permweakening,...} =
49   new_exporter "permweakenings" (K (add_weakenings o map #2))
50
51end (* struct *)
52