src/ZF/constructor.ML
author lcp
Thu Aug 18 17:41:40 1994 +0200 (1994-08-18 ago)
changeset 543 e961b2092869
parent 516 1957113f0d7d
child 1103 08fda5148971
permissions -rw-r--r--
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and
Logic.unvarify
clasohm@0
     1
(*  Title: 	ZF/constructor.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
lcp@516
     6
Constructor function module -- for (Co)Datatype Definitions
clasohm@0
     7
*)
clasohm@0
     8
lcp@516
     9
signature CONSTRUCTOR_ARG =
clasohm@0
    10
  sig
lcp@516
    11
  val thy    	   : theory		(*parent containing constructor defs*)
lcp@516
    12
  val big_rec_name : string		(*name of mutually recursive set*)
lcp@516
    13
  val con_ty_lists : ((string*typ*mixfix) * 
lcp@516
    14
		      string * term list * term list) list list
lcp@516
    15
					(*description of constructors*)
clasohm@0
    16
  end;
clasohm@0
    17
clasohm@0
    18
signature CONSTRUCTOR_RESULT =
clasohm@0
    19
  sig
lcp@516
    20
  val con_defs	 : thm list		(*definitions made in thy*)
clasohm@0
    21
  val case_eqns  : thm list		(*equations for case operator*)
clasohm@0
    22
  val free_iffs  : thm list		(*freeness rewrite rules*)
clasohm@0
    23
  val free_SEs   : thm list		(*freeness destruct rules*)
clasohm@0
    24
  val mk_free    : string -> thm	(*makes freeness theorems*)
clasohm@0
    25
  end;
clasohm@0
    26
clasohm@0
    27
lcp@516
    28
(*Proves theorems relating to constructors*)
lcp@516
    29
functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
clasohm@0
    30
                      Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
clasohm@0
    31
struct
lcp@516
    32
open Logic Const Ind_Syntax;
clasohm@0
    33
lcp@516
    34
(*1st element is the case definition; others are the constructors*)
clasohm@0
    35
val big_case_name = big_rec_name ^ "_case";
clasohm@0
    36
lcp@516
    37
val con_defs = get_def thy big_case_name :: 
lcp@516
    38
               map (get_def thy o #2) (flat con_ty_lists);
clasohm@0
    39
clasohm@0
    40
(** Prove the case theorem **)
clasohm@0
    41
lcp@516
    42
(*Get the case term from its definition*)
lcp@516
    43
val Const("==",_) $ big_case_tm $ _ =
lcp@543
    44
    hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
lcp@516
    45
lcp@516
    46
val (_, big_case_args) = strip_comb big_case_tm;
lcp@516
    47
clasohm@0
    48
(*Each equation has the form 
clasohm@0
    49
  rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
lcp@516
    50
fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = 
lcp@516
    51
    mk_tprop (eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
lcp@516
    52
		         $ (list_comb (case_free, args))) ;
clasohm@0
    53
clasohm@0
    54
val case_trans = hd con_defs RS def_trans;
clasohm@0
    55
lcp@516
    56
(*Proves a single case equation.  Could use simp_tac, but it's slower!*)
clasohm@0
    57
fun case_tacsf con_def _ = 
clasohm@0
    58
  [rewtac con_def,
clasohm@0
    59
   rtac case_trans 1,
clasohm@0
    60
   REPEAT (resolve_tac [refl, Pr.split_eq RS trans, 
clasohm@0
    61
			Su.case_inl RS trans, 
clasohm@0
    62
			Su.case_inr RS trans] 1)];
clasohm@0
    63
clasohm@0
    64
fun prove_case_equation (arg,con_def) =
lcp@543
    65
    prove_goalw_cterm [] 
lcp@543
    66
        (cterm_of (sign_of thy) (mk_case_equation arg))
lcp@543
    67
	(case_tacsf con_def);
clasohm@0
    68
clasohm@0
    69
val free_iffs = 
clasohm@0
    70
    map standard (con_defs RL [def_swap_iff]) @
clasohm@0
    71
    [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
clasohm@0
    72
clasohm@0
    73
val free_SEs   = map (gen_make_elim [conjE,FalseE]) (free_iffs RL [iffD1]);
clasohm@0
    74
clasohm@0
    75
val free_cs = ZF_cs addSEs free_SEs;
clasohm@0
    76
clasohm@0
    77
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
clasohm@0
    78
  con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
clasohm@0
    79
fun mk_free s =
lcp@516
    80
    prove_goalw thy con_defs s
clasohm@0
    81
      (fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
clasohm@0
    82
clasohm@0
    83
val case_eqns = map prove_case_equation 
clasohm@0
    84
		    (flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
clasohm@0
    85
clasohm@0
    86
end;
clasohm@0
    87
clasohm@0
    88