2844 sublocale valid_trace < rtree_RAG?: rtree "RAG s" |
2844 sublocale valid_trace < rtree_RAG?: rtree "RAG s" |
2845 using rtree_RAG . |
2845 using rtree_RAG . |
2846 |
2846 |
2847 sublocale valid_trace < fsbtRAGs?: fgraph "RAG s" |
2847 sublocale valid_trace < fsbtRAGs?: fgraph "RAG s" |
2848 proof |
2848 proof |
2849 show "\<forall>x\<in>Range (RAG s). finite (children (RAG s) x)" |
2849 show "\<And>x. finite (children (RAG s) x)" |
2850 by (rule finite_fbranchI[OF finite_RAG]) |
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 next |
2852 next |
2852 show "wf (RAG s)" using wf_RAG . |
2853 show "wf (RAG s)" using wf_RAG . |
2853 qed |
2854 qed |
2854 |
2855 |
2855 subsection {* Derived properties for sub-graphs of RAG *} |
2856 subsection {* Derived properties for sub-graphs of RAG *} |
2890 from sgv_tRAG show "single_valued (tRAG s)" . |
2891 from sgv_tRAG show "single_valued (tRAG s)" . |
2891 next |
2892 next |
2892 from acyclic_tRAG show "acyclic (tRAG s)" . |
2893 from acyclic_tRAG show "acyclic (tRAG s)" . |
2893 qed |
2894 qed |
2894 |
2895 |
|
2896 |
2895 sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s" |
2897 sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s" |
2896 proof |
2898 proof |
2897 show "\<forall>x\<in>Range (tRAG s). finite (children (tRAG s) x)" |
2899 fix x |
2898 proof(unfold tRAG_def, rule fbranch_compose) |
2900 show "finite (children (tRAG s) x)" |
2899 show "\<forall>x\<in>Range (wRAG s). finite (children (wRAG s) x)" |
2901 proof(unfold tRAG_def, rule fbranch_compose1[rule_format]) |
2900 proof(rule finite_fbranchI) |
2902 fix x show "finite (children (wRAG s) x)" |
2901 from finite_RAG show "finite (wRAG s)" |
2903 proof(rule finite_fbranchI1[rule_format]) |
2902 by (unfold RAG_split, auto) |
2904 show "finite (wRAG s)" using finite_RAG[unfolded RAG_split] by auto |
2903 qed |
2905 qed |
2904 next |
2906 next |
2905 show "\<forall>x\<in>Range (hRAG s). finite (children (hRAG s) x)" |
2907 fix x |
2906 proof(rule finite_fbranchI) |
2908 show "finite (children (hRAG s) x)" |
2907 from finite_RAG |
2909 proof(rule finite_fbranchI1[rule_format]) |
2908 show "finite (hRAG s)" by (unfold RAG_split, auto) |
2910 show "finite (hRAG s)" using finite_RAG[unfolded RAG_split] by auto |
2909 qed |
2911 qed |
2910 qed |
2912 qed |
2911 next |
2913 next |
2912 show "wf (tRAG s)" |
2914 show "wf (tRAG s)" |
2913 proof(rule wf_subset) |
2915 proof(rule wf_subset) |
2914 show "wf (RAG s O RAG s)" using wf_RAG |
2916 show "wf (RAG s O RAG s)" using wf_RAG |