reactivate postfix by change of syntax;
authorwenzelm
Wed Aug 31 15:46:38 2005 +0200 (2005-08-31)
changeset 172013bdf1dfcdee4
parent 17200 3a4d03d1a31b
child 17202 d364e0fd9c2f
reactivate postfix by change of syntax;
tuned presentation;
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Wed Aug 31 15:46:37 2005 +0200
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Aug 31 15:46:38 2005 +0200
     1.3 @@ -30,11 +30,11 @@
     1.4    by (unfold strict_prefix_def prefix_def) blast
     1.5  
     1.6  lemma strict_prefixE' [elim?]:
     1.7 -    "xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C"
     1.8 +  assumes lt: "xs < ys"
     1.9 +    and r: "!!z zs. ys = xs @ z # zs ==> C"
    1.10 +  shows C
    1.11  proof -
    1.12 -  assume r: "!!z zs. ys = xs @ z # zs ==> C"
    1.13 -  assume "xs < ys"
    1.14 -  then obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.15 +  from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    1.16      by (unfold strict_prefix_def prefix_def) blast
    1.17    with r show ?thesis by (auto simp add: neq_Nil_conv)
    1.18  qed
    1.19 @@ -105,7 +105,7 @@
    1.20  qed
    1.21  
    1.22  lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs"
    1.23 -by(simp add:prefix_def) blast
    1.24 +  by (auto simp add: prefix_def)
    1.25  
    1.26  theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))"
    1.27    by (cases xs) (auto simp add: prefix_def)
    1.28 @@ -130,28 +130,27 @@
    1.29  theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys"
    1.30    by (auto simp add: prefix_def)
    1.31  
    1.32 -
    1.33  lemma prefix_same_cases:
    1.34 - "\<lbrakk> (xs\<^isub>1::'a list) \<le> ys; xs\<^isub>2 \<le> ys \<rbrakk> \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
    1.35 -apply(simp add:prefix_def)
    1.36 -apply(erule exE)+
    1.37 -apply(simp add: append_eq_append_conv_if split:if_splits)
    1.38 - apply(rule disjI2)
    1.39 - apply(rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
    1.40 - apply clarify
    1.41 - apply(drule sym)
    1.42 - apply(insert append_take_drop_id[of "length xs\<^isub>2" xs\<^isub>1])
    1.43 - apply simp
    1.44 -apply(rule disjI1)
    1.45 -apply(rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
    1.46 -apply clarify
    1.47 -apply(insert append_take_drop_id[of "length xs\<^isub>1" xs\<^isub>2])
    1.48 -apply simp
    1.49 -done
    1.50 +    "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1"
    1.51 +  apply (simp add: prefix_def)
    1.52 +  apply (erule exE)+
    1.53 +  apply (simp add: append_eq_append_conv_if split: if_splits)
    1.54 +   apply (rule disjI2)
    1.55 +   apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI)
    1.56 +   apply clarify
    1.57 +   apply (drule sym)
    1.58 +   apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1])
    1.59 +   apply simp
    1.60 +  apply (rule disjI1)
    1.61 +  apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI)
    1.62 +  apply clarify
    1.63 +  apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2])
    1.64 +  apply simp
    1.65 +  done
    1.66  
    1.67  lemma set_mono_prefix:
    1.68 - "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
    1.69 -by(fastsimp simp add:prefix_def)
    1.70 +    "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
    1.71 +  by (auto simp add: prefix_def)
    1.72  
    1.73  
    1.74  subsection {* Parallel lists *}
    1.75 @@ -215,48 +214,48 @@
    1.76  
    1.77  
    1.78  subsection {* Postfix order on lists *}
    1.79 -(*
    1.80 +
    1.81  constdefs
    1.82 -  postfix :: "'a list => 'a list => bool"  ("(_/ >= _)" [51, 50] 50)
    1.83 -  "xs >= ys == \<exists>zs. xs = zs @ ys"
    1.84 +  postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
    1.85 +  "xs >>= ys == \<exists>zs. xs = zs @ ys"
    1.86  
    1.87 -lemma postfix_refl [simp, intro!]: "xs >= xs"
    1.88 +lemma postfix_refl [simp, intro!]: "xs >>= xs"
    1.89    by (auto simp add: postfix_def)
    1.90 -lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs"
    1.91 +lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs"
    1.92    by (auto simp add: postfix_def)
    1.93 -lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys"
    1.94 +lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys"
    1.95    by (auto simp add: postfix_def)
    1.96  
    1.97 -lemma Nil_postfix [iff]: "xs >= []"
    1.98 +lemma Nil_postfix [iff]: "xs >>= []"
    1.99    by (simp add: postfix_def)
   1.100 -lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])"
   1.101 +lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])"
   1.102    by (auto simp add:postfix_def)
   1.103  
   1.104 -lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys"
   1.105 +lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys"
   1.106    by (auto simp add: postfix_def)
   1.107 -lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys"
   1.108 +lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys"
   1.109    by (auto simp add: postfix_def)
   1.110  
   1.111 -lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs @ xs >= ys"
   1.112 +lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys"
   1.113    by (auto simp add: postfix_def)
   1.114 -lemma postfix_appendD: "xs >= zs @ ys \<Longrightarrow> xs >= ys"
   1.115 +lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys"
   1.116    by(auto simp add: postfix_def)
   1.117  
   1.118  lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
   1.119    by (induct zs, auto)
   1.120 -lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs"
   1.121 +lemma postfix_is_subset: "xs >>= ys \<Longrightarrow> set ys \<subseteq> set xs"
   1.122    by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
   1.123  
   1.124 -lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys"
   1.125 +lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >>= ys"
   1.126    by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
   1.127 -lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys"
   1.128 +lemma postfix_ConsD2: "x#xs >>= y#ys \<Longrightarrow> xs >>= ys"
   1.129    by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
   1.130  
   1.131 -lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)"
   1.132 +lemma postfix2prefix: "(xs >>= ys) = (rev ys <= rev xs)"
   1.133    apply (unfold prefix_def postfix_def, safe)
   1.134 -  apply (rule_tac x = "rev zs" in exI, simp)
   1.135 +   apply (rule_tac x = "rev zs" in exI, simp)
   1.136    apply (rule_tac x = "rev zs" in exI)
   1.137    apply (rule rev_is_rev_conv [THEN iffD1], simp)
   1.138    done
   1.139 -*)
   1.140 +
   1.141  end