equal
deleted
inserted
replaced
115 in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end |
115 in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end |
116 else NONE) |
116 else NONE) |
117 | _ => NONE |
117 | _ => NONE |
118 end |
118 end |
119 |
119 |
120 val perm_simproc_app = Simplifier.simproc (the_context ()) "perm_simproc_app" |
120 val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app" |
121 ["Nominal.perm pi x"] perm_simproc_app'; |
121 ["Nominal.perm pi x"] perm_simproc_app'; |
122 |
122 |
123 (* a simproc that deals with permutation instances in front of functions *) |
123 (* a simproc that deals with permutation instances in front of functions *) |
124 fun perm_simproc_fun' sg ss redex = |
124 fun perm_simproc_fun' sg ss redex = |
125 let |
125 let |
135 (Const("Nominal.perm",_) $ pi $ f) => |
135 (Const("Nominal.perm",_) $ pi $ f) => |
136 (if (applicable_fun f) then SOME (perm_fun_def) else NONE) |
136 (if (applicable_fun f) then SOME (perm_fun_def) else NONE) |
137 | _ => NONE |
137 | _ => NONE |
138 end |
138 end |
139 |
139 |
140 val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun" |
140 val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun" |
141 ["Nominal.perm pi x"] perm_simproc_fun'; |
141 ["Nominal.perm pi x"] perm_simproc_fun'; |
142 |
142 |
143 (* function for simplyfying permutations *) |
143 (* function for simplyfying permutations *) |
144 (* stac contains the simplifiation tactic that is *) |
144 (* stac contains the simplifiation tactic that is *) |
145 (* applied (see (no_asm) options below *) |
145 (* applied (see (no_asm) options below *) |
215 cp1_aux))) |
215 cp1_aux))) |
216 else NONE |
216 else NONE |
217 end |
217 end |
218 | _ => NONE); |
218 | _ => NONE); |
219 |
219 |
220 val perm_compose_simproc = Simplifier.simproc (the_context ()) "perm_compose" |
220 val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose" |
221 ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc'; |
221 ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc'; |
222 |
222 |
223 fun perm_compose_tac ss i = |
223 fun perm_compose_tac ss i = |
224 ("analysing permutation compositions on the lhs", |
224 ("analysing permutation compositions on the lhs", |
225 fn st => EVERY |
225 fn st => EVERY |