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