equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
4 Copyright 1997 TU Muenchen |
4 Copyright 1997 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
|
7 theory MuckeExample2 |
|
8 imports MuckeSyn |
|
9 begin |
7 |
10 |
8 MuckeExample2 = MuckeSyn + |
11 constdefs |
|
12 Init :: "bool pred" |
|
13 "Init x == x" |
|
14 R :: "[bool,bool] => bool" |
|
15 "R x y == (x & ~y) | (~x & y)" |
|
16 Reach :: "bool pred" |
|
17 "Reach == mu (%Q x. Init x | (? y. Q y & R y x))" |
|
18 Reach2:: "bool pred" |
|
19 "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))" |
9 |
20 |
10 consts |
21 lemmas Reach_rws = Init_def R_def Reach_def Reach2_def |
11 |
22 |
12 Init :: "bool pred" |
23 lemma Reach: "Reach2 True" |
13 R :: "[bool,bool] => bool" |
24 apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *}) |
14 Reach :: "bool pred" |
25 apply (tactic {* mc_mucke_tac [] 1 *}) |
15 Reach2:: "bool pred" |
26 done |
16 |
27 |
17 defs |
28 (*alternative:*) |
18 |
29 lemma Reach': "Reach2 True" |
19 Init_def " Init x == x" |
30 by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *}) |
20 |
|
21 R_def "R x y == (x & ~y) | (~x & y)" |
|
22 |
|
23 Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))" |
|
24 |
|
25 Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))" |
|
26 |
31 |
27 end |
32 end |