src/FOLP/ex/If.thy
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 25991 31b38a39e589
child 35416 d8d7d1b785af
permissions -rw-r--r--
renamed structure Display_Goal to Goal_Display;
     1 (* $Id$ *)
     2 
     3 theory If
     4 imports FOLP
     5 begin
     6 
     7 constdefs
     8   "if" :: "[o,o,o]=>o"
     9   "if(P,Q,R) == P&Q | ~P&R"
    10 
    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
    45 
    46 end