src/ZF/ind_syntax.ML
author wenzelm
Sat Mar 01 14:10:15 2008 +0100 (2008-03-01 ago)
changeset 26189 9808cca5c54d
parent 26059 b67a225b50fd
child 26939 1035c89b4c02
permissions -rw-r--r--
misc cleanup of embedded ML code;
use more antiquotations;
tuned;
     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 structure Ind_Syntax =
    10 struct
    11 
    12 (*Print tracing messages during processing of "inductive" theory sections*)
    13 val trace = ref false;
    14 
    15 fun traceIt msg thy t =
    16   if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
    17   else t;
    18 
    19 
    20 (** Abstract syntax definitions for ZF **)
    21 
    22 val iT = Type("i",[]);
    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 $ (@{const mem} $ Bound 0 $ A) $
    28 	           Term.betapply(P, Bound 0));
    29 
    30 fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
    31 
    32 (*simple error-checking in the premises of an inductive definition*)
    33 fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
    34         error"Premises may not be conjuctive"
    35   | chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
    36         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
    37   | chk_prem rec_hd t =
    38         (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
    39 
    40 (*Return the conclusion of a rule, of the form t:X*)
    41 fun rule_concl rl =
    42     let val Const (@{const_name Trueprop}, _) $ (Const (@{const_name mem}, _) $ t $ X) =
    43                 Logic.strip_imp_concl rl
    44     in  (t,X)  end;
    45 
    46 (*As above, but return error message if bad*)
    47 fun rule_concl_msg sign rl = rule_concl rl
    48     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
    49                           Sign.string_of_term sign rl);
    50 
    51 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
    52   read_instantiate replaces a propositional variable by a formula variable*)
    53 val equals_CollectD =
    54     read_instantiate [("W","?Q")]
    55         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
    56 
    57 
    58 (** For datatype definitions **)
    59 
    60 (*Constructor name, type, mixfix info;
    61   internal name from mixfix, datatype sets, full premises*)
    62 type constructor_spec =
    63     (string * typ * mixfix) * string * term list * term list;
    64 
    65 fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A)
    66   | dest_mem _ = error "Constructor specifications must have the form x:A";
    67 
    68 (*read a constructor specification*)
    69 fun read_construct sign (id, sprems, syn) =
    70     let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
    71         val args = map (#1 o dest_mem) prems
    72         val T = (map (#2 o dest_Free) args) ---> iT
    73                 handle TERM _ => error
    74                     "Bad variable in constructor specification"
    75         val name = Syntax.const_name id syn  (*handle infix constructors*)
    76     in ((id,T,syn), name, args, prems) end;
    77 
    78 val read_constructs = map o map o read_construct;
    79 
    80 (*convert constructor specifications into introduction rules*)
    81 fun mk_intr_tms sg (rec_tm, constructs) =
    82   let
    83     fun mk_intr ((id,T,syn), name, args, prems) =
    84       Logic.list_implies
    85         (map FOLogic.mk_Trueprop prems,
    86 	 FOLogic.mk_Trueprop
    87 	    (@{const mem} $ list_comb (Const (Sign.full_name sg name, T), args)
    88 	               $ rec_tm))
    89   in  map mk_intr constructs  end;
    90 
    91 fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
    92 
    93 fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;
    94 
    95 (*Make a datatype's domain: form the union of its set parameters*)
    96 fun union_params (rec_tm, cs) =
    97   let val (_,args) = strip_comb rec_tm
    98       fun is_ind arg = (type_of arg = iT)
    99   in  case List.filter is_ind (args @ cs) of
   100          []     => @{const 0}
   101        | u_args => BalancedTree.make mk_Un u_args
   102   end;
   103 
   104 
   105 (*Includes rules for succ and Pair since they are common constructions*)
   106 val elim_rls =
   107   [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0},
   108    @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject},
   109    make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}];
   110 
   111 
   112 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
   113 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   114   | tryres (th, []) = raise THM("tryres", 0, [th]);
   115 
   116 fun gen_make_elim elim_rls rl =
   117       standard (tryres (rl, elim_rls @ [revcut_rl]));
   118 
   119 (*Turns iff rules into safe elimination rules*)
   120 fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
   121 
   122 end;
   123