equal
deleted
inserted
replaced
2911 using sgv_RAG acyclic_RAG |
2911 using sgv_RAG acyclic_RAG |
2912 by (unfold rtree_def rtree_axioms_def sgv_def, auto) |
2912 by (unfold rtree_def rtree_axioms_def sgv_def, auto) |
2913 |
2913 |
2914 end |
2914 end |
2915 |
2915 |
2916 sublocale valid_trace < rtree_RAG: rtree "RAG s" |
2916 sublocale valid_trace < rtree_RAG?: rtree "RAG s" |
2917 using rtree_RAG . |
2917 using rtree_RAG . |
2918 |
2918 |
2919 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" |
2919 sublocale valid_trace < fsbtRAGs?: fsubtree "RAG s" |
2920 proof - |
2920 proof - |
2921 show "fsubtree (RAG s)" |
2921 show "fsubtree (RAG s)" |
2922 proof(intro_locales) |
2922 proof(intro_locales) |
2923 show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . |
2923 show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . |
2924 next |
2924 next |
2960 text {* |
2960 text {* |
2961 It can be shown that @{term tRAG} is also a |
2961 It can be shown that @{term tRAG} is also a |
2962 finite-branch relational tree (or forest): |
2962 finite-branch relational tree (or forest): |
2963 *} |
2963 *} |
2964 |
2964 |
2965 sublocale valid_trace < rtree_s: rtree "tRAG s" |
2965 sublocale valid_trace < rtree_s?: rtree "tRAG s" |
2966 proof(unfold_locales) |
2966 proof(unfold_locales) |
2967 from sgv_tRAG show "single_valued (tRAG s)" . |
2967 from sgv_tRAG show "single_valued (tRAG s)" . |
2968 next |
2968 next |
2969 from acyclic_tRAG show "acyclic (tRAG s)" . |
2969 from acyclic_tRAG show "acyclic (tRAG s)" . |
2970 qed |
2970 qed |
2971 |
2971 |
2972 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s" |
2972 sublocale valid_trace < fsbttRAGs?: fsubtree "tRAG s" |
2973 proof - |
2973 proof - |
2974 have "fsubtree (tRAG s)" |
2974 have "fsubtree (tRAG s)" |
2975 proof - |
2975 proof - |
2976 have "fbranch (tRAG s)" |
2976 have "fbranch (tRAG s)" |
2977 proof(unfold tRAG_def, rule fbranch_compose) |
2977 proof(unfold tRAG_def, rule fbranch_compose) |