equal
deleted
inserted
replaced
292 Const _ $ (Const ("Intensional.Valid", _) $ _) => |
292 Const _ $ (Const ("Intensional.Valid", _) $ _) => |
293 (flatten (int_unlift th) handle THM _ => th) |
293 (flatten (int_unlift th) handle THM _ => th) |
294 | _ => th |
294 | _ => th |
295 *} |
295 *} |
296 |
296 |
297 setup {* |
297 attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} "" |
298 Attrib.add_attributes [ |
298 attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} "" |
299 ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""), |
299 attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} "" |
300 ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""), |
300 attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} "" |
301 ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""), |
|
302 ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")] |
|
303 *} |
|
304 |
301 |
305 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)" |
302 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)" |
306 by (simp add: Valid_def) |
303 by (simp add: Valid_def) |
307 |
304 |
308 lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)" |
305 lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)" |