src/HOL/datatype.ML
author nipkow
Mon, 09 Feb 1998 18:09:35 +0100
changeset 4613 67a726003cf8
parent 4545 4eadc8c2681b
child 4874 c66a42846887
permissions -rw-r--r--
Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(* Title:       HOL/datatype.ML
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
   ID:          $Id$
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
     3
   Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker,
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
     4
                Konrad Slind
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
   Copyright 1995 TU Muenchen
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
     8
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
     9
(** theory information about datatypes **)
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    10
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    11
fun datatype_info_sg sg name =
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    12
  (case Symtab.lookup (ThyData.get_datatypes_sg sg, name) of
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    13
    Some info => info
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    14
  | None => error ("Unknown datatype " ^ quote name));
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    15
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    16
val datatype_info = datatype_info_sg o sign_of;
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    17
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    18
fun match_info thy name =
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    19
  let val {case_const, constructors, ...} = datatype_info thy name in
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    20
    {case_const = case_const, constructors = constructors}
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    21
  end;
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    22
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    23
fun induct_info thy name =
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    24
  let val {constructors, nchotomy, ...} = datatype_info thy name in
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    25
    {constructors = constructors, nchotomy = nchotomy}
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    26
  end;
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    27
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    28
(*retrieve information for all datatypes defined in a theory*)
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    29
fun extract_info thy =
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    30
  let
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    31
    val infos = map snd (Symtab.dest (ThyData.get_datatypes thy));
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    32
    val (congs, rewrites) = (map #case_cong infos, flat (map #case_rewrites infos));
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    33
  in {case_congs = congs, case_rewrites = rewrites} end;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    34
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    35
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    36
local
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    37
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    38
fun find_tname var Bi =
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    39
  let val frees = map dest_Free (term_frees Bi)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    40
      val params = Logic.strip_params Bi;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    41
  in case assoc (frees@params, var) of
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    42
       None => error("No such variable in subgoal: " ^ quote var)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    43
     | Some(Type(tn,_)) => tn
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    44
     | _ => error("Cannot induct on type of " ^ quote var)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    45
  end;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    46
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    47
fun infer_tname state sign i aterm =
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    48
let val (_, _, Bi, _) = dest_state (state, i)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    49
    val params = Logic.strip_params Bi	        (*params of subgoal i*)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    50
    val params = rev(rename_wrt_term Bi params) (*as they are printed*)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    51
    val (types,sorts) = types_sorts state
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    52
    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    53
      | types'(ixn) = types ixn;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    54
    val (ct,_) = read_def_cterm (sign,types',sorts) [] false
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    55
                                (aterm,TVar(("",0),[]));
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    56
in case #T(rep_cterm ct) of
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    57
     Type(tn,_) => tn
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    58
   | _ => error("Cannot induct on type of " ^ quote aterm)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    59
end;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    60
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    61
in
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    62
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    63
(* generic induction tactic for datatypes *)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    64
fun induct_tac var i state = state |>
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    65
        let val (_, _, Bi, _) = dest_state (state, i)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    66
            val sign = #sign(rep_thm state)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    67
            val tn = find_tname var Bi
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    68
            val ind_tac = #induct_tac(datatype_info_sg sign tn)
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    69
        in ind_tac var i end;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    70
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    71
(* generic exhaustion tactic for datatypes *)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    72
fun exhaust_tac aterm i state = state |>
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    73
        let val sign = #sign(rep_thm state)
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    74
            val tn = infer_tname state sign i aterm
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
    75
            val exh_tac = #exhaust_tac(datatype_info_sg sign tn)
3615
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    76
        in exh_tac aterm i end;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    77
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    78
end;
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    79
e5322197cfea Moved some functions which used to be part of thy_data.ML
berghofe
parents: 3564
diff changeset
    80
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
(*used for constructor parameters*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
datatype dt_type = dtVar of string |
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
  dtTyp of dt_type list * string |
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
  dtRek of dt_type list * string;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
structure Datatype =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
struct
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    88
local 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    89
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    90
open ThyParse HOLogic;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    91
exception Impossible;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    92
exception RecError of string;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    93
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    94
val is_dtRek = (fn dtRek _ => true  |  _  => false);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    95
fun opt_parens s = if s = "" then "" else enclose "(" ")" s; 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    96
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    97
(* ----------------------------------------------------------------------- *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    98
(* Derivation of the primrec combinator application from the equations     *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    99
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   100
(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs  *) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   101
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   102
fun subst_apps (_,_) [] t = t
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   103
  | subst_apps (fname,rpos) pairs t =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   104
    let 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   105
    fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   106
      | subst (funct $ body) = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   107
        let val (f,b) = strip_comb (funct$body)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   108
        in 
3945
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   109
          if is_Const f andalso Sign.base_name (fst(dest_Const f)) = fname 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   110
            then 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   111
              let val (ls,rest) = (take(rpos,b), drop(rpos,b));
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   112
                val (xk,rs) = (hd rest,tl rest)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   113
                  handle LIST _ => raise RecError "not enough arguments \
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   114
                   \ in recursive application on rhs"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   115
              in 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   116
                (case assoc (pairs,xk) of 
1574
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1465
diff changeset
   117
                   None   => list_comb(f, map subst b)
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1465
diff changeset
   118
                 | Some U => list_comb(U, map subst (ls @ rs)))
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   119
              end
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   120
          else list_comb(f, map subst b)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   121
        end
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   122
      | subst(t) = t
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   123
    in subst t end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   124
  
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   125
(* abstract rhs *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   126
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   127
fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) =       
2270
d7513875b2b8 Replaced map...~~ by ListPair.map
paulson
parents: 2031
diff changeset
   128
  let val rargs = (map #1 o 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   129
                   (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   130
      val subs = map (fn (s,T) => (s,dummyT))
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   131
                   (rev(rename_wrt_term rhs rargs));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   132
      val subst_rhs = subst_apps (fname,rpos)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   133
                        (map Free rargs ~~ map Free subs) rhs;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   134
  in 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   135
      list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   136
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   137
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   138
(* parsing the prim rec equations *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   139
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   140
fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   141
                 = (lhs, rhs)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   142
   | dest_eq _ = raise RecError "not a proper equation"; 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   143
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   144
fun dest_rec eq = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   145
  let val (lhs,rhs) = dest_eq eq; 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   146
    val (name,args) = strip_comb lhs; 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   147
    val (ls',rest)  = take_prefix is_Free args; 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   148
    val (middle,rs') = take_suffix is_Free rest;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   149
    val rpos = length ls';
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   150
    val (c,cargs') = strip_comb (hd middle)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   151
      handle LIST "hd" => raise RecError "constructor missing";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   152
    val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   153
                         , map dest_Free rs')
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   154
      handle TERM ("dest_Free",_) => 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   155
          raise RecError "constructor has illegal argument in pattern";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   156
  in 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   157
    if length middle > 1 then 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   158
      raise RecError "more than one non-variable in pattern"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   159
    else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   160
      raise RecError "repeated variable name in pattern" 
3945
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   161
         else (Sign.base_name (fst(dest_Const name)) handle TERM _ => 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   162
               raise RecError "function is not declared as constant in theory"
3945
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   163
                 ,rpos,ls, Sign.base_name (fst(dest_Const c)),cargs,rs,rhs)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   164
  end; 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   165
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   166
(* check function specified for all constructors and sort function terms *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   167
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   168
fun check_and_sort (n,its) = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   169
  if length its = n 
4545
4eadc8c2681b eliminated make_ord;
wenzelm
parents: 4448
diff changeset
   170
    then map snd (Library.sort (int_ord o pairself #1) its)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   171
  else raise error "Primrec definition error:\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   172
   \Please give an equation for every constructor";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   173
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   174
(* translate rec equations into function arguments suitable for rec comb *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   175
(* theory parameter needed for printing error messages                   *) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   176
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   177
fun trans_recs _ _ [] = error("No primrec equations.")
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   178
  | trans_recs thy cs' (eq1::eqs) = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   179
    let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   180
      handle RecError s =>
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   181
        error("Primrec definition error: " ^ s ^ ":\n" 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   182
              ^ "   " ^ Sign.string_of_term (sign_of thy) eq1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   183
      val tcs = map (fn (_,c,T,_,_) => (c,T)) cs';  
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   184
      val cs = map fst tcs;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   185
      fun trans_recs' _ [] = []
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   186
        | trans_recs' cis (eq::eqs) = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   187
          let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   188
            val tc = assoc(tcs,c);
4188
1025a27b08f9 changed libraray function find to find_index_eq, currying it
oheimb
parents: 4184
diff changeset
   189
            val i = 1 + find_index_eq c cs;
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   190
          in
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   191
          if name <> name1 then 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   192
            raise RecError "function names inconsistent"
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   193
          else if rpos <> rpos1 then 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   194
            raise RecError "position of rec. argument inconsistent"
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   195
          else if i = 0 then 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   196
            raise RecError "illegal argument in pattern" 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   197
          else if i mem cis then
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   198
            raise RecError "constructor already occured as pattern "
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   199
               else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs))
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   200
                     :: trans_recs' (i::cis) eqs 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   201
          end
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   202
          handle RecError s =>
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   203
                error("Primrec definition error\n" ^ s ^ "\n" 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   204
                      ^ "   " ^ Sign.string_of_term (sign_of thy) eq);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   205
    in (  name1, ls1
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   206
        , check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   207
    end ;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   208
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   209
in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   210
  fun add_datatype (typevars, tname, cons_list') thy = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   211
    let
3308
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   212
      val dummy = require_thy thy "Arith" "datatype definitions";
2880
a0fde30aa126 Removed (Unit) in Prod.
nipkow
parents: 2270
diff changeset
   213
      
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   214
      fun typid(dtRek(_,id)) = id
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   215
        | typid(dtVar s) = implode (tl (explode s))
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   216
        | typid(dtTyp(_,id)) = id;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   217
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   218
      fun index_vnames(vn::vns,tab) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   219
            (case assoc(tab,vn) of
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   220
               None => if vn mem vns
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   221
                       then (vn^"1") :: index_vnames(vns,(vn,2)::tab)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   222
                       else vn :: index_vnames(vns,tab)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   223
             | Some(i) => (vn^(string_of_int i)) ::
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   224
                          index_vnames(vns,(vn,i+1)::tab))
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   225
        | index_vnames([],tab) = [];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   226
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   227
      fun mk_var_names types = index_vnames(map typid types,[]);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   228
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   229
      (*search for free type variables and convert recursive *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   230
      fun analyse_types (cons, types, syn) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   231
        let fun analyse(t as dtVar v) =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   232
                  if t mem typevars then t
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   233
                  else error ("Free type variable " ^ v ^ " on rhs.")
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   234
              | analyse(dtTyp(typl,s)) =
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   235
                  if tname <> s then dtTyp(analyses typl, s)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   236
                  else if typevars = typl then dtRek(typl, s)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   237
                       else error (s ^ " used in different ways")
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   238
              | analyse(dtRek _) = raise Impossible
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   239
            and analyses ts = map analyse ts;
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   240
        in (cons, Syntax.const_name cons syn, analyses types,
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   241
            mk_var_names types, syn)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   242
        end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   243
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   244
     (*test if all elements are recursive, i.e. if the type is empty*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   245
      
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   246
      fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   247
        not(forall (exists is_dtRek o #3) cs) orelse
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   248
        error("Empty datatype not allowed!");
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   249
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   250
      val cons_list = map analyse_types cons_list';
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   251
      val dummy = non_empty cons_list;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   252
      val num_of_cons = length cons_list;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   253
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   254
     (* Auxiliary functions to construct argument and equation lists *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   255
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   256
     (*generate 'var_n, ..., var_m'*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   257
      fun Args(var, delim, n, m) = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   258
        space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   259
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   260
      fun C_exp name vns = name ^ opt_parens(space_implode ") (" vns);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   261
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   262
     (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   263
      fun arg_eqs vns vns' =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   264
        let fun mkeq(x,x') = x ^ "=" ^ x'
2270
d7513875b2b8 Replaced map...~~ by ListPair.map
paulson
parents: 2031
diff changeset
   265
        in space_implode " & " (ListPair.map mkeq (vns,vns')) end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   266
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   267
     (*Pretty printers for type lists;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   268
       pp_typlist1: parentheses, pp_typlist2: brackets*)
1279
f59b4f9f2cdc All constants introduced by datatype now operate on class term explicitly.
nipkow
parents: 980
diff changeset
   269
      fun pp_typ (dtVar s) = "(" ^ s ^ "::term)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   270
        | pp_typ (dtTyp (typvars, id)) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   271
          if null typvars then id else (pp_typlist1 typvars) ^ id
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   272
        | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   273
      and
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   274
        pp_typlist' ts = commas (map pp_typ ts)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   275
      and
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   276
        pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   277
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   278
      fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   279
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   280
     (* Generate syntax translation for case rules *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   281
      fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   282
        let val arity = length vns;
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   283
          val body  = "z" ^ string_of_int(c_nr);
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   284
          val args1 = if arity=0 then ""
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   285
                      else " " ^ Args ("y", " ", y_nr, y_nr+arity-1);
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   286
          val args2 = if arity=0 then ""
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   287
                      else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   288
                        ^ ". ";
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   289
          val (rest1,rest2) = 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   290
            if null cs then ("","")
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   291
            else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   292
            in (" | " ^ h1, " " ^ h2) end;
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   293
        in (name ^ args1 ^ " => " ^ body ^ rest1,
964
5f690b184f91 fixed two severe bugs in calc_xrules and case_rule
clasohm
parents: 923
diff changeset
   294
            args2 ^ body ^ (if args2 = "" then "" else ")") ^ rest2)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   295
        end
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   296
        | calc_xrules _ _ [] = raise Impossible;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   297
      
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   298
      val xrules =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   299
        let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
3534
c245c88194ff renamed |-> <-| <-> to Parse/PrintRule;
wenzelm
parents: 3308
diff changeset
   300
        in [Syntax.ParsePrintRule (("logic", "case x of " ^ first_part),
2031
03a843f0f447 Ran expandshort
paulson
parents: 1897
diff changeset
   301
                        ("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   302
        end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   303
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   304
     (*type declarations for constructors*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   305
      fun const_type (id, _, typlist, _, syn) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   306
        (id,  
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   307
         (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   308
            pp_typlist1 typevars ^ tname, syn);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   309
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   310
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   311
      fun assumpt (dtRek _ :: ts, v :: vs ,found) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   312
        let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")"
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   313
        in h ^ (assumpt (ts, vs, true)) end
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   314
        | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   315
      | assumpt ([], [], found) = if found then "|] ==>" else ""
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   316
        | assumpt _ = raise Impossible;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   317
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   318
      fun t_inducting ((_, name, types, vns, _) :: cs) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   319
        let
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   320
          val h = if null types then " P(" ^ name ^ ")"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3792
diff changeset
   321
                  else " !!" ^ (space_implode " " vns) ^ ". " ^
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   322
                    (assumpt (types, vns, false)) ^
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   323
                    "P(" ^ C_exp name vns ^ ")";
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   324
          val rest = t_inducting cs;
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   325
        in if rest = "" then h else h ^ "; " ^ rest end
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   326
        | t_inducting [] = "";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   327
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   328
      fun t_induct cl typ_name =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   329
        "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   330
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   331
      fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   332
        let val h = if (length ts) > 0
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   333
                      then pp_typlist2(f ts) ^ "=>"
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   334
                    else ""
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   335
        in h ^ typevar ^  "," ^ (gen_typlist typevar f cs) end
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   336
        | gen_typlist _ _ [] = "";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   337
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   338
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   339
(* -------------------------------------------------------------------- *)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   340
(* The case constant and rules                                          *)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   341
                
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   342
      val t_case = tname ^ "_case";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   343
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   344
      fun case_rule n (id, name, _, vns, _) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   345
        let val args = if vns = [] then "" else " " ^ space_implode " " vns
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   346
        in (t_case ^ "_" ^ id,
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   347
            t_case ^ " " ^ Args("f", " ", 1, num_of_cons)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   348
            ^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   349
        end
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   350
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   351
      fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   352
        | case_rules _ [] = [];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   353
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   354
      val datatype_arity = length typevars;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   355
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   356
      val types = [(tname, datatype_arity, NoSyn)];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   357
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   358
      val arities = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   359
        let val term_list = replicate datatype_arity termS;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   360
        in [(tname, term_list, termS)] 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   361
        end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   362
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   363
      val datatype_name = pp_typlist1 typevars ^ tname;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   364
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   365
      val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   366
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   367
      val case_const =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   368
        (t_case,
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   369
         "[" ^ gen_typlist new_tvar_name I cons_list 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   370
         ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term",
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   371
         NoSyn);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   372
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   373
      val rules_case = case_rules 1 cons_list;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   374
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   375
(* -------------------------------------------------------------------- *)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   376
(* The prim-rec combinator                                              *) 
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   377
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   378
      val t_rec = tname ^ "_rec"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   379
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   380
(* adding type variables for dtRek types to end of list of dt_types      *)   
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   381
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   382
      fun add_reks ts = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   383
        ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   384
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   385
(* positions of the dtRek types in a list of dt_types, starting from 1  *)
2270
d7513875b2b8 Replaced map...~~ by ListPair.map
paulson
parents: 2031
diff changeset
   386
      fun rek_vars ts vns = map #2 (filter (is_dtRek o fst) (ts ~~ vns))
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   387
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   388
      fun rec_rule n (id,name,ts,vns,_) = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   389
        let val args = opt_parens(space_implode ") (" vns)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   390
          val fargs = opt_parens(Args("f", ") (", 1, num_of_cons))
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   391
          fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")"
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   392
          val rargs = opt_parens(space_implode ") ("
964
5f690b184f91 fixed two severe bugs in calc_xrules and case_rule
clasohm
parents: 923
diff changeset
   393
                                 (map rarg (rek_vars ts vns)))
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   394
        in
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   395
          (t_rec ^ "_" ^ id,
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   396
           t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f"
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   397
           ^ string_of_int(n) ^ args ^ rargs)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   398
        end
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   399
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   400
      fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   401
        | rec_rules _ [] = [];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   402
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   403
      val rec_const =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   404
        (t_rec,
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   405
         "[" ^ (gen_typlist new_tvar_name add_reks cons_list) 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   406
         ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term",
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   407
         NoSyn);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   408
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   409
      val rules_rec = rec_rules 1 cons_list
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   410
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   411
(* -------------------------------------------------------------------- *)
3308
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   412
(* The size function                                                    *) 
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   413
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   414
      fun size_eqn(_,name,types,vns,_) =
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   415
        let fun sum((T,vn)::args) =
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   416
                  if is_dtRek T then "size(" ^ vn ^ ") + " ^ sum(args)
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   417
                  else sum args
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   418
              | sum [] = "1"
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   419
            val rhs = if exists is_dtRek types then sum(types~~vns) else "0"
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   420
        in ("", "size(" ^ C_exp name vns ^ ") = " ^ rhs) end;
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   421
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   422
      val size_eqns  = map size_eqn cons_list;
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   423
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3292
diff changeset
   424
(* -------------------------------------------------------------------- *)
4032
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   425
(* The split equation                                                   *) 
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   426
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   427
      local
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   428
      val fs = map (fn i => "f"^(string_of_int i)) (1 upto num_of_cons);
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   429
4184
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   430
      fun split1case concl ((_,name,_,vns,_),fi) =
4032
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   431
        let val svns = " " ^ (space_implode " " vns);
4184
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   432
            val quant = if concl then "!" else "?";
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   433
            val impl = if concl then " --> " else " & ~";
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   434
            val all = if null vns then "" else quant ^ svns ^ ". "
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   435
        in "("^all^tname^"0 = "^C_exp name vns^impl^"P("^fi^svns^"))" end;
4032
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   436
4184
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   437
      fun rhss concl = map (split1case concl) (cons_list ~~ fs);
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   438
      fun rhs concl= space_implode(if concl then " & " else " | ")(rhss concl);
4032
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   439
      val lhs = "P(" ^ t_case ^ " " ^ (space_implode " " fs) ^" "^ tname^"0)"
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   440
      in
4184
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   441
      val split_eqn = lhs ^ " = (" ^ rhs true ^ ")"
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   442
      val split_eqn_prem = lhs ^ " = ( ~ (" ^ rhs false ^ "))"
4032
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   443
      end;
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   444
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   445
(* -------------------------------------------------------------------- *)
4b1c69d8b767 For each datatype `t' there is now a theorem `split_t_case' of the form
nipkow
parents: 3979
diff changeset
   446
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   447
      val consts = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   448
        map const_type cons_list
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   449
        @ (if num_of_cons < dtK then []
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   450
           else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   451
        @ [case_const,rec_const];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   452
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   453
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   454
      fun Ci_ing ((id, name, _, vns, _) :: cs) =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   455
           if null vns then Ci_ing cs
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   456
           else let val vns' = variantlist(vns,vns)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   457
                in ("inject_" ^ id,
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   458
                    "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns')
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   459
                    ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   460
                end
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   461
        | Ci_ing [] = [];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   462
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   463
      fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   464
            let val vns2' = variantlist(vns2,vns1)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   465
                val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2'
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   466
        in (id1 ^ "_not_" ^ id2, ax) end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   467
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   468
      fun Ci_neg1 [] = []
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   469
        | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   470
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   471
      fun suc_expr n = 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   472
        if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   473
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   474
      fun Ci_neg2() =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   475
        let val ord_t = tname ^ "_ord";
2270
d7513875b2b8 Replaced map...~~ by ListPair.map
paulson
parents: 2031
diff changeset
   476
          val cis = ListPair.zip (cons_list, 0 upto (num_of_cons - 1))
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   477
          fun Ci_neg2equals ((id, name, _, vns, _), n) =
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   478
            let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   479
            in (ord_t ^ "_" ^ id, ax) end
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   480
        in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   481
          (map Ci_neg2equals cis)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   482
        end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   483
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   484
      val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   485
                           else Ci_neg2();
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   486
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   487
      val rules_inject = Ci_ing cons_list;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   488
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   489
      val rule_induct = (tname ^ "_induct", t_induct cons_list tname);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   490
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   491
      val rules = rule_induct ::
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   492
        (rules_inject @ rules_distinct @ rules_case @ rules_rec);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   493
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   494
      fun add_primrec eqns thy =
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   495
        let val rec_comb = Const(t_rec,dummyT)
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   496
          val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   497
          val (fname,ls,fns) = trans_recs thy cons_list teqns
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   498
          val rhs = 
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   499
            list_abs_free
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   500
            (ls @ [(tname,dummyT)]
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   501
             ,list_comb(rec_comb
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   502
                        , fns @ map Bound (0 ::(length ls downto 1))));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   503
          val sg = sign_of thy;
1574
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1465
diff changeset
   504
          val defpair = (fname ^ "_" ^ tname ^ "_def",
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1465
diff changeset
   505
                         Logic.mk_equals (Const(fname,dummyT), rhs))
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   506
          val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   507
          val varT = Type.varifyT T;
3945
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   508
          val ftyp = the (Sign.const_type sg (Sign.intern_const sg fname));
4040
20f7471eedbf PureThy.add_store_defs_i, PureThy.add_store_axioms;
wenzelm
parents: 4032
diff changeset
   509
        in PureThy.add_store_defs_i [defpairT] thy end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   510
1360
6bdee79ef125 added call of store_datatype
clasohm
parents: 1279
diff changeset
   511
    in
3768
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 3615
diff changeset
   512
      (thy |> Theory.add_types types
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 3615
diff changeset
   513
           |> Theory.add_arities arities
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 3615
diff changeset
   514
           |> Theory.add_consts consts
67f4ac759100 fully qualified names: Theory.add_XXX;
wenzelm
parents: 3615
diff changeset
   515
           |> Theory.add_trrules xrules
4184
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   516
           |> PureThy.add_store_axioms rules,
23a09f2fd687 Each datatype t now proves a theorem split_t_case_prem
nipkow
parents: 4107
diff changeset
   517
       add_primrec, size_eqns, (split_eqn,split_eqn_prem))
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   518
    end
3040
7d48671753da Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents: 2880
diff changeset
   519
3564
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   520
(*Warn if the (induction) variable occurs Free among the premises, which
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   521
  usually signals a mistake.  But calls the tactic either way!*)
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   522
fun occs_in_prems tacf a = 
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   523
  SUBGOAL (fn (Bi,i) =>
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   524
	   (if  exists (fn Free(a',_) => a=a')
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   525
	              (foldr add_term_frees (#2 (strip_context Bi), []))
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   526
	     then warning "Induction variable occurs also among premises!"
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   527
	     else ();
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   528
	    tacf a i));
3040
7d48671753da Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents: 2880
diff changeset
   529
7d48671753da Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents: 2880
diff changeset
   530
end;
7d48671753da Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents: 2880
diff changeset
   531
7d48671753da Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents: 2880
diff changeset
   532
end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   533
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   534
(*
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   535
Informal description of functions used in datatype.ML for the Isabelle/HOL
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   536
implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   537
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   538
* subst_apps (fname,rpos) pairs t:
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   539
   substitute the term 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   540
       fname(ls,xk,rs) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   541
   by 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   542
      yk(ls,rs) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   543
   in t for (xk,yk) in pairs, where rpos = length ls. 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   544
   Applied with : 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   545
     fname = function name 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   546
     rpos = position of recursive argument 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   547
     pairs = list of pairs (xk,yk), where 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   548
          xk are the rec. arguments of the constructor in the pattern,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   549
          yk is a variable with name derived from xk 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   550
     t = rhs of equation 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   551
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   552
* abst_rec (fname,rpos,tc,ls,cargs,rs,rhs)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   553
  - filter recursive arguments from constructor arguments cargs,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   554
  - perform substitutions on rhs, 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   555
  - derive list subs of new variable names yk for use in subst_apps, 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   556
  - abstract rhs with respect to cargs, subs, ls and rs. 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   557
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   558
* dest_eq t 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   559
  destruct a term denoting an equation into lhs and rhs. 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   560
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   561
* dest_req eq 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   562
  destruct an equation of the form 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   563
      name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   564
  into 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   565
  - function name  (name) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   566
  - position of the first non-variable parameter  (rpos)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   567
  - the list of first rpos parameters (ls = [vl1..vlrpos]) 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   568
  - the constructor (fst( dest_Const c) = Ci)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   569
  - the arguments of the constructor (cargs = [vi1..vin])
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   570
  - the rest of the variables in the pattern (rs = [vr1..vrn])
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   571
  - the right hand side of the equation (rhs).  
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   572
 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   573
* check_and_sort (n,its)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   574
  check that  n = length its holds, and sort elements of its by 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   575
  first component. 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   576
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   577
* trans_recs thy cs' (eq1::eqs)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   578
  destruct eq1 into name1, rpos1, ls1, etc.. 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   579
  get constructor list with and without type (tcs resp. cs) from cs',  
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   580
  for every equation:  
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   581
    destruct it into (name,rpos,ls,c,cargs,rs,rhs)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   582
    get typed constructor tc from c and tcs 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   583
    determine the index i of the constructor 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   584
    check function name and position of rec. argument by comparison
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   585
    with first equation 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   586
    check for repeated variable names in pattern
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   587
    derive function term f_i which is used as argument of the rec. combinator
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   588
    sort the terms f_i according to i and return them together
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   589
      with the function name and the parameter of the definition (ls). 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   590
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   591
* Application:
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   592
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   593
  The rec. combinator is applied to the function terms resulting from
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   594
  trans_rec. This results in a function which takes the recursive arg. 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   595
  as first parameter and then the arguments corresponding to ls. The
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   596
  order of parameters is corrected by setting the rhs equal to 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   597
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   598
  list_abs_free
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   599
            (ls @ [(tname,dummyT)]
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   600
             ,list_comb(rec_comb
5d7a7e439cec expanded tabs
clasohm
parents: 1455
diff changeset
   601
                        , fns @ map Bound (0 ::(length ls downto 1))));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   602
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   603
  Note the de-Bruijn indices counting the number of lambdas between the
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   604
  variable and its binding. 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   605
*)
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   606
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   607
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   608
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   609
(* ----------------------------------------------- *)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   610
(* The following has been written by Konrad Slind. *)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   611
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   612
3040
7d48671753da Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents: 2880
diff changeset
   613
(* type dtype_info is defined in simpdata.ML *)
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   614
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   615
signature Dtype_sig =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   616
sig
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   617
  val build_case_cong: Sign.sg -> thm list -> cterm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   618
  val build_nchotomy: Sign.sg -> thm list -> cterm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   619
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   620
  val prove_case_cong: thm -> thm list -> cterm -> thm
1690
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   621
  val prove_nchotomy: (string -> int -> tactic) -> cterm -> thm
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   622
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   623
  val case_thms : Sign.sg -> thm list -> (string -> int -> tactic)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   624
                   -> {nchotomy:thm, case_cong:thm}
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   625
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   626
  val build_record: theory * (string * string list) * (string -> int -> tactic)
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   627
    -> string * datatype_info
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   628
  val add_record: string * string list * (string -> int -> tactic) -> theory -> theory
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   629
  val add_datatype_info: string * datatype_info -> theory -> theory
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   630
end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   631
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   632
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   633
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   634
 * This structure is support for the Isabelle datatype package. It provides
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   635
 * entrypoints for 1) building and proving the case congruence theorem for
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   636
 * a datatype and 2) building and proving the "exhaustion" theorem for
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   637
 * a datatype (I have called this theorem "nchotomy" for no good reason).
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   638
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   639
 * It also brings all these together in the function "build_record", which
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   640
 * is probably what will be used.
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   641
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   642
 * Since these routines are required in order to support TFL, they have
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   643
 * been written so they will compile "stand-alone", i.e., in Isabelle-HOL
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   644
 * without any TFL code around.
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   645
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   646
structure Dtype : Dtype_sig =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   647
struct
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   648
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   649
exception DTYPE_ERR of {func:string, mesg:string};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   650
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   651
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   652
 * General support routines
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   653
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   654
fun itlist f L base_value =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   655
   let fun it [] = base_value
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   656
         | it (a::rst) = f a (it rst)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   657
   in it L 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   658
   end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   659
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   660
fun end_itlist f =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   661
let fun endit [] = raise DTYPE_ERR{func="end_itlist", mesg="list too short"}
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   662
      | endit alist = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   663
         let val (base::ralist) = rev alist
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   664
         in itlist f (rev ralist) base  end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   665
in endit
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   666
end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   667
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   668
fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]);
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   669
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   670
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   671
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   672
 * Miscellaneous Syntax manipulation
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   673
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   674
val mk_var = Free;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   675
val mk_const = Const
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   676
fun mk_comb(Rator,Rand) = Rator $ Rand;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   677
fun mk_abs(r as (Var((s,_),ty),_))  = Abs(s,ty,abstract_over r)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   678
  | mk_abs(r as (Free(s,ty),_))     = Abs(s,ty,abstract_over r)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   679
  | mk_abs _ = raise DTYPE_ERR{func="mk_abs", mesg="1st not a variable"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   680
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   681
fun dest_var(Var((s,i),ty)) = (s,ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   682
  | dest_var(Free(s,ty))    = (s,ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   683
  | dest_var _ = raise DTYPE_ERR{func="dest_var", mesg="not a variable"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   684
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   685
fun dest_const(Const p) = p
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   686
  | dest_const _ = raise DTYPE_ERR{func="dest_const", mesg="not a constant"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   687
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   688
fun dest_comb(t1 $ t2) = (t1,t2)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   689
  | dest_comb _ =  raise DTYPE_ERR{func = "dest_comb", mesg = "not a comb"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   690
val rand = #2 o dest_comb;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   691
val rator = #1 o dest_comb;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   692
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   693
fun dest_abs(a as Abs(s,ty,M)) = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   694
     let val v = Free(s, ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   695
      in (v, betapply (a,v)) end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   696
  | dest_abs _ =  raise DTYPE_ERR{func="dest_abs", mesg="not an abstraction"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   697
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   698
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   699
val bool = Type("bool",[])
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   700
and prop = Type("prop",[]);
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   701
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   702
fun mk_eq(lhs,rhs) = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   703
   let val ty = type_of lhs
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   704
       val c = mk_const("op =", ty --> ty --> bool)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   705
   in list_comb(c,[lhs,rhs])
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   706
   end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   707
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   708
fun dest_eq(Const("op =",_) $ M $ N) = (M, N)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   709
  | dest_eq _ = raise DTYPE_ERR{func="dest_eq", mesg="not an equality"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   710
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   711
fun mk_disj(disj1,disj2) =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   712
   let val c = Const("op |", bool --> bool --> bool)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   713
   in list_comb(c,[disj1,disj2])
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   714
   end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   715
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   716
fun mk_forall (r as (Bvar,_)) = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   717
  let val ty = type_of Bvar
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   718
      val c = Const("All", (ty --> bool) --> bool)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   719
  in mk_comb(c, mk_abs r)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   720
  end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   721
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   722
fun mk_exists (r as (Bvar,_)) = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   723
  let val ty = type_of Bvar 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   724
      val c = Const("Ex", (ty --> bool) --> bool)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   725
  in mk_comb(c, mk_abs r)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   726
  end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   727
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   728
fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   729
  | mk_prop tm = mk_comb(Const("Trueprop", bool --> prop),tm);
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   730
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   731
fun drop_prop (Const("Trueprop",_) $ X) = X
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   732
  | drop_prop X = X;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   733
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   734
fun mk_all (r as (Bvar,_)) = mk_comb(all (type_of Bvar), mk_abs r);
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   735
fun list_mk_all(V,t) = itlist(fn v => fn b => mk_all(v,b)) V t;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   736
fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v,b)) V t;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   737
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1,tm))
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   738
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   739
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   740
fun dest_thm thm = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   741
   let val {prop,hyps,...} = rep_thm thm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   742
   in (map drop_prop hyps, drop_prop prop)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   743
   end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   744
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   745
val concl = #2 o dest_thm;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   746
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   747
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   748
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   749
 * Names of all variables occurring in a term, including bound ones. These
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   750
 * are added into the second argument.
3265
8358e19d0d4c Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents: 3197
diff changeset
   751
 *---------------------------------------------------------------------------
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   752
fun add_term_names tm =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   753
let fun insert (x:string) = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   754
     let fun canfind[] = [x] 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   755
           | canfind(alist as (y::rst)) = 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   756
              if (x<y) then x::alist
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   757
              else if (x=y) then y::rst
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   758
              else y::canfind rst 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   759
     in canfind end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   760
    fun add (Free(s,_)) V = insert s V
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   761
      | add (Var((s,_),_)) V = insert s V
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   762
      | add (Abs(s,_,body)) V = add body (insert s V)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   763
      | add (f$t) V = add t (add f V)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   764
      | add _ V = V
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   765
in add tm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   766
end;
3265
8358e19d0d4c Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents: 3197
diff changeset
   767
Why bound ones???
8358e19d0d4c Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents: 3197
diff changeset
   768
*)
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   769
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   770
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   771
 * We need to make everything free, so that we can put the term into a
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   772
 * goalstack, or submit it as an argument to prove_goalw_cterm.
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   773
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   774
fun make_free_ty(Type(s,alist)) = Type(s,map make_free_ty alist)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   775
  | make_free_ty(TVar((s,i),srt)) = TFree(s,srt)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   776
  | make_free_ty x = x;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   777
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   778
fun make_free (Var((s,_),ty)) = Free(s,make_free_ty ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   779
  | make_free (Abs(s,x,body)) = Abs(s,make_free_ty x, make_free body)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   780
  | make_free (f$t) = (make_free f $ make_free t)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   781
  | make_free (Const(s,ty)) = Const(s, make_free_ty ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   782
  | make_free (Free(s,ty)) = Free(s, make_free_ty ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   783
  | make_free b = b;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   784
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   785
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   786
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   787
 * Structure of case congruence theorem looks like this:
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   788
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   789
 *    (M = M') 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   790
 *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = f1' x1..xk)) 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   791
 *    ==> ... 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   792
 *    ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = fn' x1..xj)) 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   793
 *    ==>
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   794
 *      (ty_case f1..fn M = ty_case f1'..fn' m')
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   795
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   796
 * The input is the list of rules for the case construct for the type, i.e.,
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   797
 * that found in the "ty.cases" field of a theory where datatype "ty" is
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   798
 * defined.
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   799
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   800
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   801
fun build_case_cong sign case_rewrites =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   802
 let val clauses = map concl case_rewrites
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   803
     val clause1 = hd clauses
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   804
     val left = (#1 o dest_eq) clause1
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   805
     val ty = type_of ((#2 o dest_comb) left)
3265
8358e19d0d4c Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents: 3197
diff changeset
   806
     val varnames = foldr add_term_names (clauses, [])
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   807
     val M = variant varnames "M"
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   808
     val Mvar = Free(M, ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   809
     val M' = variant (M::varnames) M
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   810
     val M'var = Free(M', ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   811
     fun mk_clause clause =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   812
       let val (lhs,rhs) = dest_eq clause
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   813
           val func = (#1 o strip_comb) rhs
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   814
           val (constr,xbar) = strip_comb(rand lhs)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   815
           val (Name,Ty) = dest_var func
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   816
           val func'name = variant (M::M'::varnames) (Name^"a")
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   817
           val func' = mk_var(func'name,Ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   818
       in (func', list_mk_all
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   819
                  (xbar, Logic.mk_implies
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   820
                         (mk_prop(mk_eq(M'var, list_comb(constr,xbar))),
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   821
                          mk_prop(mk_eq(list_comb(func, xbar),
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   822
                                        list_comb(func',xbar))))))   end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   823
     val (funcs',clauses') = unzip (map mk_clause clauses)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   824
     val lhsM = mk_comb(rator left, Mvar)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   825
     val c = #1(strip_comb left)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   826
 in
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   827
 cterm_of sign
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   828
  (make_free
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   829
   (Logic.list_implies(mk_prop(mk_eq(Mvar, M'var))::clauses',
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   830
                       mk_prop(mk_eq(lhsM, list_comb(c,(funcs'@[M'var])))))))
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   831
 end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   832
 handle _ => raise DTYPE_ERR{func="build_case_cong",mesg="failed"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   833
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   834
  
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   835
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   836
 * Proves the result of "build_case_cong". 
1897
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   837
 * This one solves it a disjunct at a time, and builds the ss only once.
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   838
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   839
fun prove_case_cong nchotomy case_rewrites ctm =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   840
 let val {sign,t,...} = rep_cterm ctm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   841
     val (Const("==>",_) $ tm $ _) = t
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   842
     val (Const("Trueprop",_) $ (Const("op =",_) $ _ $ Ma)) = tm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   843
     val (Free(str,_)) = Ma
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   844
     val thm = prove_goalw_cterm[] ctm
1897
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   845
      (fn prems => 
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   846
        let val simplify = asm_simp_tac(HOL_ss addsimps (prems@case_rewrites))
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   847
        in [simp_tac (HOL_ss addsimps [hd prems]) 1,
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   848
            cut_inst_tac [("x",str)] (nchotomy RS spec) 1,
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   849
            REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   850
            REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
71e51870cc9a Replaced prove_case_cong by Konrad Slinds optimized version.
berghofe
parents: 1810
diff changeset
   851
        end) 
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   852
 in standard (thm RS eq_reflection)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   853
 end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   854
 handle _ => raise DTYPE_ERR{func="prove_case_cong",mesg="failed"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   855
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   856
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   857
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   858
 * Structure of exhaustion theorem looks like this:
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   859
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   860
 *    !v. (EX y1..yi. v = C1 y1..yi) | ... | (EX y1..yj. v = Cn y1..yj)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   861
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   862
 * As for "build_case_cong", the input is the list of rules for the case 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   863
 * construct (the case "rewrites").
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   864
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   865
fun build_nchotomy sign case_rewrites =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   866
 let val clauses = map concl case_rewrites
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   867
     val C_ybars = map (rand o #1 o dest_eq) clauses
3265
8358e19d0d4c Replaced Konrad's own add_term_names by the predefined one.
nipkow
parents: 3197
diff changeset
   868
     val varnames = foldr add_term_names (C_ybars, [])
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   869
     val vname = variant varnames "v"
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   870
     val ty = type_of (hd C_ybars)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   871
     val v = mk_var(vname,ty)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   872
     fun mk_disj C_ybar =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   873
       let val ybar = #2(strip_comb C_ybar)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   874
       in list_mk_exists(ybar, mk_eq(v,C_ybar))
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   875
       end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   876
 in
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   877
 cterm_of sign
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   878
   (make_free(mk_prop (mk_forall(v, list_mk_disj (map mk_disj C_ybars)))))
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   879
 end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   880
 handle _ => raise DTYPE_ERR{func="build_nchotomy",mesg="failed"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   881
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   882
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   883
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   884
 * Takes the induction tactic for the datatype, and the result from 
1690
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   885
 * "build_nchotomy" 
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   886
 *
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   887
 *    !v. (EX y1..yi. v = C1 y1..yi) | ... | (EX y1..yj. v = Cn y1..yj)
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   888
 *
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   889
 * and proves the theorem. The proof works along a diagonal: the nth 
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   890
 * disjunct in the nth subgoal is easy to solve. Thus this routine depends 
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   891
 * on the order of goals arising out of the application of the induction 
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   892
 * tactic. A more general solution would have to use injectiveness and 
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   893
 * distinctness rewrite rules.
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   894
 *---------------------------------------------------------------------------*)
1690
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   895
fun prove_nchotomy induct_tac ctm =
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   896
 let val (Const ("Trueprop",_) $ g) = #t(rep_cterm ctm)
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   897
     val (Const ("All",_) $ Abs (v,_,_)) = g
1690
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   898
     (* For goal i, select the correct disjunct to attack, then prove it *)
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   899
     fun tac i 0 = (rtac disjI1 i ORELSE all_tac) THEN
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   900
                   REPEAT (rtac exI i) THEN (rtac refl i)
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   901
       | tac i n = rtac disjI2 i THEN tac i (n-1)
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   902
 in 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   903
 prove_goalw_cterm[] ctm
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   904
     (fn _ => [rtac allI 1,
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   905
               induct_tac v 1,
1690
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   906
               ALLGOALS (fn i => tac i (i-1))])
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   907
 end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   908
 handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"};
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   909
3282
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   910
(*---------------------------------------------------------------------------
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   911
 * Turn nchotomy into exhaustion:
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   912
 *    [| !!y1..yi. v = C1 y1..yi ==> P; ...; !!y1..yj. v = Cn y1..yj ==> P |]
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   913
 *    ==> P
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   914
 *---------------------------------------------------------------------------*)
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   915
fun mk_exhaust nchotomy =
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   916
  let val tac = rtac impI 1 THEN
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   917
                REPEAT(SOMEGOAL(eresolve_tac [disjE,exE]))
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   918
  in standard(rule_by_tactic tac (nchotomy RS spec RS rev_mp)) end;
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   919
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   920
(* find name of v in exhaustion: *)
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   921
fun exhaust_var thm =
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   922
  let val _ $ ( _ $ Var((x,_),_) $ _ ) =
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   923
        hd(Logic.strip_assums_hyp(hd(prems_of thm)))
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   924
  in x end;
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   925
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   926
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   927
 * Brings the preceeding functions together.
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   928
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   929
fun case_thms sign case_rewrites induct_tac =
1690
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   930
  let val nchotomy = prove_nchotomy induct_tac
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   931
                                    (build_nchotomy sign case_rewrites)
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   932
      val cong = prove_case_cong nchotomy case_rewrites
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   933
                                 (build_case_cong sign case_rewrites)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   934
  in {nchotomy=nchotomy, case_cong=cong}
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   935
  end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   936
1690
e0ff33a33fa5 added changes by Konrad to prove_nchotomy
clasohm
parents: 1668
diff changeset
   937
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   938
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   939
 * Tests
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   940
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   941
 * 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   942
     Dtype.case_thms (sign_of List.thy) List.list.cases List.list.induct_tac;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   943
     Dtype.case_thms (sign_of Prod.thy) [split] 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   944
                     (fn s => res_inst_tac [("p",s)] PairE_lemma);
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   945
     Dtype.case_thms (sign_of Nat.thy) [nat_case_0, nat_case_Suc] nat_ind_tac;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   946
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   947
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   948
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   949
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   950
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   951
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   952
 * Given a theory and the name (and constructors) of a datatype declared in 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   953
 * an ancestor of that theory and an induction tactic for that datatype, 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   954
 * return the information that TFL needs. This should only be called once for
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   955
 * a datatype, because "build_record" proves various facts, and thus is slow. 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   956
 * It fails on the datatype of pairs, which must be included for TFL to work. 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   957
 * The test shows how to  build the record for pairs.
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   958
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   959
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   960
local fun mk_rw th = (th RS eq_reflection) handle _ => th
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   961
      fun get_fact thy s = (get_axiom thy s handle _ => get_thm thy s)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   962
in
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   963
fun build_record (thy,(ty,cl),itac) =
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   964
 let val sign = sign_of thy
3945
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   965
     val intern_const = Sign.intern_const sign;
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   966
     fun const s =
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   967
       let val s' = intern_const s
ae9c61d69888 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   968
       in Const(s', the (Sign.const_type sign s')) end
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   969
     val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   970
     val {nchotomy,case_cong} = case_thms sign case_rewrites itac
3282
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   971
     val exhaustion = mk_exhaust nchotomy
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   972
     val exh_var = exhaust_var exhaustion;
4613
67a726003cf8 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
nipkow
parents: 4545
diff changeset
   973
     fun exhaust_tac a =  (res_inst_tac [(exh_var,a)] exhaustion)
67a726003cf8 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
nipkow
parents: 4545
diff changeset
   974
                          THEN_ALL_NEW (rotate_tac ~1);
3564
f886dbd91ee5 Now Datatype.occs_in_prems prints the necessary warning ITSELF.
paulson
parents: 3538
diff changeset
   975
     val induct_tac = Datatype.occs_in_prems itac 
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   976
 in
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   977
  (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   978
        case_const = const (ty^"_case"),
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   979
        case_rewrites = map mk_rw case_rewrites,
3040
7d48671753da Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents: 2880
diff changeset
   980
        induct_tac = induct_tac,
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   981
        nchotomy = nchotomy,
3282
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   982
        exhaustion = exhaustion,
c31e6239d4c9 Added exhaustion thm and exhaust_tac for each datatype.
nipkow
parents: 3265
diff changeset
   983
        exhaust_tac = exhaust_tac,
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   984
        case_cong = case_cong})
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   985
 end
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   986
end;
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   987
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   988
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   989
fun add_datatype_info info thy = thy |>
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   990
  ThyData.put_datatypes (Symtab.update (info, ThyData.get_datatypes thy));
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   991
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   992
fun add_record (ty, cl, itac) thy = thy |>
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   993
  add_datatype_info (build_record (thy, (ty, cl), itac));
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   994
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   995
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   996
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 4040
diff changeset
   997
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   998
(*---------------------------------------------------------------------------
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   999
 * Test
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1000
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1001
 * 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1002
    map Dtype.build_record 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1003
          [(Nat.thy, ("nat",["0", "Suc"]), nat_ind_tac),
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1004
           (List.thy,("list",["[]", "#"]), List.list.induct_tac)]
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1005
    @
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1006
    [let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1007
                                 (fn s => res_inst_tac [("p",s)] PairE_lemma)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1008
         fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1009
     in ("*", 
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1010
         {constructors = [const "Pair"],
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1011
            case_const = const "split",
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1012
         case_rewrites = [split RS eq_reflection],
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1013
             case_cong = #case_cong prod_case_thms,
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1014
              nchotomy = #nchotomy prod_case_thms}) end];
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1015
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1016
 *
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1017
 *---------------------------------------------------------------------------*)
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1018
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
  1019
end;