equal
deleted
inserted
replaced
2833 *} |
2833 *} |
2834 |
2834 |
2835 context valid_trace |
2835 context valid_trace |
2836 begin |
2836 begin |
2837 |
2837 |
2838 lemma rtree_RAG: "rtree (RAG s)" |
2838 lemma forest_RAG: "forest (RAG s)" |
2839 using sgv_RAG acyclic_RAG |
2839 using sgv_RAG acyclic_RAG |
2840 by (unfold rtree_def, auto) |
2840 by (unfold forest_def, auto) |
2841 |
2841 |
2842 end |
2842 end |
2843 |
2843 |
2844 sublocale valid_trace < rtree_RAG?: rtree "RAG s" |
2844 sublocale valid_trace < forest_RAG?: forest "RAG s" |
2845 using rtree_RAG . |
2845 using forest_RAG . |
2846 |
2846 |
2847 sublocale valid_trace < fsbtRAGs?: fgraph "RAG s" |
2847 sublocale valid_trace < fsbtRAGs?: fforest "RAG s" |
2848 proof |
2848 proof |
2849 show "\<And>x. finite (children (RAG s) x)" |
2849 show "\<And>x. finite (children (RAG s) x)" |
2850 by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI) |
2850 by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI) |
2851 (*by (rule finite_fbranchI[OF finite_RAG])*) |
2851 (*by (rule finite_fbranchI[OF finite_RAG])*) |
2852 next |
2852 next |
2884 text {* |
2884 text {* |
2885 It can be shown that @{term tRAG} is also a |
2885 It can be shown that @{term tRAG} is also a |
2886 finite-branch relational tree (or forest): |
2886 finite-branch relational tree (or forest): |
2887 *} |
2887 *} |
2888 |
2888 |
2889 sublocale valid_trace < rtree_s?: rtree "tRAG s" |
2889 sublocale valid_trace < forest_s?: forest "tRAG s" |
2890 proof(unfold_locales) |
2890 proof(unfold_locales) |
2891 from sgv_tRAG show "single_valued (tRAG s)" . |
2891 from sgv_tRAG show "single_valued (tRAG s)" . |
2892 next |
2892 next |
2893 from acyclic_tRAG show "acyclic (tRAG s)" . |
2893 from acyclic_tRAG show "acyclic (tRAG s)" . |
2894 qed |
2894 qed |
2895 |
2895 |
2896 |
2896 |
2897 sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s" |
2897 sublocale valid_trace < fsbttRAGs?: fforest "tRAG s" |
2898 proof |
2898 proof |
2899 fix x |
2899 fix x |
2900 show "finite (children (tRAG s) x)" |
2900 show "finite (children (tRAG s) x)" |
2901 proof(unfold tRAG_def, rule fbranch_compose1[rule_format]) |
2901 proof(unfold tRAG_def, rule fbranch_compose1[rule_format]) |
2902 fix x show "finite (children (wRAG s) x)" |
2902 fix x show "finite (children (wRAG s) x)" |
3208 by (auto simp:subtree_def) |
3208 by (auto simp:subtree_def) |
3209 from star_rpath[OF this(1)] star_rpath[OF this(2)] |
3209 from star_rpath[OF this(1)] star_rpath[OF this(2)] |
3210 obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)" |
3210 obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)" |
3211 "rpath (RAG s) n xs2 (Th th2)" by metis |
3211 "rpath (RAG s) n xs2 (Th th2)" by metis |
3212 hence False |
3212 hence False |
3213 proof(cases rule:rtree_RAG.rpath_overlap') |
3213 proof(cases rule:forest_RAG.rpath_overlap') |
3214 case (less_1 xs3) |
3214 case (less_1 xs3) |
3215 from rpath_star[OF this(3)] |
3215 from rpath_star[OF this(3)] |
3216 have "Th th1 \<in> subtree (RAG s) (Th th2)" |
3216 have "Th th1 \<in> subtree (RAG s) (Th th2)" |
3217 by (auto simp:subtree_def) |
3217 by (auto simp:subtree_def) |
3218 thus ?thesis |
3218 thus ?thesis |