# HG changeset patch # User paulson # Date 961749271 -7200 # Node ID 33b32680669a250a1ce6737852606722f6e40c95 # Parent 40d759b9725f2184a708e7f0f22908b369cd4c6b genPrefix_trans_O: generalizes genPrefix_trans diff -r 40d759b9725f -r 33b32680669a src/HOL/UNITY/GenPrefix.ML --- a/src/HOL/UNITY/GenPrefix.ML Fri Jun 23 10:33:46 2000 +0200 +++ b/src/HOL/UNITY/GenPrefix.ML Fri Jun 23 10:34:31 2000 +0200 @@ -67,24 +67,50 @@ Addsimps [genPrefix_refl]; +Goal "r<=s ==> genPrefix r <= genPrefix s"; +by (Clarify_tac 1); +by (etac genPrefix.induct 1); +by (auto_tac (claset() addIs [genPrefix.append], simpset())); +qed "genPrefix_mono"; + (** Transitivity **) -(*Merely a lemma for proving transitivity*) +(*A lemma for proving genPrefix_trans_O*) Goal "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"; by (induct_tac "xs" 1); by Auto_tac; qed_spec_mp "append_genPrefix"; -Goalw [trans_def] - "[| (x, y) : genPrefix r; trans r |] \ -\ ==> ALL z. (y, z) : genPrefix r --> (x, z) : genPrefix r"; +(*Lemma proving transitivity and more*) +Goalw [prefix_def] + "(x, y) : genPrefix r \ +\ ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"; by (etac genPrefix.induct 1); -by (blast_tac (claset() addDs [append_genPrefix]) 3); -by (blast_tac (claset() addIs [genPrefix.prepend]) 2); + by (blast_tac (claset() addDs [append_genPrefix]) 3); + by (blast_tac (claset() addIs [genPrefix.prepend]) 2); by (Blast_tac 1); +qed_spec_mp "genPrefix_trans_O"; + +Goal "[| (x,y) : genPrefix r; (y,z) : genPrefix r; trans r |] \ +\ ==> (x,z) : genPrefix r"; +by (rtac (impOfSubs (trans_O_subset RS genPrefix_mono)) 1); + by (assume_tac 2); +by (blast_tac (claset() addIs [genPrefix_trans_O]) 1); qed_spec_mp "genPrefix_trans"; +Goalw [prefix_def] + "[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"; +by (stac (R_O_Id RS sym) 1 THEN etac genPrefix_trans_O 1); +by (assume_tac 1); +qed_spec_mp "prefix_genPrefix_trans"; + +Goalw [prefix_def] + "[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r"; +by (stac (Id_O_R RS sym) 1 THEN etac genPrefix_trans_O 1); +by (assume_tac 1); +qed_spec_mp "genPrefix_prefix_trans"; + Goal "trans r ==> trans (genPrefix r)"; by (blast_tac (claset() addIs [transI, genPrefix_trans]) 1); qed "trans_genPrefix"; @@ -329,12 +355,6 @@ by Auto_tac; qed_spec_mp "common_prefix_linear"; -Goal "r<=s ==> genPrefix r <= genPrefix s"; -by (Clarify_tac 1); -by (etac genPrefix.induct 1); -by (auto_tac (claset() addIs [genPrefix.append], simpset())); -qed "genPrefix_mono"; - (*** pfixLe, pfixGe: properties inherited from the translations ***)