Datatype.ML
author lcp
Fri, 17 Jun 1994 18:34:12 +0200
changeset 85 33d50643dccc
parent 80 d3d727449d7b
child 87 b0ea0e55dfe8
permissions -rw-r--r--
HOL/Arith/add_left_commute: tidied HOL/Arith/add_mult_distrib: DELETED DUPLICATE COPY
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
     1
(*  Title:       HOL/Datatype
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
     2
    ID:          $Id$
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
     3
    Author:      Max Breitling / Carsten Clasohm
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
     4
    Copyright    1994 TU Muenchen
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
     5
*)
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
     6
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
     7
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
     8
(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
     9
val dtK = 5;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    10
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    11
local open ThyParse in
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    12
val datatype_decls =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    13
  let fun cat s1 s2 = s1 ^ " " ^ s2;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    14
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    15
      val pars = parents "(" ")";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    16
      val brackets = parents "[" "]";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    17
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    18
      val mk_list = brackets o commas;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    19
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    20
      val tvar = type_var >> cat "dtVar";
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
    21
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    22
      val type_var_list = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    23
        tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    24
    
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    25
      val typ =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    26
         ident                  >> (cat "dtId" o quote)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    27
        ||
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    28
         type_var_list -- ident >> (fn (ts, id) => "Comp (" ^ mk_list ts ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    29
  				  ", " ^ quote id ^ ")")
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    30
        ||
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    31
         tvar;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    32
    
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    33
      val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    34
  
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    35
      val cons = name -- typ_list;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    36
  
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    37
      fun constructs ts =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    38
        ( cons --$$ "|" -- constructs >> op::
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    39
         ||
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    40
          cons                        >> (fn c => [c])) ts;  
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    41
  
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    42
      val mk_cons = map (fn (s, ts) => pars (s ^ ", " ^ mk_list ts));
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    43
  
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    44
      (*remove all quotes from a string*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    45
      fun rem_quotes s = implode (filter (fn c => c <> "\"") (explode s));
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    46
            
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    47
      (*generate names of ineq axioms*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    48
      fun rules_ineq cs tname = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    49
        let (*combine all constructor names with all others w/o duplicates*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    50
            fun negOne _ [] = [] 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    51
              | negOne (c : string * 'b) ((c2 : string * 'b) :: cs) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    52
                  quote ("ineq_" ^ rem_quotes (#1 c) ^ "_" ^ 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    53
                  rem_quotes (#1 c2)) :: negOne c cs;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    54
  
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    55
            fun neg1 [] = []
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    56
              | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    57
        in if length cs < dtK then neg1 cs
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    58
           else map (fn n => quote (tname ^ "_ord" ^ string_of_int n)) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    59
                    (0 upto (length cs))
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    60
        end;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    61
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    62
      fun arg1 (id, ts) = not (null ts);
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    63
          
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    64
      (*generate string calling 'add_datatype'*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    65
      fun mk_params ((ts, tname), cons) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    66
       ("|> add_datatype\n" ^ 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    67
       pars (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]),
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    68
       "structure " ^ tname ^ " =\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    69
       \struct\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    70
       \  val inject = map (get_axiom thy) " ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    71
         mk_list (map (fn (s,_) => quote ("inject_" ^ rem_quotes s)) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    72
                      (filter arg1 cons)) ^ ";\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    73
       \  val ineq = " ^ (if length cons < dtK then "let val ineq' = " else "")
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    74
         ^ "map (get_axiom thy) " ^ mk_list (rules_ineq cons tname) ^ 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    75
         (if length cons < dtK then 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    76
           "  in ineq' @ (map (fn t => sym COMP (t RS contrapos)) ineq') end"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    77
          else "") ^ ";\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    78
       \  val induct = get_axiom thy \"induct\";\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    79
       \  val cases = map (get_axiom thy) " ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    80
         mk_list (map (fn (s,_) => quote (tname ^ "_case_" ^ rem_quotes s)) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    81
                      cons) ^ ";\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    82
       \  val simps = inject @ ineq @ cases;\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    83
       \  fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    84
       \end;\n");
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    85
  in (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params end
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
    86
end;
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
    87
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    88
(*used for constructor parameters*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    89
datatype dt_type = dtVar of string |
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    90
                   dtId  of string |
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    91
                   Comp of dt_type list * string |
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    92
                   Rek of dt_type list * string;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
    93
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
    94
exception Impossible;
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
    95
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    96
local open Syntax.Mixfix in
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    97
fun add_datatype (typevars, tname, cons_list') thy = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
    98
  let fun cat s1 s2 = s1 ^ " " ^ s2;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
    99
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   100
      val pars = parents "(" ")";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   101
      val brackets = parents "[" "]";
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   102
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   103
      val mk_list = brackets o commas;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   104
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   105
      (*check if constructor names are unique*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   106
      fun check_cons cs =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   107
        (case findrep (map fst cs) of
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   108
           [] => true
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   109
         | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice"));
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   110
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   111
      (*search for free type variables and convert recursive *)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   112
      fun analyse ((cons, typlist) :: cs) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   113
            let fun analyseOne ((dtVar v) :: typlist) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   114
                     if ((dtVar v) mem typevars) then
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   115
                       (dtVar v) :: analyseOne typlist
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   116
                     else error ("Variable " ^ v ^ " is free.")
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   117
                  | analyseOne ((dtId s) :: typlist) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   118
                     if tname<>s then (dtId s) :: analyseOne typlist
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   119
                     else if null typevars then 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   120
                       Rek ([], tname) :: analyseOne typlist
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   121
                     else error (s ^ " used in different ways")
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   122
                  | analyseOne (Comp (typl,s) :: typlist) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   123
                     if tname <> s then Comp (analyseOne typl, s)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   124
                                     :: analyseOne typlist
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   125
                     else if typevars = typl then
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   126
                       Rek (typl, s) :: analyseOne typlist
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   127
                     else 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   128
                       error (s ^ " used in different ways")
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   129
                  | analyseOne [] = []
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   130
                  | analyseOne ((Rek _) :: _) = raise Impossible;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   131
            in (cons, analyseOne typlist) :: analyse cs end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   132
        | analyse [] = [];
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   133
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   134
      (*test if there are elements that are not recursive, i.e. if the type is
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   135
        not empty*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   136
      fun one_not_rek cs = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   137
        let val contains_no_rek = forall (fn Rek _ => false | _ => true);
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   138
        in exists (contains_no_rek o snd) cs orelse
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   139
           error("Empty type not allowed!") end;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   140
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   141
      val _ = check_cons cons_list';
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   142
      val cons_list = analyse cons_list';
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   143
      val _ = one_not_rek cons_list;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   144
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   145
      (*Pretty printers for type lists;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   146
        pp_typlist1: parentheses, pp_typlist2: brackets*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   147
      fun pp_typ (dtVar s) = s
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   148
        | pp_typ (dtId s) = s
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   149
        | pp_typ (Comp (typvars, id)) = (pp_typlist1 typvars) ^ id
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   150
        | pp_typ (Rek (typvars, id)) = (pp_typlist1 typvars) ^ id
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   151
      and
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   152
          pp_typlist' ts = commas (map pp_typ ts)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   153
      and
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   154
          pp_typlist1 ts = if null ts then "" else pars (pp_typlist' ts);
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   155
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   156
      fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   157
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   158
      fun Args(var, delim, n, m) = if n = m then var ^ string_of_int(n) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   159
                                   else var ^ string_of_int(n) ^ delim ^ 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   160
			    	        Args(var, delim, n+1, m);
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   161
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   162
      (* Generate syntax translation for case rules *)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   163
      fun calc_xrules c_nr y_nr ((c, typlist) :: cs) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   164
            let val arity = length typlist;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   165
                val body  = "z" ^ string_of_int(c_nr);
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   166
                val args1 = if arity=0 then ""
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   167
                            else pars (Args ("y", ",", y_nr, y_nr+arity-1));
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   168
                val args2 = if arity=0 then ""
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   169
                            else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   170
                            ^ ". ";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   171
                val (rest1,rest2) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   172
		  if null cs then ("", "")
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   173
                  else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   174
                       in (" | " ^ h1, ", " ^ h2) end;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   175
            in (c ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   176
        | calc_xrules _ _ [] = raise Impossible;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   177
      
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   178
      val xrules =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   179
         let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   180
         in  [("logic", "case x of " ^ first_part) <->
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   181
              ("logic", tname ^ "_case(x, " ^ scnd_part ^ ")" )]
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   182
         end;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   183
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   184
      (*type declarations for constructors*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   185
      fun const_types ((c, typlist) :: cs) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   186
           (c,  
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   187
            (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   188
             pp_typlist1 typevars ^ tname, NoSyn)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   189
           :: const_types cs
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   190
        | const_types [] = [];
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   191
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   192
      fun create_typevar (dtVar s) typlist =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   193
            if (dtVar s) mem typlist then 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   194
	      create_typevar (dtVar (s ^ "'")) typlist 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   195
            else s
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   196
        | create_typevar _ _ = raise Impossible;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   197
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   198
      fun assumpt (Rek _ :: ts, v :: vs ,found) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   199
            let val h = if found then ";P(" ^ v ^ ")"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   200
                                 else "[| P(" ^ v ^ ")"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   201
            in h ^ (assumpt (ts, vs, true)) end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   202
        | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   203
        | assumpt ([], [], found) = if found then "|] ==>" else ""
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   204
        | assumpt _ = raise Impossible;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   205
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   206
      (*insert type with suggested name 'varname' into table*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   207
      fun insert typ varname ((t, s, n) :: xs) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   208
            if typ = t then (t, s, n+1) :: xs
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   209
            else if varname = s then (t,s,n) :: (insert typ (varname ^ "'") xs)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   210
                                else (t,s,n) :: (insert typ varname xs)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   211
        | insert typ varname [] = [(typ, varname, 1)];
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   212
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   213
      fun insert_types (Rek (l,id) :: ts) tab =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   214
            insert_types ts (insert (Rek(l,id)) id tab)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   215
        | insert_types ((dtVar s) :: ts) tab =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   216
            insert_types ts (insert (dtVar s) (implode (tl (explode s))) tab)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   217
        | insert_types ((dtId s) :: ts) tab =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   218
            insert_types ts (insert (dtId s) s tab)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   219
        | insert_types (Comp (l,id) :: ts) tab =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   220
            insert_types ts (insert (Comp(l,id)) id tab)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   221
        | insert_types [] tab = tab;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   222
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   223
      fun update(Rek _, s, v :: vs, (Rek _) :: ts) = s :: vs
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   224
        | update(t, s, v :: vs, t1 :: ts) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   225
            if t=t1 then s :: vs
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   226
                    else v :: (update (t, s, vs, ts))
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   227
        | update _ = raise Impossible;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   228
      
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   229
      fun update_n (Rek r1, s, v :: vs, (Rek r2) :: ts, n) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   230
            if r1 = r2 then (s ^ string_of_int n) :: 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   231
                            (update_n (Rek r1, s, vs, ts, n+1))
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   232
                       else v :: (update_n (Rek r1, s, vs, ts, n))
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   233
        | update_n (t, s, v :: vs, t1 :: ts, n) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   234
            if t = t1 then (s ^ string_of_int n) :: 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   235
                           (update_n (t, s, vs, ts, n+1))
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   236
                      else v :: (update_n (t, s, vs, ts, n))
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   237
        | update_n (_,_,[],[],_) = []
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   238
        | update_n _ = raise Impossible;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   239
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   240
      (*insert type variables into table*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   241
      fun convert ((t, s, n) :: ts) var_list typ_list =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   242
            let val h = if n=1 then update (t, s, var_list, typ_list)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   243
                               else update_n (t, s, var_list, typ_list, 1)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   244
            in convert ts h typ_list end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   245
        | convert [] var_list _ = var_list;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   246
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   247
      fun empty_list n = replicate n "";
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   248
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   249
      fun t_inducting ((name, typl) :: cs) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   250
            let val tab = insert_types typl [];
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   251
                val arity = length typl;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   252
                val var_list = convert tab (empty_list arity) typl; 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   253
                val h = if arity = 0 then " P(" ^ name ^ ")"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   254
                        else " !!" ^ (space_implode " " var_list) ^ "." ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   255
                             (assumpt (typl, var_list, false)) ^ "P(" ^ 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   256
                             name ^ "(" ^ (commas var_list) ^ "))";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   257
                val rest = t_inducting cs;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   258
            in if rest="" then h else h ^ "; " ^ rest end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   259
        | t_inducting [] = "";
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   260
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   261
      fun t_induct cl typ_name=
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   262
        "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   263
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   264
      fun case_typlist typevar ((c, typlist) :: cs) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   265
           let val h = if (length typlist) > 0 then 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   266
		         (pp_typlist2 typlist) ^ "=>"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   267
                       else ""
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   268
           in "," ^ h ^ typevar ^ (case_typlist typevar cs) end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   269
        | case_typlist _ [] = "";
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   270
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   271
      fun case_rules t_case arity n ((id, typlist) :: cs) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   272
            let val args = if null typlist then ""
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   273
  			   else "(" ^ Args ("x", ",", 1, length typlist) ^ ")"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   274
            in (t_case ^ "_" ^ id,
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   275
                t_case ^ "(" ^ id ^ args ^ "," ^ Args ("f", ",", 1, arity) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   276
                ^ ") = f" ^ string_of_int(n) ^ args)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   277
               :: (case_rules t_case arity (n+1) cs)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   278
            end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   279
        | case_rules _ _ _ [] = [];
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   280
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   281
      val datatype_arity = length typevars;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   282
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   283
      val sign = sign_of thy;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   284
      val {tsig, ...} = Sign.rep_sg sign;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   285
            
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   286
      val types =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   287
        let val {args, ...} = Type.rep_tsig tsig;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   288
        in case assoc (args, tname) of
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   289
             None => [(tname, datatype_arity, NoSyn)]
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   290
           | Some _ => []
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   291
        end;
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   292
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   293
      val arities = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   294
        let val {coreg, ...} = Type.rep_tsig tsig;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   295
            val term_list = replicate datatype_arity ["term"];
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   296
        in case assoc (coreg, tname) of
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   297
             None => [(tname, term_list, ["term"])]
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   298
           | Some _ => []
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   299
        end;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   300
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   301
      val datatype_name = pp_typlist1 typevars ^ tname;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   302
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   303
      val (case_const, rules_case) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   304
         let val typevar = create_typevar (dtVar "'beta") typevars;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   305
             val t_case = tname ^ "_case";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   306
             val arity = length cons_list;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   307
             val dekl = (t_case, "[" ^ pp_typlist1 typevars ^ tname ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   308
                       case_typlist typevar cons_list ^ "]=>" ^ typevar, NoSyn)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   309
                       :: nil;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   310
             val rules = case_rules t_case arity 1 cons_list;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   311
         in (dekl, rules) end;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   312
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   313
      val consts = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   314
        let val {const_tab, ...} = Sign.rep_sg sign;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   315
            fun const_undef (c, _, _) = case Symtab.lookup (const_tab, c) of
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   316
                Some _ => false
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   317
              | None => true;
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   318
        in (filter const_undef (const_types cons_list)) @
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   319
	   (if length cons_list < dtK then []
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   320
	   else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   321
	   @ case_const
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   322
        end;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   323
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   324
      (*generate 'var_n, ..., var_m'*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   325
      fun Args(var, delim, n, m) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   326
        space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   327
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   328
      (*generate 'name_1', ..., 'name_n'*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   329
      fun C_exp(name, n, var) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   330
        if n > 0 then name ^ "(" ^ Args (var, ",", 1, n) ^ ")"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   331
                 else name;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   332
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   333
      (*generate 'x_n = y_n, ..., x_m = y_m'*)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   334
      fun Arg_eql(n,m) = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   335
        if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   336
        else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   337
             Arg_eql(n+1, m);
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   338
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   339
      fun Ci_ing (c :: cs) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   340
            let val (name, typlist) = c
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   341
                val arity = length typlist
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   342
            in if arity>0 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   343
               then ("inject_" ^ name,
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   344
                     "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   345
                     ^ ") = (" ^ Arg_eql(1,arity) ^ ")") :: (Ci_ing cs)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   346
               else (Ci_ing cs)      
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   347
            end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   348
        | Ci_ing [] = [];
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   349
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   350
      fun Ci_negOne _ [] = []
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   351
        | Ci_negOne c (c1::cs) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   352
           let val (name1, tl1) = c
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   353
               val (name2, tl2) = c1
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   354
               val arit1 = length tl1
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   355
               val arit2 = length tl2
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   356
               val h = "(" ^ C_exp(name1, arit1, "x") ^ "~=" ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   357
                             C_exp(name2, arit2, "y") ^ ")"
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   358
           in ("ineq_" ^ name1 ^ "_" ^ name2, h):: (Ci_negOne c cs) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   359
	   end;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   360
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   361
      fun Ci_neg1 [] = []
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   362
        | Ci_neg1 (c1::cs) = Ci_negOne c1 cs @ Ci_neg1 cs;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   363
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   364
      fun suc_expr n = 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   365
        if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   366
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   367
      fun Ci_neg2equals (ord_t, ((c, typlist) :: cs), n) =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   368
          let val h = ord_t ^ "(" ^ (C_exp(c, length typlist, "x")) ^ ") = " ^
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   369
                      (suc_expr n)
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   370
          in (ord_t ^ (string_of_int(n+1)), h) 
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   371
             :: (Ci_neg2equals (ord_t, cs , n+1))
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   372
          end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   373
        | Ci_neg2equals (_, [], _) = [];
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   374
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   375
      val Ci_neg2 =
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   376
        let val ord_t = tname ^ "_ord";
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   377
        in (Ci_neg2equals (ord_t, cons_list, 0)) @
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   378
           [(ord_t^"0",
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   379
            "(" ^ ord_t ^ "(x) ~= " ^ ord_t ^ "(y)) ==> (x ~= y)")]
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   380
        end;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   381
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   382
      val rules_ineq = if length cons_list < dtK then Ci_neg1 cons_list
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   383
                                                 else Ci_neg2;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   384
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   385
      val rules_inject = Ci_ing cons_list;
53
5e0570ea8b70 ML-like datatype decalaration facility. Axiomatic.
nipkow
parents:
diff changeset
   386
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   387
      val rule_induct = ("induct", t_induct cons_list tname);
60
43e36c15a831 new field "simps" added
nipkow
parents: 53
diff changeset
   388
80
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   389
      val rules =rule_induct :: (rules_inject @ rules_ineq @ rules_case);
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   390
  in thy
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   391
     |> add_types types
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   392
     |> add_arities arities
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   393
     |> add_consts consts
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   394
     |> add_trrules xrules
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   395
     |> add_axioms rules
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   396
  end
d3d727449d7b datatypes must now be defined using a thy file section
clasohm
parents: 60
diff changeset
   397
end;