# HG changeset patch # User Christian Urban # Date 1401804012 -3600 # Node ID 0781a2fc93f13f17ebf53069aa88ae4024d3cd4e # Parent 7ea6b019ce24fe84c3b54ee26163aed8774c9936 added a library about graphs diff -r 7ea6b019ce24 -r 0781a2fc93f1 Graphs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Graphs.thy Tue Jun 03 15:00:12 2014 +0100 @@ -0,0 +1,71 @@ +theory Graphs +imports Main +begin + +lemma rtrancl_eq_trancl [simp]: + assumes "x \ y" + shows "(x, y) \ r\<^sup>* \ (x, y) \ r\<^sup>+" +using assms by (metis rtrancl_eq_or_trancl) + +lemma trancl_split: + "(a, b) \ r^+ \ \ c. (a, c) \ r" +by (induct rule:trancl_induct, auto) + +lemma unique_minus: + assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" + and xy: "(x, y) \ r" + and xz: "(x, z) \ r^+" + and neq: "y \ z" + shows "(y, z) \ r^+" +by (metis converse_tranclE neq unique xy xz) + +lemma unique_base: + assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" + and xy: "(x, y) \ r" + and xz: "(x, z) \ r^+" + and neq_yz: "y \ z" + shows "(y, z) \ r^+" +by (metis neq_yz unique unique_minus xy xz) + +lemma unique_chain_star: + assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" + and xy: "(x, y) \ r^*" + and xz: "(x, z) \ r^*" + shows "(y, z) \ r^* \ (z, y) \ r^*" +thm single_valued_confluent single_valued_def unique xy xz +by (metis single_valued_confluent single_valued_def unique xy xz) + +lemma unique_chain: + assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" + and xy: "(x, y) \ r^+" + and xz: "(x, z) \ r^+" + and neq_yz: "y \ z" + shows "(y, z) \ r^+ \ (z, y) \ r^+" +proof - + have xy_star: "(x, y) \ r^*" + and xz_star: "(x, z) \ r^*" using xy xz by simp_all + from unique_chain_star[OF unique xy_star xz_star] + have "(y, z) \ r\<^sup>* \ (z, y) \ r\<^sup>*" by auto + with neq_yz + show ?thesis by(auto) +qed + +definition funof :: "[('a * 'b)set, 'a] => 'b" where + "funof r == (\x. THE y. (x, y) \ r)" + +lemma funof_eq: "[|single_valued r; (x, y) \ r|] ==> funof r x = y" +by (simp add: funof_def single_valued_def, blast) + +lemma funof_Pair_in: + "[|single_valued r; x \ Domain r|] ==> (x, funof r x) \ r" +by (force simp add: funof_eq) + +lemma funof_in: + "[|r `` {x} \ A; single_valued r; x \ Domain r|] ==> funof r x \ A" +by (force simp add: funof_eq) + +lemma single_valuedP_update: + shows "single_valuedP r \ single_valuedP (r(x := y))" +oops + +end \ No newline at end of file diff -r 7ea6b019ce24 -r 0781a2fc93f1 Test.thy --- a/Test.thy Mon Jun 02 14:58:42 2014 +0100 +++ b/Test.thy Tue Jun 03 15:00:12 2014 +0100 @@ -1,5 +1,5 @@ theory Test -imports Precedence_ord +imports Precedence_ord Graphs begin type_synonym thread = nat -- {* Type for thread identifiers. *} @@ -244,7 +244,21 @@ using assms wq_distinct[OF vt(1), of"cs"] by (auto simp add: Let_def wq_def) -lemma waiting_unique: +(* +lemma single_valued_waits2: + assumes "vt s" + shows "single_valuedP (waits2 s)" +using assms +apply(induct) +apply(simp add: waits2_def waits_def) +apply(erule step.cases) +apply(auto simp add: Let_def waits2_def) +unfolding single_valued_def waits2_def waits_def +apply(auto) +*) + + +lemma waits2_unique: assumes "vt s" and "waits2 s th cs1" and "waits2 s th cs2" @@ -260,11 +274,34 @@ apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) +lemma single_valued_holds2: + assumes "vt s" + shows "single_valuedP (\cs th. holds2 s th cs)" +unfolding single_valued_def holds2_def holds_def by simp -lemma rtrancl_eq_trancl [simp]: - assumes "x \ y" - shows "(x, y) \ r\<^sup>* \ (x, y) \ r\<^sup>+" -using assms by (metis rtrancl_eq_or_trancl) + +lemma holds2_unique: + assumes "holds2 s th1 cs" + and "holds2 s th2 cs" + shows "th1 = th2" +using assms +unfolding holds2_def holds_def by auto + +lemma single_valued_waits2: + assumes "vt s" + shows "single_valuedP (waits2 s)" +by (metis (erased, hide_lams) assms mem_Collect_eq old.prod.case single_valued_def waits2_unique) + + +(* was unique_RAG2 *) +lemma single_valued_RAG2: + assumes "vt s" + shows "single_valued (RAG2 s)" +using single_valued_waits2[OF assms] single_valued_holds2[OF assms] +unfolding RAG2_def RAG_def +unfolding single_valued_def +unfolding holds2_def waits2_def +by auto lemma acyclic_RAG_step: assumes vt: "vt s" @@ -337,7 +374,7 @@ have "waits2 s nth cs'" using b(2) unfolding RAG2_def RAG_def waits2_def by simp ultimately have "cs = cs'" - by (rule_tac waiting_unique[OF vt waits2_cs]) + by (rule_tac waits2_unique[OF vt waits2_cs]) then show "False" using a b(1) by simp qed ultimately @@ -416,4 +453,45 @@ oops + + + + +lemma dchain_unique: + assumes vt: "vt s" + and th1_d: "(n, Th th1) \ (RAG2 s)^+" + and th1_r: "th1 \ readys s" + and th2_d: "(n, Th th2) \ (RAG2 s)^+" + and th2_r: "th2 \ readys s" + shows "th1 = th2" +proof(rule ccontr) + assume neq: "th1 \ th2" + hence "Th th1 \ Th th2" by simp + from unique_chain [OF _ th1_d th2_d this] and single_valued_RAG2 [OF vt] + have "(Th th1, Th th2) \ (RAG2 s)\<^sup>+ \ (Th th2, Th th1) \ (RAG2 s)\<^sup>+" + unfolding single_valued_def by auto + then show "False" + proof + assume "(Th th1, Th th2) \ (RAG2 s)\<^sup>+" + from trancl_split [OF this] + obtain n where dd: "(Th th1, n) \ RAG2 s" by auto + then obtain cs where eq_n: "n = Cs cs" + unfolding RAG2_def RAG_def by (case_tac n) (auto) + from dd eq_n have "th1 \ readys s" + unfolding RAG2_def RAG_def waits2_def readys_def by (auto) + with th1_r show ?thesis by auto + next + assume "(Th th2, Th th1) \ (RAG2 s)\<^sup>+" + from trancl_split [OF this] + obtain n where dd: "(Th th2, n) \ RAG2 s" by auto + then obtain cs where eq_n: "n = Cs cs" + unfolding RAG2_def RAG_def by (case_tac n) (auto) + from dd eq_n have "th2 \ readys s" + unfolding RAG2_def RAG_def waits2_def readys_def by (auto) + with th2_r show ?thesis by auto + qed +qed + + + end \ No newline at end of file