'a list: Nil, Cons;
authorwenzelm
Mon Aug 16 22:07:12 1999 +0200 (1999-08-16)
changeset 7224e41e64476f9b
parent 7223 b0198ca65867
child 7225 0a7c43c56092
'a list: Nil, Cons;
src/HOL/Lex/RegExp2NA.thy
src/HOL/Lex/RegExp2NAe.thy
src/HOL/List.ML
src/HOL/List.thy
src/HOL/String.thy
src/HOL/TLA/Intensional.thy
     1.1 --- a/src/HOL/Lex/RegExp2NA.thy	Mon Aug 16 22:04:07 1999 +0200
     1.2 +++ b/src/HOL/Lex/RegExp2NA.thy	Mon Aug 16 22:07:12 1999 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  types 'a bitsNA = ('a,bool list)na
     1.5  
     1.6  syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
     1.7 -translations "x ## S" == "op # x `` S"
     1.8 +translations "x ## S" == "Cons x `` S"
     1.9  
    1.10  constdefs
    1.11   atom  :: 'a => 'a bitsNA
     2.1 --- a/src/HOL/Lex/RegExp2NAe.thy	Mon Aug 16 22:04:07 1999 +0200
     2.2 +++ b/src/HOL/Lex/RegExp2NAe.thy	Mon Aug 16 22:07:12 1999 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  types 'a bitsNAe = ('a,bool list)nae
     2.5  
     2.6  syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
     2.7 -translations "x ## S" == "op # x `` S"
     2.8 +translations "x ## S" == "Cons x `` S"
     2.9  
    2.10  constdefs
    2.11   atom  :: 'a => 'a bitsNAe
     3.1 --- a/src/HOL/List.ML	Mon Aug 16 22:04:07 1999 +0200
     3.2 +++ b/src/HOL/List.ML	Mon Aug 16 22:07:12 1999 +0200
     3.3 @@ -253,18 +253,18 @@
     3.4  val list_eq_pattern =
     3.5    Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
     3.6  
     3.7 -fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
     3.8 -      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
     3.9 +fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    3.10 +      (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    3.11    | last (Const("List.op @",_) $ _ $ ys) = last ys
    3.12    | last t = t;
    3.13  
    3.14 -fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
    3.15 +fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
    3.16    | list1 _ = false;
    3.17  
    3.18 -fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
    3.19 -      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
    3.20 +fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
    3.21 +      (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
    3.22    | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    3.23 -  | butlast xs = Const("List.list.[]",fastype_of xs);
    3.24 +  | butlast xs = Const("List.list.Nil",fastype_of xs);
    3.25  
    3.26  val rearr_tac =
    3.27    simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
     4.1 --- a/src/HOL/List.thy	Mon Aug 16 22:04:07 1999 +0200
     4.2 +++ b/src/HOL/List.thy	Mon Aug 16 22:07:12 1999 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  
     4.5  List = Datatype + WF_Rel + NatBin +
     4.6  
     4.7 -datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
     4.8 +datatype 'a list = Nil ("[]") | Cons 'a ('a list) (infixr "#" 65)
     4.9  
    4.10  consts
    4.11    "@"         :: ['a list, 'a list] => 'a list            (infixr 65)
     5.1 --- a/src/HOL/String.thy	Mon Aug 16 22:04:07 1999 +0200
     5.2 +++ b/src/HOL/String.thy	Mon Aug 16 22:07:12 1999 +0200
     5.3 @@ -67,11 +67,11 @@
     5.4  
     5.5    (* strings *)
     5.6  
     5.7 -  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
     5.8 -    | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
     5.9 +  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
    5.10 +    | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
    5.11  
    5.12 -  fun dest_string (Const ("[]", _)) = []
    5.13 -    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
    5.14 +  fun dest_string (Const ("Nil", _)) = []
    5.15 +    | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
    5.16      | dest_string _ = raise Match;
    5.17  
    5.18  
    5.19 @@ -79,12 +79,12 @@
    5.20          mk_string (map mk_char (Syntax.explode_xstr xstr))
    5.21      | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    5.22  
    5.23 -  fun cons_tr' (*"op #"*) [c, cs] =
    5.24 +  fun cons_tr' (*"Cons"*) [c, cs] =
    5.25          Syntax.const "_String" $
    5.26            syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
    5.27 -    | cons_tr' (*"op #"*) ts = raise Match;
    5.28 +    | cons_tr' (*"Cons"*) ts = raise Match;
    5.29  
    5.30  in
    5.31    val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
    5.32 -  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
    5.33 +  val print_translation = [("Char", char_tr'), ("Cons", cons_tr')];
    5.34  end;
     6.1 --- a/src/HOL/TLA/Intensional.thy	Mon Aug 16 22:04:07 1999 +0200
     6.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Aug 16 22:07:12 1999 +0200
     6.3 @@ -130,7 +130,7 @@
     6.4    "_liftFinset x" == "_lift2 insert x (_const {})"
     6.5    "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
     6.6    "_liftPair"     == "_lift2 Pair"
     6.7 -  "_liftCons"     == "lift2 (op #)"
     6.8 +  "_liftCons"     == "lift2 Cons"
     6.9    "_liftApp"      == "lift2 (op @)"
    6.10    "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
    6.11    "_liftList x"   == "_liftCons x (_const [])"