src/HOL/List.ML
changeset 5427 26c9a7c0b36b
parent 5425 157c6663dedd
child 5443 e2459d18ff47
     1.1 --- a/src/HOL/List.ML	Thu Sep 03 16:40:02 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Fri Sep 04 11:01:59 1998 +0200
     1.3 @@ -246,6 +246,63 @@
     1.4  qed "append_eq_appendI";
     1.5  
     1.6  
     1.7 +(***
     1.8 +Simplification procedure for all list equalities.
     1.9 +Currently only tries to rearranges @ to see if
    1.10 +- both lists end in a singleton list,
    1.11 +- or both lists end in the same list.
    1.12 +***)
    1.13 +local
    1.14 +
    1.15 +val list_eq_pattern =
    1.16 +  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
    1.17 +
    1.18 +fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
    1.19 +      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
    1.20 +  | last (Const("List.op @",_) $ _ $ ys) = last ys
    1.21 +  | last t = t;
    1.22 +
    1.23 +fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
    1.24 +  | list1 _ = false;
    1.25 +
    1.26 +fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
    1.27 +      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
    1.28 +  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.29 +  | butlast xs = Const("List.list.[]",fastype_of xs);
    1.30 +
    1.31 +val rearr_tac =
    1.32 +  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
    1.33 +
    1.34 +fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    1.35 +  let
    1.36 +    val lastl = last lhs and lastr = last rhs
    1.37 +    fun rearr conv =
    1.38 +      let val lhs1 = butlast lhs and rhs1 = butlast rhs
    1.39 +          val Type(_,listT::_) = eqT
    1.40 +          val appT = [listT,listT] ---> listT
    1.41 +          val app = Const("List.op @",appT)
    1.42 +          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    1.43 +          val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
    1.44 +          val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
    1.45 +            handle ERROR =>
    1.46 +            error("The error(s) above occurred while trying to prove " ^
    1.47 +                  string_of_cterm ct)
    1.48 +      in Some((conv RS (thm RS trans)) RS eq_reflection) end
    1.49 +
    1.50 +  in if list1 lastl andalso list1 lastr
    1.51 +     then rearr append1_eq_conv
    1.52 +     else
    1.53 +     if lastl aconv lastr
    1.54 +     then rearr append_same_eq
    1.55 +     else None
    1.56 +  end;
    1.57 +in
    1.58 +val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
    1.59 +end;
    1.60 +
    1.61 +Addsimprocs [list_eq_simproc];
    1.62 +
    1.63 +
    1.64  (** map **)
    1.65  
    1.66  section "map";
    1.67 @@ -827,27 +884,59 @@
    1.68  
    1.69  (** upto **)
    1.70  
    1.71 -Goal "!i j. ~ j < i --> j - i < Suc j - i";
    1.72 -by(strip_tac 1);
    1.73 -br diff_less_Suc_diff 1;
    1.74 -be leI 1;
    1.75 -val lemma = result();
    1.76 +(* Does not terminate! *)
    1.77 +Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
    1.78 +by(induct_tac "j" 1);
    1.79 +by Auto_tac;
    1.80 +by(REPEAT(trans_tac 1));
    1.81 +qed "upt_rec";
    1.82  
    1.83 -Goalw [upto_def] "j<i ==> [i..j] = []";
    1.84 +Goal "j<=i ==> [i..j(] = []";
    1.85 +by(stac upt_rec 1);
    1.86 +by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
    1.87 +qed "upt_conv_Nil";
    1.88 +Addsimps [upt_conv_Nil];
    1.89 +
    1.90 +Goal "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]";
    1.91 +by (Asm_simp_tac 1);
    1.92 +qed "upt_Suc";
    1.93 +
    1.94 +Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
    1.95  br trans 1;
    1.96 -brs paired_upto.rules 1;
    1.97 -br lemma 1;
    1.98 -by(Asm_simp_tac 1);
    1.99 -qed "upto_conv_Nil";
   1.100 +by(stac upt_rec 1);
   1.101 +br refl 2;
   1.102 +by (Asm_simp_tac 1);
   1.103 +qed "upt_conv_Cons";
   1.104 +
   1.105 +Goal "length [i..j(] = j-i";
   1.106 +by(induct_tac "j" 1);
   1.107 + by (Simp_tac 1);
   1.108 +by(asm_simp_tac (simpset() addsimps [Suc_diff_le] addSolver cut_trans_tac) 1);
   1.109 +qed "length_upt";
   1.110 +Addsimps [length_upt];
   1.111  
   1.112 -Goalw [upto_def] "i<=j ==> [i..j] = i#[Suc i..j]";
   1.113 -br trans 1;
   1.114 -brs paired_upto.rules 1;
   1.115 -br lemma 1;
   1.116 -by(asm_simp_tac (simpset() addsimps [leD]) 1);
   1.117 -qed "upto_conv_Cons";
   1.118 +Goal "i+k < j --> [i..j(] ! k = i+k";
   1.119 +by(induct_tac "j" 1);
   1.120 + by(Simp_tac 1);
   1.121 +by(asm_simp_tac (simpset() addsimps ([nth_append,less_diff_conv]@add_ac)
   1.122 +                           addSolver cut_trans_tac) 1);
   1.123 +br conjI 1;
   1.124 + by(Clarify_tac 1);
   1.125 + bd add_lessD1 1;
   1.126 + by(trans_tac 1);
   1.127 +by(Clarify_tac 1);
   1.128 +br conjI 1;
   1.129 + by(Clarify_tac 1);
   1.130 + by(subgoal_tac "n=i+k" 1);
   1.131 +  by(Asm_full_simp_tac 1);
   1.132 + by(trans_tac 1);
   1.133 +by(Clarify_tac 1);
   1.134 +by(subgoal_tac "n=i+k" 1);
   1.135 + by(Asm_full_simp_tac 1);
   1.136 +by(trans_tac 1);
   1.137 +qed_spec_mp "nth_upt";
   1.138 +Addsimps [nth_upt];
   1.139  
   1.140 -Addsimps [upto_conv_Nil,upto_conv_Cons];
   1.141  
   1.142  (** nodups & remdups **)
   1.143  section "nodups & remdups";
   1.144 @@ -973,60 +1062,3 @@
   1.145  by (Blast_tac 1);
   1.146  qed "Cons_in_lex";
   1.147  AddIffs [Cons_in_lex];
   1.148 -
   1.149 -
   1.150 -(***
   1.151 -Simplification procedure for all list equalities.
   1.152 -Currently only tries to rearranges @ to see if
   1.153 -- both lists end in a singleton list,
   1.154 -- or both lists end in the same list.
   1.155 -***)
   1.156 -local
   1.157 -
   1.158 -val list_eq_pattern =
   1.159 -  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
   1.160 -
   1.161 -fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
   1.162 -      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
   1.163 -  | last (Const("List.op @",_) $ _ $ ys) = last ys
   1.164 -  | last t = t;
   1.165 -
   1.166 -fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
   1.167 -  | list1 _ = false;
   1.168 -
   1.169 -fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
   1.170 -      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
   1.171 -  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
   1.172 -  | butlast xs = Const("List.list.[]",fastype_of xs);
   1.173 -
   1.174 -val rearr_tac =
   1.175 -  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
   1.176 -
   1.177 -fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
   1.178 -  let
   1.179 -    val lastl = last lhs and lastr = last rhs
   1.180 -    fun rearr conv =
   1.181 -      let val lhs1 = butlast lhs and rhs1 = butlast rhs
   1.182 -          val Type(_,listT::_) = eqT
   1.183 -          val appT = [listT,listT] ---> listT
   1.184 -          val app = Const("List.op @",appT)
   1.185 -          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
   1.186 -          val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
   1.187 -          val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
   1.188 -            handle ERROR =>
   1.189 -            error("The error(s) above occurred while trying to prove " ^
   1.190 -                  string_of_cterm ct)
   1.191 -      in Some((conv RS (thm RS trans)) RS eq_reflection) end
   1.192 -
   1.193 -  in if list1 lastl andalso list1 lastr
   1.194 -     then rearr append1_eq_conv
   1.195 -     else
   1.196 -     if lastl aconv lastr
   1.197 -     then rearr append_same_eq
   1.198 -     else None
   1.199 -  end;
   1.200 -in
   1.201 -val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
   1.202 -end;
   1.203 -
   1.204 -Addsimprocs [list_eq_simproc];