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--
```     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
```