src/ZF/ind_syntax.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 55151 f331472f1027
child 59755 f8d164ab0dc1
permissions -rw-r--r--
proper context for match_tac etc.;
     1 (*  Title:      ZF/ind_syntax.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Abstract Syntax functions for Inductive Definitions.
     6 *)
     7 
     8 structure Ind_Syntax =
     9 struct
    10 
    11 (*Print tracing messages during processing of "inductive" theory sections*)
    12 val trace = Unsynchronized.ref false;
    13 
    14 fun traceIt msg thy t =
    15   if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
    16   else t;
    17 
    18 
    19 (** Abstract syntax definitions for ZF **)
    20 
    21 val iT = Type(@{type_name i}, []);
    22 
    23 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    24 fun mk_all_imp (A,P) =
    25     FOLogic.all_const iT $
    26       Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
    27                    Term.betapply(P, Bound 0));
    28 
    29 fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT) t;
    30 
    31 (*simple error-checking in the premises of an inductive definition*)
    32 fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =
    33         error"Premises may not be conjuctive"
    34   | chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
    35         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
    36   | chk_prem rec_hd t =
    37         (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
    38 
    39 (*Return the conclusion of a rule, of the form t:X*)
    40 fun rule_concl rl =
    41     let val Const (@{const_name Trueprop}, _) $ (Const (@{const_name mem}, _) $ t $ X) =
    42                 Logic.strip_imp_concl rl
    43     in  (t,X)  end;
    44 
    45 (*As above, but return error message if bad*)
    46 fun rule_concl_msg sign rl = rule_concl rl
    47     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
    48                           Syntax.string_of_term_global sign rl);
    49 
    50 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
    51   read_instantiate replaces a propositional variable by a formula variable*)
    52 val equals_CollectD =
    53     Rule_Insts.read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
    54         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
    55 
    56 
    57 (** For datatype definitions **)
    58 
    59 (*Constructor name, type, mixfix info;
    60   internal name from mixfix, datatype sets, full premises*)
    61 type constructor_spec =
    62     (string * typ * mixfix) * string * term list * term list;
    63 
    64 fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A)
    65   | dest_mem _ = error "Constructor specifications must have the form x:A";
    66 
    67 (*read a constructor specification*)
    68 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
    69     let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
    70           |> Syntax.check_terms ctxt
    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     in ((id,T,syn), id, args, prems) end;
    76 
    77 val read_constructs = map o map o read_construct;
    78 
    79 (*convert constructor specifications into introduction rules*)
    80 fun mk_intr_tms sg (rec_tm, constructs) =
    81   let
    82     fun mk_intr ((id,T,syn), name, args, prems) =
    83       Logic.list_implies
    84         (map FOLogic.mk_Trueprop prems,
    85          FOLogic.mk_Trueprop
    86             (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
    87                        $ rec_tm))
    88   in  map mk_intr constructs  end;
    89 
    90 fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
    91 
    92 fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;
    93 
    94 (*Make a datatype's domain: form the union of its set parameters*)
    95 fun union_params (rec_tm, cs) =
    96   let val (_,args) = strip_comb rec_tm
    97       fun is_ind arg = (type_of arg = iT)
    98   in  case filter is_ind (args @ cs) of
    99          [] => @{const zero}
   100        | u_args => Balanced_Tree.make mk_Un u_args
   101   end;
   102 
   103 
   104 (*Includes rules for succ and Pair since they are common constructions*)
   105 val elim_rls =
   106   [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0},
   107    @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject},
   108    make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}];
   109 
   110 
   111 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
   112 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   113   | tryres (th, []) = raise THM("tryres", 0, [th]);
   114 
   115 fun gen_make_elim elim_rls rl =
   116   Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
   117 
   118 (*Turns iff rules into safe elimination rules*)
   119 fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
   120 
   121 end;
   122