src/ZF/ind_syntax.ML
author paulson
Fri Dec 22 11:09:28 1995 +0100 (1995-12-22 ago)
changeset 1418 f5f97ee67cbb
parent 742 faa3efc1d130
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
Improving space efficiency of inductive/datatype definitions.
Reduce usage of "open" and change struct open X; D end to
let open X in struct D end end whenever possible -- removes X from the final
structure. Especially needed for functors Intr_elim and Indrule.

intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of
generating a new one. Inductive defs no longer export sumprod_free_SEs

ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM.
It is never used outside, is easily recovered using
bnd_mono and def_lfp_Tarski, and takes up considerable store.

Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items
no longer exported.

mutual_induct is simply "True" unless it is going to be
significantly different from induct -- either because there is mutual
recursion or because it involves tuples.
     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 (** Abstract syntax definitions for FOL and ZF **)
    16 
    17 val iT = Type("i",[])
    18 and oT = Type("o",[]);
    19 
    20 (*Given u expecting arguments of types [T1,...,Tn], create term of 
    21   type T1*...*Tn => i using split*)
    22 fun ap_split split u [ ]   = Abs("null", iT, u)
    23   | ap_split split u [_]   = u
    24   | ap_split split u [_,_] = split $ u
    25   | ap_split split u (T::Ts) = 
    26       split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
    27 
    28 val conj = Const("op &", [oT,oT]--->oT)
    29 and disj = Const("op |", [oT,oT]--->oT)
    30 and imp = Const("op -->", [oT,oT]--->oT);
    31 
    32 val eq_const = Const("op =", [iT,iT]--->oT);
    33 
    34 val mem_const = Const("op :", [iT,iT]--->oT);
    35 
    36 val exists_const = Const("Ex", [iT-->oT]--->oT);
    37 fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
    38 
    39 val all_const = Const("All", [iT-->oT]--->oT);
    40 fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
    41 
    42 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    43 fun mk_all_imp (A,P) = 
    44     all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
    45 
    46 val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    47 
    48 val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
    49 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
    50 
    51 val Trueprop = Const("Trueprop",oT-->propT);
    52 fun mk_tprop P = Trueprop $ P;
    53 
    54 (*simple error-checking in the premises of an inductive definition*)
    55 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    56 	error"Premises may not be conjuctive"
    57   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
    58 	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
    59   | chk_prem rec_hd t = 
    60 	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
    61 
    62 (*Return the conclusion of a rule, of the form t:X*)
    63 fun rule_concl rl = 
    64     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
    65 		Logic.strip_imp_concl rl
    66     in  (t,X)  end;
    67 
    68 (*As above, but return error message if bad*)
    69 fun rule_concl_msg sign rl = rule_concl rl
    70     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
    71 			  Sign.string_of_term sign rl);
    72 
    73 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
    74   read_instantiate replaces a propositional variable by a formula variable*)
    75 val equals_CollectD = 
    76     read_instantiate [("W","?Q")]
    77         (make_elim (equalityD1 RS subsetD RS CollectD2));
    78 
    79 
    80 (** For datatype definitions **)
    81 
    82 fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
    83   | dest_mem _ = error "Constructor specifications must have the form x:A";
    84 
    85 (*read a constructor specification*)
    86 fun read_construct sign (id, sprems, syn) =
    87     let val prems = map (readtm sign oT) sprems
    88 	val args = map (#1 o dest_mem) prems
    89 	val T = (map (#2 o dest_Free) args) ---> iT
    90 		handle TERM _ => error 
    91 		    "Bad variable in constructor specification"
    92         val name = Syntax.const_name id syn  (*handle infix constructors*)
    93     in ((id,T,syn), name, args, prems) end;
    94 
    95 val read_constructs = map o map o read_construct;
    96 
    97 (*convert constructor specifications into introduction rules*)
    98 fun mk_intr_tms (rec_tm, constructs) =
    99   let fun mk_intr ((id,T,syn), name, args, prems) =
   100 	  Logic.list_implies
   101 	      (map mk_tprop prems,
   102 	       mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
   103   in  map mk_intr constructs  end;
   104 
   105 val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
   106 
   107 val Un		= Const("op Un", [iT,iT]--->iT)
   108 and empty	= Const("0", iT)
   109 and univ	= Const("univ", iT-->iT)
   110 and quniv	= Const("quniv", iT-->iT);
   111 
   112 (*Make a datatype's domain: form the union of its set parameters*)
   113 fun union_params rec_tm =
   114   let val (_,args) = strip_comb rec_tm
   115   in  case (filter (fn arg => type_of arg = iT) args) of
   116          []    => empty
   117        | iargs => fold_bal (app Un) iargs
   118   end;
   119 
   120 (*Previously these both did    replicate (length rec_tms);  however now
   121   [q]univ itself constitutes the sum domain for mutual recursion!*)
   122 fun data_domain rec_tms = univ $ union_params (hd rec_tms);
   123 fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
   124 
   125 (*Could go to FOL, but it's hardly general*)
   126 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
   127  (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
   128 
   129 val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
   130   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
   131 
   132 (*Delete needless equality assumptions*)
   133 val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
   134      (fn _ => [assume_tac 1]);
   135 
   136 (*Includes rules for succ and Pair since they are common constructions*)
   137 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   138 		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
   139 		make_elim succ_inject, 
   140 		refl_thin, conjE, exE, disjE];
   141 
   142 (*Turns iff rules into safe elimination rules*)
   143 fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
   144 
   145 end;
   146