17480

1 
(* $Id$ *)


2 


3 
theory If


4 
imports FOLP


5 
begin


6 


7 
constdefs

19796

8 
"if" :: "[o,o,o]=>o"

17480

9 
"if(P,Q,R) == P&Q  ~P&R"


10 

25991

11 
lemma ifI:


12 
assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R"


13 
shows "?p : if(P,Q,R)"


14 
apply (unfold if_def)


15 
apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})


16 
done


17 


18 
lemma ifE:


19 
assumes 1: "p : if(P,Q,R)" and


20 
2: "!!x y. [ x : P; y : Q ] ==> f(x, y) : S" and


21 
3: "!!x y. [ x : ~P; y : R ] ==> g(x, y) : S"


22 
shows "?p : S"


23 
apply (insert 1)


24 
apply (unfold if_def)


25 
apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})


26 
done


27 


28 
lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))"


29 
apply (rule iffI)


30 
apply (erule ifE)


31 
apply (erule ifE)


32 
apply (rule ifI)


33 
apply (rule ifI)


34 
oops


35 


36 
ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}


37 


38 
lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))"


39 
apply (tactic {* fast_tac if_cs 1 *})


40 
done


41 


42 
lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,A,B))"


43 
apply (tactic {* fast_tac if_cs 1 *})


44 
done

17480

45 

0

46 
end
