doc-src/ZF/IFOL_examples.thy
changeset 14152 12f6f18e7afc
child 16417 9bc16273c2d4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/ZF/IFOL_examples.thy	Tue Aug 19 13:53:58 2003 +0200
     1.3 @@ -0,0 +1,58 @@
     1.4 +header{*Examples of Intuitionistic Reasoning*}
     1.5 +
     1.6 +theory IFOL_examples = IFOL:
     1.7 +
     1.8 +text{*Quantifier example from the book Logic and Computation*}
     1.9 +lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    1.10 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.11 +apply (rule impI)
    1.12 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.13 +apply (rule allI)
    1.14 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.15 +apply (rule exI)
    1.16 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.17 +apply (erule exE)
    1.18 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.19 +apply (erule allE)
    1.20 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.21 +txt{*Now @{text "apply assumption"} fails*}
    1.22 +oops
    1.23 +
    1.24 +text{*Trying again, with the same first two steps*}
    1.25 +lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    1.26 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.27 +apply (rule impI)
    1.28 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.29 +apply (rule allI)
    1.30 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.31 +apply (erule exE)
    1.32 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.33 +apply (rule exI)
    1.34 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.35 +apply (erule allE)
    1.36 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.37 +apply assumption
    1.38 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.39 +done
    1.40 +
    1.41 +lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    1.42 +by (tactic {*IntPr.fast_tac 1*})
    1.43 +
    1.44 +text{*Example of Dyckhoff's method*}
    1.45 +lemma "~ ~ ((P-->Q) | (Q-->P))"
    1.46 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.47 +apply (unfold not_def)
    1.48 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.49 +apply (rule impI)
    1.50 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.51 +apply (erule disj_impE)
    1.52 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.53 +apply (erule imp_impE)
    1.54 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.55 + apply (erule imp_impE)
    1.56 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.57 +apply assumption 
    1.58 +apply (erule FalseE)+
    1.59 +done
    1.60 +
    1.61 +end