doc-src/ZF/FOL_examples.thy
 changeset 14152 12f6f18e7afc child 16417 9bc16273c2d4
equal inserted replaced
14151:b8bb6a6a2c46 14152:12f6f18e7afc
`       `
`     1 header{*Examples of Classical Reasoning*}`
`       `
`     2 `
`       `
`     3 theory FOL_examples = FOL:`
`       `
`     4 `
`       `
`     5 lemma "EX y. ALL x. P(y)-->P(x)"`
`       `
`     6   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`     7 apply (rule exCI)`
`       `
`     8   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`     9 apply (rule allI)`
`       `
`    10   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    11 apply (rule impI)`
`       `
`    12   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    13 apply (erule allE)`
`       `
`    14   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    15 txt{*see below for @{text allI} combined with @{text swap}*}`
`       `
`    16 apply (erule allI [THEN [2] swap])`
`       `
`    17   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    18 apply (rule impI)`
`       `
`    19   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    20 apply (erule notE)`
`       `
`    21   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    22 apply assumption`
`       `
`    23 done`
`       `
`    24 `
`       `
`    25 text {*`
`       `
`    26 @{thm[display] allI [THEN [2] swap]}`
`       `
`    27 *}`
`       `
`    28 `
`       `
`    29 lemma "EX y. ALL x. P(y)-->P(x)"`
`       `
`    30 by blast`
`       `
`    31 `
`       `
`    32 end`
`       `
`    33 `
`       `
`    34 `