src/FOLP/ex/If.thy
changeset 58957 c9e744ea8a38
parent 36319 8feb2c4bef1a
child 60770 240563fbf41d
equal deleted inserted replaced
58956:a816aa3ff391 58957:c9e744ea8a38
     7 
     7 
     8 schematic_lemma ifI:
     8 schematic_lemma ifI:
     9   assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
     9   assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
    10   shows "?p : if(P,Q,R)"
    10   shows "?p : if(P,Q,R)"
    11 apply (unfold if_def)
    11 apply (unfold if_def)
    12 apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
    12 apply (tactic {* fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1 *})
    13 done
    13 done
    14 
    14 
    15 schematic_lemma ifE:
    15 schematic_lemma ifE:
    16   assumes 1: "p : if(P,Q,R)" and
    16   assumes 1: "p : if(P,Q,R)" and
    17     2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" 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"
    18     3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
    19   shows "?p : S"
    19   shows "?p : S"
    20 apply (insert 1)
    20 apply (insert 1)
    21 apply (unfold if_def)
    21 apply (unfold if_def)
    22 apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
    22 apply (tactic {* fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
    23 done
    23 done
    24 
    24 
    25 schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    25 schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    26 apply (rule iffI)
    26 apply (rule iffI)
    27 apply (erule ifE)
    27 apply (erule ifE)
    31 oops
    31 oops
    32 
    32 
    33 ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
    33 ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
    34 
    34 
    35 schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    35 schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    36 apply (tactic {* fast_tac if_cs 1 *})
    36 apply (tactic {* fast_tac @{context} if_cs 1 *})
    37 done
    37 done
    38 
    38 
    39 schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    39 schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    40 apply (tactic {* fast_tac if_cs 1 *})
    40 apply (tactic {* fast_tac @{context} if_cs 1 *})
    41 done
    41 done
    42 
    42 
    43 end
    43 end