src/FOLP/ex/If.thy
 author wenzelm Fri Apr 23 23:35:43 2010 +0200 (2010-04-23) changeset 36319 8feb2c4bef1a parent 35762 af3ff2ba4c54 child 58957 c9e744ea8a38 permissions -rw-r--r--
mark schematic statements explicitly;
```     1 theory If
```
```     2 imports FOLP
```
```     3 begin
```
```     4
```
```     5 definition "if" :: "[o,o,o]=>o" where
```
```     6   "if(P,Q,R) == P&Q | ~P&R"
```
```     7
```
```     8 schematic_lemma ifI:
```
```     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)
```
```    12 apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
```
```    13 done
```
```    14
```
```    15 schematic_lemma ifE:
```
```    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)
```
```    22 apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
```
```    23 done
```
```    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))"
```
```    26 apply (rule iffI)
```
```    27 apply (erule ifE)
```
```    28 apply (erule ifE)
```
```    29 apply (rule ifI)
```
```    30 apply (rule ifI)
```
```    31 oops
```
```    32
```
```    33 ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
```
```    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))"
```
```    36 apply (tactic {* fast_tac if_cs 1 *})
```
```    37 done
```
```    38
```
```    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 *})
```
```    41 done
```
```    42
```
```    43 end
```