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;
wenzelm@17480
     1
(* $Id$ *)
wenzelm@17480
     2
wenzelm@17480
     3
theory If
wenzelm@17480
     4
imports FOLP
wenzelm@17480
     5
begin
wenzelm@17480
     6
wenzelm@17480
     7
constdefs
wenzelm@19796
     8
  "if" :: "[o,o,o]=>o"
wenzelm@17480
     9
  "if(P,Q,R) == P&Q | ~P&R"
wenzelm@17480
    10
wenzelm@25991
    11
lemma ifI:
wenzelm@25991
    12
  assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
wenzelm@25991
    13
  shows "?p : if(P,Q,R)"
wenzelm@25991
    14
apply (unfold if_def)
wenzelm@25991
    15
apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
wenzelm@25991
    16
done
wenzelm@25991
    17
wenzelm@25991
    18
lemma ifE:
wenzelm@25991
    19
  assumes 1: "p : if(P,Q,R)" and
wenzelm@25991
    20
    2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
wenzelm@25991
    21
    3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
wenzelm@25991
    22
  shows "?p : S"
wenzelm@25991
    23
apply (insert 1)
wenzelm@25991
    24
apply (unfold if_def)
wenzelm@25991
    25
apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
wenzelm@25991
    26
done
wenzelm@25991
    27
wenzelm@25991
    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))"
wenzelm@25991
    29
apply (rule iffI)
wenzelm@25991
    30
apply (erule ifE)
wenzelm@25991
    31
apply (erule ifE)
wenzelm@25991
    32
apply (rule ifI)
wenzelm@25991
    33
apply (rule ifI)
wenzelm@25991
    34
oops
wenzelm@25991
    35
wenzelm@25991
    36
ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
wenzelm@25991
    37
wenzelm@25991
    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))"
wenzelm@25991
    39
apply (tactic {* fast_tac if_cs 1 *})
wenzelm@25991
    40
done
wenzelm@25991
    41
wenzelm@25991
    42
lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
wenzelm@25991
    43
apply (tactic {* fast_tac if_cs 1 *})
wenzelm@25991
    44
done
wenzelm@17480
    45
clasohm@0
    46
end