src/ZF/ind_syntax.ML
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 23419 8c30dd4b3b22
child 24826 78e6a3cea367
permissions -rw-r--r--
added Tools/lin_arith.ML;
     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 thy t = 
    19   if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
    20   else t;
    21 
    22 
    23 (** Abstract syntax definitions for ZF **)
    24 
    25 val iT = Type("i",[]);
    26 
    27 val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
    28 
    29 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    30 fun mk_all_imp (A,P) = 
    31     FOLogic.all_const iT $ 
    32       Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
    33 	           Term.betapply(P, Bound 0));
    34 
    35 val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    36 
    37 val apply_const = Const("op `", [iT,iT]--->iT);
    38 
    39 val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
    40 
    41 val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
    42 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
    43 
    44 (*simple error-checking in the premises of an inductive definition*)
    45 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    46         error"Premises may not be conjuctive"
    47   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
    48         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
    49   | chk_prem rec_hd t = 
    50         (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
    51 
    52 (*Return the conclusion of a rule, of the form t:X*)
    53 fun rule_concl rl = 
    54     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
    55                 Logic.strip_imp_concl rl
    56     in  (t,X)  end;
    57 
    58 (*As above, but return error message if bad*)
    59 fun rule_concl_msg sign rl = rule_concl rl
    60     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
    61                           Sign.string_of_term sign rl);
    62 
    63 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
    64   read_instantiate replaces a propositional variable by a formula variable*)
    65 val equals_CollectD = 
    66     read_instantiate [("W","?Q")]
    67         (make_elim (equalityD1 RS subsetD RS CollectD2));
    68 
    69 
    70 (** For datatype definitions **)
    71 
    72 (*Constructor name, type, mixfix info;
    73   internal name from mixfix, datatype sets, full premises*)
    74 type constructor_spec = 
    75     ((string * typ * mixfix) * string * term list * term list);
    76 
    77 fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
    78   | dest_mem _ = error "Constructor specifications must have the form x:A";
    79 
    80 (*read a constructor specification*)
    81 fun read_construct sign (id, sprems, syn) =
    82     let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
    83         val args = map (#1 o dest_mem) prems
    84         val T = (map (#2 o dest_Free) args) ---> iT
    85                 handle TERM _ => error 
    86                     "Bad variable in constructor specification"
    87         val name = Syntax.const_name id syn  (*handle infix constructors*)
    88     in ((id,T,syn), name, args, prems) end;
    89 
    90 val read_constructs = map o map o read_construct;
    91 
    92 (*convert constructor specifications into introduction rules*)
    93 fun mk_intr_tms sg (rec_tm, constructs) =
    94   let
    95     fun mk_intr ((id,T,syn), name, args, prems) =
    96       Logic.list_implies
    97         (map FOLogic.mk_Trueprop prems,
    98 	 FOLogic.mk_Trueprop
    99 	    (mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
   100 	               $ rec_tm))
   101   in  map mk_intr constructs  end;
   102 
   103 fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
   104 
   105 fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
   106 
   107 val empty       = Const("0", iT)
   108 and univ        = Const("Univ.univ", iT-->iT)
   109 and quniv       = Const("QUniv.quniv", iT-->iT);
   110 
   111 (*Make a datatype's domain: form the union of its set parameters*)
   112 fun union_params (rec_tm, cs) =
   113   let val (_,args) = strip_comb rec_tm
   114       fun is_ind arg = (type_of arg = iT)
   115   in  case List.filter is_ind (args @ cs) of
   116          []     => empty
   117        | u_args => BalancedTree.make mk_Un u_args
   118   end;
   119 
   120 (*univ or quniv constitutes the sum domain for mutual recursion;
   121   it is applied to the datatype parameters and to Consts occurring in the
   122   definition other than Nat.nat and the datatype sets themselves.
   123   FIXME: could insert all constant set expressions, e.g. nat->nat.*)
   124 fun data_domain co (rec_tms, con_ty_lists) = 
   125     let val rec_hds = map head_of rec_tms
   126         val dummy = assert_all is_Const rec_hds
   127           (fn t => "Datatype set not previously declared as constant: " ^
   128                    Sign.string_of_term @{theory IFOL} t);
   129         val rec_names = (*nat doesn't have to be added*)
   130 	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
   131 	val u = if co then quniv else univ
   132 	val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
   133           (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
   134             | _ => I)) con_ty_lists [];
   135     in  u $ union_params (hd rec_tms, cs)  end;
   136 
   137 
   138 (*Could go to FOL, but it's hardly general*)
   139 val def_swap_iff = prove_goal (the_context ()) "a==b ==> a=c <-> c=b"
   140   (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
   141 
   142 val def_trans = prove_goal (the_context ()) "[| f==g;  g(a)=b |] ==> f(a)=b"
   143   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
   144 
   145 (*Delete needless equality assumptions*)
   146 val refl_thin = prove_goal (the_context ()) "!!P. [| a=a;  P |] ==> P"
   147      (fn _ => [assume_tac 1]);
   148 
   149 (*Includes rules for succ and Pair since they are common constructions*)
   150 val elim_rls = [asm_rl, FalseE, thm "succ_neq_0", sym RS thm "succ_neq_0",
   151                 thm "Pair_neq_0", sym RS thm "Pair_neq_0", thm "Pair_inject",
   152                 make_elim (thm "succ_inject"),
   153                 refl_thin, conjE, exE, disjE];
   154 
   155 
   156 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
   157 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   158   | tryres (th, []) = raise THM("tryres", 0, [th]);
   159 
   160 fun gen_make_elim elim_rls rl = 
   161       standard (tryres (rl, elim_rls @ [revcut_rl]));
   162 
   163 (*Turns iff rules into safe elimination rules*)
   164 fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
   165 
   166 end;
   167 
   168 
   169 (*For convenient access by the user*)
   170 val trace_induct = Ind_Syntax.trace;