equal
deleted
inserted
replaced
73 lemma fixedpoint_invariant_correct: |
73 lemma fixedpoint_invariant_correct: |
74 "fixedpoint \<inter> reach_invariant = { %v. (init, v) \<in> edges^* }" |
74 "fixedpoint \<inter> reach_invariant = { %v. (init, v) \<in> edges^* }" |
75 apply (unfold fixedpoint_def) |
75 apply (unfold fixedpoint_def) |
76 apply (rule equalityI) |
76 apply (rule equalityI) |
77 apply (auto intro!: ext) |
77 apply (auto intro!: ext) |
78 prefer 2 apply (blast intro: rtrancl_trans) |
78 (* CBtrancl: prefer 2 apply (blast intro: rtrancl_trans) *) |
79 apply (erule rtrancl_induct, auto) |
79 apply (erule rtrancl_induct, auto) |
80 done |
80 done |
81 |
81 |
82 lemma lemma1: |
82 lemma lemma1: |
83 "FP Rprg \<subseteq> fixedpoint" |
83 "FP Rprg \<subseteq> fixedpoint" |