src/HOL/UNITY/ListOrder.thy
changeset 45477 11d9c2768729
parent 35416 d8d7d1b785af
child 46577 e5438c5797ae
     1.1 --- a/src/HOL/UNITY/ListOrder.thy	Sat Nov 12 20:14:09 2011 +0100
     1.2 +++ b/src/HOL/UNITY/ListOrder.thy	Sat Nov 12 21:10:56 2011 +0100
     1.3 @@ -106,36 +106,39 @@
     1.4  (** Transitivity **)
     1.5  
     1.6  (*A lemma for proving genPrefix_trans_O*)
     1.7 -lemma append_genPrefix [rule_format]:
     1.8 -     "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
     1.9 -by (induct_tac "xs", auto)
    1.10 +lemma append_genPrefix:
    1.11 +     "(xs @ ys, zs) : genPrefix r \<Longrightarrow> (xs, zs) : genPrefix r"
    1.12 +  by (induct xs arbitrary: zs) auto
    1.13  
    1.14  (*Lemma proving transitivity and more*)
    1.15 -lemma genPrefix_trans_O [rule_format]: 
    1.16 -     "(x, y) : genPrefix r  
    1.17 -      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
    1.18 -apply (erule genPrefix.induct)
    1.19 -  prefer 3 apply (blast dest: append_genPrefix)
    1.20 - prefer 2 apply (blast intro: genPrefix.prepend, blast)
    1.21 -done
    1.22 +lemma genPrefix_trans_O:
    1.23 +  assumes "(x, y) : genPrefix r"
    1.24 +  shows "\<And>z. (y, z) : genPrefix s \<Longrightarrow> (x, z) : genPrefix (r O s)"
    1.25 +  apply (atomize (full))
    1.26 +  using assms
    1.27 +  apply induct
    1.28 +    apply blast
    1.29 +   apply (blast intro: genPrefix.prepend)
    1.30 +  apply (blast dest: append_genPrefix)
    1.31 +  done
    1.32  
    1.33 -lemma genPrefix_trans [rule_format]:
    1.34 -     "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]  
    1.35 -      ==> (x,z) : genPrefix r"
    1.36 -apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
    1.37 - apply assumption
    1.38 -apply (blast intro: genPrefix_trans_O)
    1.39 -done
    1.40 +lemma genPrefix_trans:
    1.41 +  "(x, y) : genPrefix r \<Longrightarrow> (y, z) : genPrefix r \<Longrightarrow> trans r
    1.42 +    \<Longrightarrow> (x, z) : genPrefix r"
    1.43 +  apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
    1.44 +   apply assumption
    1.45 +  apply (blast intro: genPrefix_trans_O)
    1.46 +  done
    1.47  
    1.48 -lemma prefix_genPrefix_trans [rule_format]: 
    1.49 -     "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
    1.50 +lemma prefix_genPrefix_trans:
    1.51 +  "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
    1.52  apply (unfold prefix_def)
    1.53  apply (drule genPrefix_trans_O, assumption)
    1.54  apply simp
    1.55  done
    1.56  
    1.57 -lemma genPrefix_prefix_trans [rule_format]: 
    1.58 -     "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
    1.59 +lemma genPrefix_prefix_trans:
    1.60 +  "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
    1.61  apply (unfold prefix_def)
    1.62  apply (drule genPrefix_trans_O, assumption)
    1.63  apply simp
    1.64 @@ -147,23 +150,30 @@
    1.65  
    1.66  (** Antisymmetry **)
    1.67  
    1.68 -lemma genPrefix_antisym [rule_format]:
    1.69 -     "[| (xs,ys) : genPrefix r;  antisym r |]  
    1.70 -      ==> (ys,xs) : genPrefix r --> xs = ys"
    1.71 -apply (erule genPrefix.induct)
    1.72 -  txt{*Base case*}
    1.73 -  apply blast
    1.74 - txt{*prepend case*}
    1.75 - apply (simp add: antisym_def)
    1.76 -txt{*append case is the hardest*}
    1.77 -apply clarify
    1.78 -apply (subgoal_tac "length zs = 0", force)
    1.79 -apply (drule genPrefix_length_le)+
    1.80 -apply (simp del: length_0_conv)
    1.81 -done
    1.82 +lemma genPrefix_antisym:
    1.83 +  assumes 1: "(xs, ys) : genPrefix r"
    1.84 +    and 2: "antisym r"
    1.85 +    and 3: "(ys, xs) : genPrefix r"
    1.86 +  shows "xs = ys"
    1.87 +  using 1 3
    1.88 +proof induct
    1.89 +  case Nil
    1.90 +  then show ?case by blast
    1.91 +next
    1.92 +  case prepend
    1.93 +  then show ?case using 2 by (simp add: antisym_def)
    1.94 +next
    1.95 +  case (append xs ys zs)
    1.96 +  then show ?case
    1.97 +    apply -
    1.98 +    apply (subgoal_tac "length zs = 0", force)
    1.99 +    apply (drule genPrefix_length_le)+
   1.100 +    apply (simp del: length_0_conv)
   1.101 +    done
   1.102 +qed
   1.103  
   1.104  lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
   1.105 -by (blast intro: antisymI genPrefix_antisym)
   1.106 +  by (blast intro: antisymI genPrefix_antisym)
   1.107  
   1.108  
   1.109  subsection{*recursion equations*}
   1.110 @@ -229,23 +239,23 @@
   1.111  
   1.112  (** Proving the equivalence with Charpentier's definition **)
   1.113  
   1.114 -lemma genPrefix_imp_nth [rule_format]:
   1.115 -     "ALL i ys. i < length xs  
   1.116 -                --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
   1.117 -apply (induct_tac "xs", auto)
   1.118 -apply (case_tac "i", auto)
   1.119 -done
   1.120 +lemma genPrefix_imp_nth:
   1.121 +    "i < length xs \<Longrightarrow> (xs, ys) : genPrefix r \<Longrightarrow> (xs ! i, ys ! i) : r"
   1.122 +  apply (induct xs arbitrary: i ys)
   1.123 +   apply auto
   1.124 +  apply (case_tac i)
   1.125 +   apply auto
   1.126 +  done
   1.127  
   1.128 -lemma nth_imp_genPrefix [rule_format]:
   1.129 -     "ALL ys. length xs <= length ys   
   1.130 -      --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)   
   1.131 -      --> (xs, ys) : genPrefix r"
   1.132 -apply (induct_tac "xs")
   1.133 -apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
   1.134 -apply clarify
   1.135 -apply (case_tac "ys")
   1.136 -apply (force+)
   1.137 -done
   1.138 +lemma nth_imp_genPrefix:
   1.139 +  "length xs <= length ys \<Longrightarrow>
   1.140 +     (\<forall>i. i < length xs --> (xs ! i, ys ! i) : r) \<Longrightarrow>
   1.141 +     (xs, ys) : genPrefix r"
   1.142 +  apply (induct xs arbitrary: ys)
   1.143 +   apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib)
   1.144 +  apply (case_tac ys)
   1.145 +   apply (force+)
   1.146 +  done
   1.147  
   1.148  lemma genPrefix_iff_nth:
   1.149       "((xs,ys) : genPrefix r) =  
   1.150 @@ -371,10 +381,10 @@
   1.151  
   1.152  (*Although the prefix ordering is not linear, the prefixes of a list
   1.153    are linearly ordered.*)
   1.154 -lemma common_prefix_linear [rule_format]:
   1.155 -     "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
   1.156 -by (rule_tac xs = zs in rev_induct, auto)
   1.157 -
   1.158 +lemma common_prefix_linear:
   1.159 +  fixes xs ys zs :: "'a list"
   1.160 +  shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs"
   1.161 +  by (induct zs rule: rev_induct) auto
   1.162  
   1.163  subsection{*pfixLe, pfixGe: properties inherited from the translations*}
   1.164