src/ZF/ind_syntax.ML
author lcp
Tue Jan 18 16:37:12 1994 +0100 (1994-01-18 ago)
changeset 231 cb6a24451544
parent 202 4e68398cdc06
child 435 ca5356bd315a
permissions -rw-r--r--
Updated refs to old Sign functions
     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 
    10 (*SHOULD BE ABLE TO DELETE THESE!*)
    11 fun flatten_typ sign T = 
    12     let val {syn,...} = Sign.rep_sg sign 
    13     in  Pretty.str_of (Syntax.pretty_typ syn T)
    14     end;
    15 fun flatten_term sign t = Pretty.str_of (Sign.pretty_term sign t);
    16 
    17 (*Add constants to a theory*)
    18 infix addconsts;
    19 fun thy addconsts const_decs = 
    20     extend_theory thy (space_implode "_" (flat (map #1 const_decs)) 
    21 		       ^ "_Theory")
    22 		  ([], [], [], [], [], const_decs, None) [];
    23 
    24 
    25 (*Make a definition, lhs==rhs, checking that vars on lhs contain *)
    26 fun mk_defpair sign (lhs,rhs) = 
    27   let val Const(name,_) = head_of lhs
    28       val dummy = assert (term_vars rhs subset term_vars lhs
    29 		       andalso
    30 		       term_frees rhs subset term_frees lhs
    31 		       andalso
    32 		       term_tvars rhs subset term_tvars lhs
    33 		       andalso
    34 		       term_tfrees rhs subset term_tfrees lhs)
    35 	          ("Extra variables on RHS in definition of " ^ name)
    36   in  (name ^ "_def",
    37        flatten_term sign (Logic.mk_equals (lhs,rhs)))
    38   end;
    39 
    40 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
    41 
    42 (*export to Pure/library?  *)
    43 fun assert_all pred l msg_fn = 
    44   let fun asl [] = ()
    45 	| asl (x::xs) = if pred x then asl xs
    46 	                else error (msg_fn x)
    47   in  asl l  end;
    48 
    49 
    50 (** Abstract syntax definitions for FOL and ZF **)
    51 
    52 val iT = Type("i",[])
    53 and oT = Type("o",[]);
    54 
    55 fun ap t u = t$u;
    56 fun app t (u1,u2) = t $ u1 $ u2;
    57 
    58 (*Given u expecting arguments of types [T1,...,Tn], create term of 
    59   type T1*...*Tn => i using split*)
    60 fun ap_split split u [ ]   = Abs("null", iT, u)
    61   | ap_split split u [_]   = u
    62   | ap_split split u [_,_] = split $ u
    63   | ap_split split u (T::Ts) = 
    64       split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
    65 
    66 val conj = Const("op &", [oT,oT]--->oT)
    67 and disj = Const("op |", [oT,oT]--->oT)
    68 and imp = Const("op -->", [oT,oT]--->oT);
    69 
    70 val eq_const = Const("op =", [iT,iT]--->oT);
    71 
    72 val mem_const = Const("op :", [iT,iT]--->oT);
    73 
    74 val exists_const = Const("Ex", [iT-->oT]--->oT);
    75 fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
    76 
    77 val all_const = Const("All", [iT-->oT]--->oT);
    78 fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
    79 
    80 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    81 fun mk_all_imp (A,P) = 
    82     all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
    83 
    84 
    85 val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    86 
    87 val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
    88 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
    89 
    90 val Trueprop = Const("Trueprop",oT-->propT);
    91 fun mk_tprop P = Trueprop $ P;
    92 fun dest_tprop (Const("Trueprop",_) $ P) = P;
    93 
    94 (*Prove a goal stated as a term, with exception handling*)
    95 fun prove_term sign defs (P,tacsf) = 
    96     let val ct = cterm_of sign P
    97     in  prove_goalw_cterm defs ct tacsf
    98 	handle e => (writeln ("Exception in proof of\n" ^
    99 			       string_of_cterm ct); 
   100 		     raise e)
   101     end;
   102 
   103 (*Read an assumption in the given theory*)
   104 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
   105 
   106 (*Make distinct individual variables a1, a2, a3, ..., an. *)
   107 fun mk_frees a [] = []
   108   | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
   109 
   110 (*Used by intr-elim.ML and in individual datatype definitions*)
   111 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
   112 		   ex_mono, Collect_mono, Part_mono, in_mono];
   113 
   114 (*Return the conclusion of a rule, of the form t:X*)
   115 fun rule_concl rl = 
   116     case dest_tprop (Logic.strip_imp_concl rl) of
   117         Const("op :",_) $ t $ X => (t,X) 
   118       | _ => error "Conclusion of rule should be a set membership";
   119 
   120 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   121   read_instantiate replaces a propositional variable by a formula variable*)
   122 val equals_CollectD = 
   123     read_instantiate [("W","?Q")]
   124         (make_elim (equalityD1 RS subsetD RS CollectD2));
   125 
   126 
   127 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
   128 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   129   | tryres (th, []) = raise THM("tryres", 0, [th]);
   130 
   131 fun gen_make_elim elim_rls rl = 
   132       standard (tryres (rl, elim_rls @ [revcut_rl]));
   133 
   134 (** For constructor.ML **)
   135 
   136 (*Avoids duplicate definitions by removing constants already declared mixfix*)
   137 fun remove_mixfixes None decs = decs
   138   | remove_mixfixes (Some sext) decs =
   139       let val mixtab = Symtab.st_of_declist(Syntax.constants sext, Symtab.null)
   140 	  fun is_mix c = case Symtab.lookup(mixtab,c) of
   141 			     None=>false | Some _ => true
   142       in  map (fn (cs,styp)=> (filter_out is_mix cs, styp)) decs
   143       end;
   144 
   145 fun ext_constants None        = []
   146   | ext_constants (Some sext) = Syntax.constants sext;
   147 
   148 
   149 (*Could go to FOL, but it's hardly general*)
   150 val [def] = goal IFOL.thy "a==b ==> a=c <-> c=b";
   151 by (rewtac def);
   152 by (rtac iffI 1);
   153 by (REPEAT (etac sym 1));
   154 val def_swap_iff = result();
   155 
   156 val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
   157   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
   158 
   159 (*Delete needless equality assumptions*)
   160 val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
   161      (fn _ => [assume_tac 1]);
   162