paulson@14152: header{*Examples of Intuitionistic Reasoning*}
paulson@14152: 
haftmann@16417: theory IFOL_examples imports IFOL begin
paulson@14152: 
paulson@14152: text{*Quantifier example from the book Logic and Computation*}
paulson@14152: lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule impI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule allI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule exI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule exE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule allE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: txt{*Now @{text "apply assumption"} fails*}
paulson@14152: oops
paulson@14152: 
paulson@14152: text{*Trying again, with the same first two steps*}
paulson@14152: lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule impI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule allI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule exE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule exI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule allE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply assumption
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: done
paulson@14152: 
paulson@14152: lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
paulson@14152: by (tactic {*IntPr.fast_tac 1*})
paulson@14152: 
paulson@14152: text{*Example of Dyckhoff's method*}
paulson@14152: lemma "~ ~ ((P-->Q) | (Q-->P))"
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (unfold not_def)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (rule impI)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule disj_impE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply (erule imp_impE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152:  apply (erule imp_impE)
paulson@14152:   --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152: apply assumption 
paulson@14152: apply (erule FalseE)+
paulson@14152: done
paulson@14152: 
paulson@14152: end