src/Doc/Logics_ZF/IFOL_examples.thy
author haftmann
Mon, 06 Feb 2017 20:56:34 +0100
changeset 64990 c6a7de505796
parent 58889 5b7a9633cfa8
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
more explicit errors in pathological cases
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 56451
diff changeset
     1
section{*Examples of Intuitionistic Reasoning*}
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     2
48510
8f3069015441 proper imports;
wenzelm
parents: 16417
diff changeset
     3
theory IFOL_examples imports "~~/src/FOL/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))"
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 48985
diff changeset
    39
by (tactic {*IntPr.fast_tac @{context} 1*})
14152
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