src/HOL/List.thy
changeset 13462 56610e2ba220
parent 13366 114b7c14084a
child 13480 bb72bd43c6c3
     1.1 --- a/src/HOL/List.thy	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4 -(* Title:HOL/List.thy
     1.5 -   ID: $Id$
     1.6 -   Author: Tobias Nipkow
     1.7 -   Copyright 1994 TU Muenchen
     1.8 +(*  Title:      HOL/List.thy
     1.9 +    ID:         $Id$
    1.10 +    Author:     Tobias Nipkow
    1.11 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.12  *)
    1.13  
    1.14  header {* The datatype of finite lists *}
    1.15 @@ -367,50 +367,50 @@
    1.16  val append1_eq_conv = thm "append1_eq_conv";
    1.17  val append_same_eq = thm "append_same_eq";
    1.18  
    1.19 -val list_eq_pattern =
    1.20 -Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT)
    1.21 -
    1.22  fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    1.23 -(case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    1.24 -| last (Const("List.op @",_) $ _ $ ys) = last ys
    1.25 -| last t = t
    1.26 +  (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    1.27 +  | last (Const("List.op @",_) $ _ $ ys) = last ys
    1.28 +  | last t = t;
    1.29  
    1.30  fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
    1.31 -| list1 _ = false
    1.32 +  | list1 _ = false;
    1.33  
    1.34  fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
    1.35 -(case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
    1.36 -| butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.37 -| butlast xs = Const("List.list.Nil",fastype_of xs)
    1.38 +  (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
    1.39 +  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.40 +  | butlast xs = Const("List.list.Nil",fastype_of xs);
    1.41  
    1.42  val rearr_tac =
    1.43 -simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons])
    1.44 +  simp_tac (HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons]);
    1.45  
    1.46  fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    1.47 -let
    1.48 -val lastl = last lhs and lastr = last rhs
    1.49 -fun rearr conv =
    1.50 -let val lhs1 = butlast lhs and rhs1 = butlast rhs
    1.51 -val Type(_,listT::_) = eqT
    1.52 -val appT = [listT,listT] ---> listT
    1.53 -val app = Const("List.op @",appT)
    1.54 -val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    1.55 -val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
    1.56 -val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
    1.57 -handle ERROR =>
    1.58 -error("The error(s) above occurred while trying to prove " ^
    1.59 -string_of_cterm ct)
    1.60 -in Some((conv RS (thm RS trans)) RS eq_reflection) end
    1.61 +  let
    1.62 +    val lastl = last lhs and lastr = last rhs;
    1.63 +    fun rearr conv =
    1.64 +      let
    1.65 +        val lhs1 = butlast lhs and rhs1 = butlast rhs;
    1.66 +        val Type(_,listT::_) = eqT
    1.67 +        val appT = [listT,listT] ---> listT
    1.68 +        val app = Const("List.op @",appT)
    1.69 +        val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    1.70 +        val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
    1.71 +        val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
    1.72 +          handle ERROR =>
    1.73 +            error("The error(s) above occurred while trying to prove " ^
    1.74 +              string_of_cterm ct);
    1.75 +      in Some ((conv RS (thm RS trans)) RS eq_reflection) end;
    1.76  
    1.77 -in if list1 lastl andalso list1 lastr
    1.78 - then rearr append1_eq_conv
    1.79 - else
    1.80 - if lastl aconv lastr
    1.81 - then rearr append_same_eq
    1.82 - else None
    1.83 -end
    1.84 +  in
    1.85 +    if list1 lastl andalso list1 lastr then rearr append1_eq_conv
    1.86 +    else if lastl aconv lastr then rearr append_same_eq
    1.87 +    else None
    1.88 +  end;
    1.89 +
    1.90  in
    1.91 -val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq
    1.92 +
    1.93 +val list_eq_simproc =
    1.94 +  Simplifier.simproc (Theory.sign_of (the_context ())) "list_eq" ["(xs::'a list) = ys"] list_eq;
    1.95 +
    1.96  end;
    1.97  
    1.98  Addsimprocs [list_eq_simproc];
    1.99 @@ -1364,6 +1364,7 @@
   1.100                  drop_Cons'[of "number_of v",standard]
   1.101                  nth_Cons'[of _ _ "number_of v",standard]
   1.102  
   1.103 +
   1.104  subsection {* Characters and strings *}
   1.105  
   1.106  datatype nibble =