src/ZF/ind_syntax.ML
author paulson
Wed May 27 12:23:45 1998 +0200 (1998-05-27 ago)
changeset 4972 7fe1d30c1374
parent 4804 02b7c759159b
child 6053 8a1059aa01f0
permissions -rw-r--r--
mk_all_imp: no longer creates goals that have beta-redexes
     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 (** Abstract syntax definitions for ZF **)
    19 
    20 val iT = Type("i",[]);
    21 
    22 val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
    23 
    24 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    25 fun mk_all_imp (A,P) = 
    26     FOLogic.all_const iT $ 
    27       Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
    28 	           betapply(P, Bound 0));
    29 
    30 val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    31 
    32 val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
    33 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
    34 
    35 (*simple error-checking in the premises of an inductive definition*)
    36 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    37         error"Premises may not be conjuctive"
    38   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
    39         deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
    40   | chk_prem rec_hd t = 
    41         deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
    42 
    43 (*Return the conclusion of a rule, of the form t:X*)
    44 fun rule_concl rl = 
    45     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
    46                 Logic.strip_imp_concl rl
    47     in  (t,X)  end;
    48 
    49 (*As above, but return error message if bad*)
    50 fun rule_concl_msg sign rl = rule_concl rl
    51     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
    52                           Sign.string_of_term sign rl);
    53 
    54 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
    55   read_instantiate replaces a propositional variable by a formula variable*)
    56 val equals_CollectD = 
    57     read_instantiate [("W","?Q")]
    58         (make_elim (equalityD1 RS subsetD RS CollectD2));
    59 
    60 
    61 (** For datatype definitions **)
    62 
    63 fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
    64   | dest_mem _ = error "Constructor specifications must have the form x:A";
    65 
    66 (*read a constructor specification*)
    67 fun read_construct sign (id, sprems, syn) =
    68     let val prems = map (readtm sign FOLogic.oT) sprems
    69         val args = map (#1 o dest_mem) prems
    70         val T = (map (#2 o dest_Free) args) ---> iT
    71                 handle TERM _ => error 
    72                     "Bad variable in constructor specification"
    73         val name = Syntax.const_name id syn  (*handle infix constructors*)
    74     in ((id,T,syn), name, args, prems) end;
    75 
    76 val read_constructs = map o map o read_construct;
    77 
    78 (*convert constructor specifications into introduction rules*)
    79 fun mk_intr_tms sg (rec_tm, constructs) =
    80   let
    81     fun mk_intr ((id,T,syn), name, args, prems) =
    82       Logic.list_implies
    83         (map FOLogic.mk_Trueprop prems,
    84 	 FOLogic.mk_Trueprop
    85 	    (mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
    86 	               $ rec_tm))
    87   in  map mk_intr constructs  end;
    88 
    89 fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
    90 
    91 val Un          = Const("op Un", [iT,iT]--->iT)
    92 and empty       = Const("0", iT)
    93 and univ        = Const("univ", iT-->iT)
    94 and quniv       = Const("quniv", iT-->iT);
    95 
    96 (*Make a datatype's domain: form the union of its set parameters*)
    97 fun union_params rec_tm =
    98   let val (_,args) = strip_comb rec_tm
    99   in  case (filter (fn arg => type_of arg = iT) args) of
   100          []    => empty
   101        | iargs => fold_bal (app Un) iargs
   102   end;
   103 
   104 (*Previously these both did    replicate (length rec_tms);  however now
   105   [q]univ itself constitutes the sum domain for mutual recursion!*)
   106 fun data_domain rec_tms = univ $ union_params (hd rec_tms);
   107 fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
   108 
   109 (*Could go to FOL, but it's hardly general*)
   110 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
   111  (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
   112 
   113 val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
   114   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
   115 
   116 (*Delete needless equality assumptions*)
   117 val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
   118      (fn _ => [assume_tac 1]);
   119 
   120 (*Includes rules for succ and Pair since they are common constructions*)
   121 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   122                 Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
   123                 make_elim succ_inject, 
   124                 refl_thin, conjE, exE, disjE];
   125 
   126 (*Turns iff rules into safe elimination rules*)
   127 fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
   128 
   129 end;
   130 
   131 
   132 val trace_induct = Ind_Syntax.trace;