author  paulson 
Thu, 14 Jun 2018 14:23:48 +0100  
changeset 68446  92ddca1edc43 
parent 61337  4645502c3c64 
child 69593  3dda49e08b9d 
permissions  rwrr 
17480  1 
theory If 
2 
imports FOLP 

3 
begin 

4 

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

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

61337  8 
schematic_goal ifI: 
25991  9 
assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R" 
10 
shows "?p : if(P,Q,R)" 

11 
apply (unfold if_def) 

60770  12 
apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1\<close>) 
25991  13 
done 
14 

61337  15 
schematic_goal ifE: 
25991  16 
assumes 1: "p : if(P,Q,R)" and 
17 
2: "!!x y. [ x : P; y : Q ] ==> f(x, y) : S" and 

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

19 
shows "?p : S" 

20 
apply (insert 1) 

21 
apply (unfold if_def) 

60770  22 
apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\<close>) 
25991  23 
done 
24 

61337  25 
schematic_goal if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))" 
25991  26 
apply (rule iffI) 
27 
apply (erule ifE) 

28 
apply (erule ifE) 

29 
apply (rule ifI) 

30 
apply (rule ifI) 

31 
oops 

32 

60770  33 
ML \<open>val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}]\<close> 
25991  34 

61337  35 
schematic_goal if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))" 
60770  36 
apply (tactic \<open>fast_tac @{context} if_cs 1\<close>) 
25991  37 
done 
38 

61337  39 
schematic_goal nested_ifs: "?p : if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,A,B))" 
60770  40 
apply (tactic \<open>fast_tac @{context} if_cs 1\<close>) 
25991  41 
done 
17480  42 

0  43 
end 