src/ZF/ind_syntax.ML
author wenzelm
Tue Jan 12 15:17:37 1999 +0100 (1999-01-12 ago)
changeset 6093 87bf8c03b169
parent 6053 8a1059aa01f0
child 6112 5e4871c5136b
permissions -rw-r--r--
eliminated global/local names;
clasohm@1461
     1
(*  Title:      ZF/ind-syntax.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Abstract Syntax functions for Inductive Definitions
clasohm@0
     7
*)
clasohm@0
     8
lcp@516
     9
(*The structure protects these items from redeclaration (somewhat!).  The 
lcp@516
    10
  datatype definitions in theory files refer to these items by name!
lcp@516
    11
*)
lcp@516
    12
structure Ind_Syntax =
lcp@516
    13
struct
clasohm@0
    14
paulson@4804
    15
(*Print tracing messages during processing of "inductive" theory sections*)
paulson@4804
    16
val trace = ref false;
paulson@4804
    17
paulson@6053
    18
fun traceIt msg ct = 
paulson@6053
    19
    if !trace then (writeln (msg ^ string_of_cterm ct); ct)
paulson@6053
    20
    else ct;
paulson@6053
    21
paulson@4352
    22
(** Abstract syntax definitions for ZF **)
clasohm@0
    23
paulson@4352
    24
val iT = Type("i",[]);
clasohm@0
    25
paulson@4352
    26
val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
clasohm@0
    27
clasohm@0
    28
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
clasohm@0
    29
fun mk_all_imp (A,P) = 
paulson@4352
    30
    FOLogic.all_const iT $ 
paulson@4972
    31
      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
paulson@4972
    32
	           betapply(P, Bound 0));
clasohm@0
    33
clasohm@0
    34
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
clasohm@0
    35
paulson@6053
    36
val apply_const = Const("op `", [iT,iT]--->iT);
paulson@6053
    37
wenzelm@6093
    38
val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
paulson@6053
    39
paulson@4352
    40
val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
clasohm@0
    41
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
clasohm@0
    42
lcp@516
    43
(*simple error-checking in the premises of an inductive definition*)
lcp@516
    44
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
clasohm@1461
    45
        error"Premises may not be conjuctive"
lcp@516
    46
  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
clasohm@1461
    47
        deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
lcp@516
    48
  | chk_prem rec_hd t = 
clasohm@1461
    49
        deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
lcp@516
    50
lcp@14
    51
(*Return the conclusion of a rule, of the form t:X*)
clasohm@0
    52
fun rule_concl rl = 
lcp@435
    53
    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
clasohm@1461
    54
                Logic.strip_imp_concl rl
lcp@435
    55
    in  (t,X)  end;
lcp@435
    56
lcp@435
    57
(*As above, but return error message if bad*)
lcp@435
    58
fun rule_concl_msg sign rl = rule_concl rl
lcp@435
    59
    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
clasohm@1461
    60
                          Sign.string_of_term sign rl);
clasohm@0
    61
clasohm@0
    62
(*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
clasohm@0
    63
  read_instantiate replaces a propositional variable by a formula variable*)
clasohm@0
    64
val equals_CollectD = 
clasohm@0
    65
    read_instantiate [("W","?Q")]
clasohm@0
    66
        (make_elim (equalityD1 RS subsetD RS CollectD2));
clasohm@0
    67
clasohm@0
    68
lcp@516
    69
(** For datatype definitions **)
lcp@516
    70
paulson@6053
    71
(*Constructor name, type, mixfix info;
paulson@6053
    72
  internal name from mixfix, datatype sets, full premises*)
paulson@6053
    73
type constructor_spec = 
paulson@6053
    74
    ((string * typ * mixfix) * string * term list * term list);
paulson@6053
    75
lcp@516
    76
fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
lcp@516
    77
  | dest_mem _ = error "Constructor specifications must have the form x:A";
lcp@516
    78
lcp@516
    79
(*read a constructor specification*)
lcp@516
    80
fun read_construct sign (id, sprems, syn) =
paulson@4352
    81
    let val prems = map (readtm sign FOLogic.oT) sprems
clasohm@1461
    82
        val args = map (#1 o dest_mem) prems
clasohm@1461
    83
        val T = (map (#2 o dest_Free) args) ---> iT
clasohm@1461
    84
                handle TERM _ => error 
clasohm@1461
    85
                    "Bad variable in constructor specification"
wenzelm@568
    86
        val name = Syntax.const_name id syn  (*handle infix constructors*)
lcp@516
    87
    in ((id,T,syn), name, args, prems) end;
lcp@516
    88
lcp@516
    89
val read_constructs = map o map o read_construct;
clasohm@0
    90
lcp@516
    91
(*convert constructor specifications into introduction rules*)
wenzelm@3925
    92
fun mk_intr_tms sg (rec_tm, constructs) =
wenzelm@3925
    93
  let
wenzelm@3925
    94
    fun mk_intr ((id,T,syn), name, args, prems) =
wenzelm@3925
    95
      Logic.list_implies
paulson@4352
    96
        (map FOLogic.mk_Trueprop prems,
paulson@4352
    97
	 FOLogic.mk_Trueprop
paulson@4352
    98
	    (mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
paulson@4352
    99
	               $ rec_tm))
lcp@516
   100
  in  map mk_intr constructs  end;
lcp@516
   101
wenzelm@3925
   102
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
clasohm@0
   103
clasohm@1461
   104
val Un          = Const("op Un", [iT,iT]--->iT)
clasohm@1461
   105
and empty       = Const("0", iT)
wenzelm@6093
   106
and univ        = Const("Univ.univ", iT-->iT)
wenzelm@6093
   107
and quniv       = Const("QUniv.quniv", iT-->iT);
clasohm@0
   108
lcp@516
   109
(*Make a datatype's domain: form the union of its set parameters*)
lcp@516
   110
fun union_params rec_tm =
lcp@516
   111
  let val (_,args) = strip_comb rec_tm
lcp@516
   112
  in  case (filter (fn arg => type_of arg = iT) args) of
lcp@516
   113
         []    => empty
lcp@516
   114
       | iargs => fold_bal (app Un) iargs
lcp@516
   115
  end;
lcp@516
   116
lcp@742
   117
(*Previously these both did    replicate (length rec_tms);  however now
lcp@742
   118
  [q]univ itself constitutes the sum domain for mutual recursion!*)
paulson@6053
   119
fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
paulson@6053
   120
  | data_domain true  rec_tms = quniv $ union_params (hd rec_tms);
clasohm@0
   121
clasohm@0
   122
(*Could go to FOL, but it's hardly general*)
lcp@516
   123
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
lcp@516
   124
 (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
clasohm@0
   125
clasohm@0
   126
val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
clasohm@0
   127
  (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
clasohm@0
   128
lcp@55
   129
(*Delete needless equality assumptions*)
lcp@55
   130
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
lcp@55
   131
     (fn _ => [assume_tac 1]);
clasohm@0
   132
paulson@1418
   133
(*Includes rules for succ and Pair since they are common constructions*)
paulson@1418
   134
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
clasohm@1461
   135
                Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
clasohm@1461
   136
                make_elim succ_inject, 
clasohm@1461
   137
                refl_thin, conjE, exE, disjE];
paulson@1418
   138
paulson@1418
   139
(*Turns iff rules into safe elimination rules*)
paulson@1418
   140
fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
paulson@1418
   141
lcp@516
   142
end;
lcp@516
   143