doc-src/ZF/IFOL_examples.thy
author wenzelm
Thu, 15 May 2008 20:14:10 +0200
changeset 26913 67040326ab7a
parent 16417 9bc16273c2d4
child 48510 8f3069015441
permissions -rw-r--r--
use Isabelle sty files from Doc/;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     1
header{*Examples of Intuitionistic Reasoning*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     2
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14152
diff changeset
     3
theory IFOL_examples imports IFOL begin
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     4
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     5
text{*Quantifier example from the book Logic and Computation*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     6
lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     7
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     8
apply (rule impI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     9
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    10
apply (rule allI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    11
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    12
apply (rule exI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    13
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    14
apply (erule exE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    15
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    16
apply (erule allE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    17
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    18
txt{*Now @{text "apply assumption"} fails*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    19
oops
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    20
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    21
text{*Trying again, with the same first two steps*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    22
lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    23
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    24
apply (rule impI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    25
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    26
apply (rule allI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    27
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    28
apply (erule exE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    29
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    30
apply (rule exI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    31
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    32
apply (erule allE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    33
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    34
apply assumption
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    35
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    36
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    37
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    38
lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    39
by (tactic {*IntPr.fast_tac 1*})
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    40
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    41
text{*Example of Dyckhoff's method*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    42
lemma "~ ~ ((P-->Q) | (Q-->P))"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    43
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    44
apply (unfold not_def)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    45
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    46
apply (rule impI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    47
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    48
apply (erule disj_impE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    49
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    50
apply (erule imp_impE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    51
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    52
 apply (erule imp_impE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    53
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    54
apply assumption 
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    55
apply (erule FalseE)+
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    56
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    57
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    58
end