src/ZF/constructor.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 3925 90f499226ab9
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
     1
(*  Title:      ZF/constructor.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
     6
Constructor function module -- for (Co)Datatype Definitions
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
     9
signature CONSTRUCTOR_ARG =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  sig
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    11
  val thy          : theory             (*parent containing constructor defs*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    12
  val big_rec_name : string             (*name of mutually recursive set*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    13
  val con_ty_lists : ((string*typ*mixfix) * 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    14
                      string * term list * term list) list list
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    15
                                        (*description of constructors*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
signature CONSTRUCTOR_RESULT =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  sig
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    20
  val con_defs   : thm list             (*definitions made in thy*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    21
  val case_eqns  : thm list             (*equations for case operator*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    22
  val free_iffs  : thm list             (*freeness rewrite rules*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    23
  val free_SEs   : thm list             (*freeness destruct rules*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    24
  val mk_free    : string -> thm        (*makes freeness theorems*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    28
(*Proves theorems relating to constructors*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    29
functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
                      Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    31
let
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    33
(*1st element is the case definition; others are the constructors*)
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    34
val big_case_name = Const.big_rec_name ^ "_case";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    36
val con_defs = get_def Const.thy big_case_name :: 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    37
               map (get_def Const.thy o #2) (flat Const.con_ty_lists);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
(** Prove the case theorem **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    41
(*Get the case term from its definition*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    42
val Const("==",_) $ big_case_tm $ _ =
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    43
    hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    44
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    45
val (_, big_case_args) = strip_comb big_case_tm;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    46
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(*Each equation has the form 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    49
fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = 
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    50
    Ind_Syntax.mk_tprop
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    51
      (Ind_Syntax.eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    52
       $ (list_comb (case_free, args))) ;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    54
val case_trans = hd con_defs RS Ind_Syntax.def_trans
1103
08fda5148971 prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents: 543
diff changeset
    55
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    57
(*Proves a single case equation.  Could use simp_tac, but it's slower!*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
fun case_tacsf con_def _ = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  [rewtac con_def,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
   rtac case_trans 1,
1103
08fda5148971 prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents: 543
diff changeset
    61
   REPEAT (resolve_tac [refl, split_trans, 
08fda5148971 prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents: 543
diff changeset
    62
                        Su.case_inl RS trans, 
08fda5148971 prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents: 543
diff changeset
    63
                        Su.case_inr RS trans] 1)];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
fun prove_case_equation (arg,con_def) =
543
e961b2092869 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents: 516
diff changeset
    66
    prove_goalw_cterm [] 
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    67
        (cterm_of (sign_of Const.thy) (mk_case_equation arg))
1103
08fda5148971 prove_case_equation now calls uses meta_eq_to_obj_eq to cope
lcp
parents: 543
diff changeset
    68
        (case_tacsf con_def);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    70
val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    71
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    72
in
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    73
  struct
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    74
  val con_defs = con_defs
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    75
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    76
  val free_iffs = con_iffs @ 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    79
  val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    81
  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    82
    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    83
  fun mk_free s =
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    84
      prove_goalw Const.thy con_defs s
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    85
        (fn prems => [cut_facts_tac prems 1, 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    86
                      fast_tac (ZF_cs addSEs free_SEs) 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    88
  val case_eqns = map prove_case_equation 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    89
              (flat Const.con_ty_lists ~~ big_case_args ~~ tl con_defs);
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1103
diff changeset
    90
  end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93