author  haftmann 
Mon, 01 Mar 2010 13:40:23 +0100  
changeset 35416  d8d7d1b785af 
parent 25991  31b38a39e589 
child 35762  af3ff2ba4c54 
permissions  rwrr 
17480  1 
(* $Id$ *) 
2 

3 
theory If 

4 
imports FOLP 

5 
begin 

6 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
25991
diff
changeset

7 
definition "if" :: "[o,o,o]=>o" where 
17480  8 
"if(P,Q,R) == P&Q  ~P&R" 
9 

25991  10 
lemma ifI: 
11 
assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R" 

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

13 
apply (unfold if_def) 

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

15 
done 

16 

17 
lemma ifE: 

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

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

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

21 
shows "?p : S" 

22 
apply (insert 1) 

23 
apply (unfold if_def) 

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

25 
done 

26 

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

28 
apply (rule iffI) 

29 
apply (erule ifE) 

30 
apply (erule ifE) 

31 
apply (rule ifI) 

32 
apply (rule ifI) 

33 
oops 

34 

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

36 

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

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

39 
done 

40 

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

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

43 
done 

17480  44 

0  45 
end 