wenzelm@58889: section{*Examples of Classical Reasoning*} paulson@14152: wenzelm@66453: theory FOL_examples imports FOL begin paulson@14152: paulson@14152: lemma "EX y. ALL x. P(y)-->P(x)" paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: apply (rule exCI) paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: apply (rule allI) paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: apply (rule impI) paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: apply (erule allE) paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: txt{*see below for @{text allI} combined with @{text swap}*} paulson@14152: apply (erule allI [THEN [2] swap]) paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: apply (rule impI) paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: apply (erule notE) paulson@14152: --{* @{subgoals[display,indent=0,margin=65]} *} paulson@14152: apply assumption paulson@14152: done paulson@14152: paulson@14152: text {* paulson@14152: @{thm[display] allI [THEN [2] swap]} paulson@14152: *} paulson@14152: paulson@14152: lemma "EX y. ALL x. P(y)-->P(x)" paulson@14152: by blast paulson@14152: paulson@14152: end paulson@14152: paulson@14152: