equal
deleted
inserted
replaced
677 definition |
677 definition |
678 s_tG_abv: |
678 s_tG_abv: |
679 "tG (s::state) \<equiv> tG_raw (wq s)" |
679 "tG (s::state) \<equiv> tG_raw (wq s)" |
680 |
680 |
681 lemma tG_alt_def: |
681 lemma tG_alt_def: |
682 "tG s = {(th1, th2) | th1 th2. |
682 "tG s = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2. |
683 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R") |
683 \<exists> cs. (Th th\<^sub>1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th\<^sub>2) \<in> RAG s}" (is "?L = ?R") |
684 by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp) |
684 by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp) |
685 |
685 |
686 lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" |
686 lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" |
687 by (unfold tRAG_alt_def tG_alt_def, auto) |
687 by (unfold tRAG_alt_def tG_alt_def, auto) |
688 |
688 |