header{*Examples of Intuitionistic Reasoning*}

 theory IFOL_examples imports IFOL begin

 text{*Quantifier example from the book Logic and Computation*}

 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule impI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule allI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule exI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule exE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule allE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 txt{*Now @{text "apply assumption"} fails*}

 oops

 text{*Trying again, with the same first two steps*}

 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule impI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule allI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule exE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule exI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule allE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply assumption

   --{* @{subgoals[display,indent=0,margin=65]} *}

 done

 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"

 by (tactic {*IntPr.fast_tac 1*})

 text{*Example of Dyckhoff's method*}

 lemma "~ ~ ((P-->Q) | (Q-->P))"

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (unfold not_def)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule impI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule disj_impE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule imp_impE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

  apply (erule imp_impE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply assumption 

 apply (erule FalseE)+

 done

 end