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