2842 end |
2842 end |
2843 |
2843 |
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?: fsubtree "RAG s" |
2847 sublocale valid_trace < fsbtRAGs?: fgraph "RAG s" |
2848 proof - |
2848 proof |
2849 show "fsubtree (RAG s)" |
2849 show "\<forall>x\<in>Range (RAG s). finite (children (RAG s) x)" |
2850 proof(intro_locales) |
2850 by (rule finite_fbranchI[OF finite_RAG]) |
2851 show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . |
2851 next |
2852 next |
2852 show "wf (RAG s)" using wf_RAG . |
2853 show "fsubtree_axioms (RAG s)" |
|
2854 proof(unfold fsubtree_axioms_def) |
|
2855 from wf_RAG show "wf (RAG s)" . |
|
2856 qed |
|
2857 qed |
|
2858 qed |
2853 qed |
2859 |
2854 |
2860 subsection {* Derived properties for sub-graphs of RAG *} |
2855 subsection {* Derived properties for sub-graphs of RAG *} |
2861 |
2856 |
2862 context valid_trace |
2857 context valid_trace |
2895 from sgv_tRAG show "single_valued (tRAG s)" . |
2890 from sgv_tRAG show "single_valued (tRAG s)" . |
2896 next |
2891 next |
2897 from acyclic_tRAG show "acyclic (tRAG s)" . |
2892 from acyclic_tRAG show "acyclic (tRAG s)" . |
2898 qed |
2893 qed |
2899 |
2894 |
2900 sublocale valid_trace < fsbttRAGs?: fsubtree "tRAG s" |
2895 sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s" |
2901 proof - |
2896 proof |
2902 have "fsubtree (tRAG s)" |
2897 show "\<forall>x\<in>Range (tRAG s). finite (children (tRAG s) x)" |
2903 proof - |
2898 proof(unfold tRAG_def, rule fbranch_compose) |
2904 have "fbranch (tRAG s)" |
2899 show "\<forall>x\<in>Range (wRAG s). finite (children (wRAG s) x)" |
2905 proof(unfold tRAG_def, rule fbranch_compose) |
|
2906 show "fbranch (wRAG s)" |
|
2907 proof(rule finite_fbranchI) |
2900 proof(rule finite_fbranchI) |
2908 from finite_RAG show "finite (wRAG s)" |
2901 from finite_RAG show "finite (wRAG s)" |
2909 by (unfold RAG_split, auto) |
2902 by (unfold RAG_split, auto) |
2910 qed |
2903 qed |
2911 next |
2904 next |
2912 show "fbranch (hRAG s)" |
2905 show "\<forall>x\<in>Range (hRAG s). finite (children (hRAG s) x)" |
2913 proof(rule finite_fbranchI) |
2906 proof(rule finite_fbranchI) |
2914 from finite_RAG |
2907 from finite_RAG |
2915 show "finite (hRAG s)" by (unfold RAG_split, auto) |
2908 show "finite (hRAG s)" by (unfold RAG_split, auto) |
2916 qed |
2909 qed |
2917 qed |
2910 qed |
2918 moreover have "wf (tRAG s)" |
2911 next |
2919 proof(rule wf_subset) |
2912 show "wf (tRAG s)" |
|
2913 proof(rule wf_subset) |
2920 show "wf (RAG s O RAG s)" using wf_RAG |
2914 show "wf (RAG s O RAG s)" using wf_RAG |
2921 by (fold wf_comp_self, simp) |
2915 by (fold wf_comp_self, simp) |
2922 next |
2916 next |
2923 show "tRAG s \<subseteq> (RAG s O RAG s)" |
2917 show "tRAG s \<subseteq> (RAG s O RAG s)" |
2924 by (unfold tRAG_alt_def, auto) |
2918 by (unfold tRAG_alt_def, auto) |
2925 qed |
2919 qed |
2926 ultimately show ?thesis |
|
2927 by (unfold fsubtree_def fsubtree_axioms_def,auto) |
|
2928 qed |
|
2929 from this[folded tRAG_def] show "fsubtree (tRAG s)" . |
|
2930 qed |
2920 qed |
2931 |
2921 |
2932 section {* Chain to readys *} |
2922 section {* Chain to readys *} |
2933 |
2923 |
2934 text {* |
2924 text {* |