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