doc-src/ZF/IFOL_examples.thy
author haftmann
Tue Oct 10 13:59:12 2006 +0200 (2006-10-10)
changeset 20950 981fa0ce23ed
parent 16417 9bc16273c2d4
child 48510 8f3069015441
permissions -rw-r--r--
added IsarAdvanced material
     1 header{*Examples of Intuitionistic Reasoning*}
     2 
     3 theory IFOL_examples imports IFOL begin
     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