src/Doc/ZF/IFOL_examples.thy
 author wenzelm Sat, 05 Apr 2014 15:03:40 +0200 changeset 56421 1ffd7eaa778b parent 51798 ad3a241def73 permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
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` 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 ```