equal
deleted
inserted
replaced
28 b2 :: "'a -> tr" and |
28 b2 :: "'a -> tr" and |
29 g :: "'a -> 'a" |
29 g :: "'a -> 'a" |
30 |
30 |
31 definition |
31 definition |
32 p :: "'a -> 'a" where |
32 p :: "'a -> 'a" where |
33 "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)" |
33 "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)" |
34 |
34 |
35 definition |
35 definition |
36 q :: "'a -> 'a" where |
36 q :: "'a -> 'a" where |
37 "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)" |
37 "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x)" |
38 |
38 |
39 |
39 |
40 (* --------- pure HOLCF logic, some little lemmas ------ *) |
40 (* --------- pure HOLCF logic, some little lemmas ------ *) |
41 |
41 |
42 lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU" |
42 lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU" |
100 done |
100 done |
101 |
101 |
102 |
102 |
103 (* ----- access to definitions ----- *) |
103 (* ----- access to definitions ----- *) |
104 |
104 |
105 lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi" |
105 lemma p_def3: "p$x = If b1$x then p$(g$x) else x" |
106 apply (rule trans) |
106 apply (rule trans) |
107 apply (rule p_def [THEN eq_reflection, THEN fix_eq3]) |
107 apply (rule p_def [THEN eq_reflection, THEN fix_eq3]) |
108 apply simp |
108 apply simp |
109 done |
109 done |
110 |
110 |
111 lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi" |
111 lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x" |
112 apply (rule trans) |
112 apply (rule trans) |
113 apply (rule q_def [THEN eq_reflection, THEN fix_eq3]) |
113 apply (rule q_def [THEN eq_reflection, THEN fix_eq3]) |
114 apply simp |
114 apply simp |
115 done |
115 done |
116 |
116 |