src/Doc/Logics_ZF/FOL_examples.thy
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (23 months ago) changeset 66816 212a3334e7da parent 66453 cc19f7ca2ed6 child 67406 23307fd33906 permissions -rw-r--r--
more fundamental definition of div and mod on int
```     1 section{*Examples of Classical Reasoning*}
```
```     2
```
```     3 theory FOL_examples imports FOL begin
```
```     4
```
```     5 lemma "EX y. ALL x. P(y)-->P(x)"
```
```     6   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```     7 apply (rule exCI)
```
```     8   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```     9 apply (rule allI)
```
```    10   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```    11 apply (rule impI)
```
```    12   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```    13 apply (erule allE)
```
```    14   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```    15 txt{*see below for @{text allI} combined with @{text swap}*}
```
```    16 apply (erule allI [THEN [2] swap])
```
```    17   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```    18 apply (rule impI)
```
```    19   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```    20 apply (erule notE)
```
```    21   --{* @{subgoals[display,indent=0,margin=65]} *}
```
```    22 apply assumption
```
```    23 done
```
```    24
```
```    25 text {*
```
```    26 @{thm[display] allI [THEN [2] swap]}
```
```    27 *}
```
```    28
```
```    29 lemma "EX y. ALL x. P(y)-->P(x)"
```
```    30 by blast
```
```    31
```
```    32 end
```
```    33
```
```    34
```