doc-src/ZF/IFOL_examples.thy
 changeset 14152 12f6f18e7afc child 16417 9bc16273c2d4
equal inserted replaced
14151:b8bb6a6a2c46 14152:12f6f18e7afc
`       `
`     1 header{*Examples of Intuitionistic Reasoning*}`
`       `
`     2 `
`       `
`     3 theory IFOL_examples = IFOL:`
`       `
`     4 `
`       `
`     5 text{*Quantifier example from the book Logic and Computation*}`
`       `
`     6 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"`
`       `
`     7   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`     8 apply (rule impI)`
`       `
`     9   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    10 apply (rule allI)`
`       `
`    11   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    12 apply (rule exI)`
`       `
`    13   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    14 apply (erule exE)`
`       `
`    15   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    16 apply (erule allE)`
`       `
`    17   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    18 txt{*Now @{text "apply assumption"} fails*}`
`       `
`    19 oops`
`       `
`    20 `
`       `
`    21 text{*Trying again, with the same first two steps*}`
`       `
`    22 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"`
`       `
`    23   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    24 apply (rule impI)`
`       `
`    25   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    26 apply (rule allI)`
`       `
`    27   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    28 apply (erule exE)`
`       `
`    29   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    30 apply (rule exI)`
`       `
`    31   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    32 apply (erule allE)`
`       `
`    33   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    34 apply assumption`
`       `
`    35   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    36 done`
`       `
`    37 `
`       `
`    38 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"`
`       `
`    39 by (tactic {*IntPr.fast_tac 1*})`
`       `
`    40 `
`       `
`    41 text{*Example of Dyckhoff's method*}`
`       `
`    42 lemma "~ ~ ((P-->Q) | (Q-->P))"`
`       `
`    43   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    44 apply (unfold not_def)`
`       `
`    45   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    46 apply (rule impI)`
`       `
`    47   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    48 apply (erule disj_impE)`
`       `
`    49   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    50 apply (erule imp_impE)`
`       `
`    51   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    52  apply (erule imp_impE)`
`       `
`    53   --{* @{subgoals[display,indent=0,margin=65]} *}`
`       `
`    54 apply assumption `
`       `
`    55 apply (erule FalseE)+`
`       `
`    56 done`
`       `
`    57 `
`       `
`    58 end`