src/ZF/ind_syntax.ML
author lcp
Tue Jun 21 17:20:34 1994 +0200 (1994-06-21 ago)
changeset 435 ca5356bd315a
parent 231 cb6a24451544
child 444 3ca9d49fd662
permissions -rw-r--r--
Addition of cardinals and order types, various tidying
     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 
    93 (*Prove a goal stated as a term, with exception handling*)
    94 fun prove_term sign defs (P,tacsf) = 
    95     let val ct = cterm_of sign P
    96     in  prove_goalw_cterm defs ct tacsf
    97 	handle e => (writeln ("Exception in proof of\n" ^
    98 			       string_of_cterm ct); 
    99 		     raise e)
   100     end;
   101 
   102 (*Read an assumption in the given theory*)
   103 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
   104 
   105 (*Make distinct individual variables a1, a2, a3, ..., an. *)
   106 fun mk_frees a [] = []
   107   | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
   108 
   109 (*Used by intr-elim.ML and in individual datatype definitions*)
   110 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
   111 		   ex_mono, Collect_mono, Part_mono, in_mono];
   112 
   113 (*Return the conclusion of a rule, of the form t:X*)
   114 fun rule_concl rl = 
   115     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
   116 		Logic.strip_imp_concl rl
   117     in  (t,X)  end;
   118 
   119 (*As above, but return error message if bad*)
   120 fun rule_concl_msg sign rl = rule_concl rl
   121     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
   122 			  Sign.string_of_term sign rl);
   123 
   124 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   125   read_instantiate replaces a propositional variable by a formula variable*)
   126 val equals_CollectD = 
   127     read_instantiate [("W","?Q")]
   128         (make_elim (equalityD1 RS subsetD RS CollectD2));
   129 
   130 
   131 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
   132 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   133   | tryres (th, []) = raise THM("tryres", 0, [th]);
   134 
   135 fun gen_make_elim elim_rls rl = 
   136       standard (tryres (rl, elim_rls @ [revcut_rl]));
   137 
   138 (** For constructor.ML **)
   139 
   140 (*Avoids duplicate definitions by removing constants already declared mixfix*)
   141 fun remove_mixfixes None decs = decs
   142   | remove_mixfixes (Some sext) decs =
   143       let val mixtab = Symtab.st_of_declist(Syntax.constants sext, Symtab.null)
   144 	  fun is_mix c = case Symtab.lookup(mixtab,c) of
   145 			     None=>false | Some _ => true
   146       in  map (fn (cs,styp)=> (filter_out is_mix cs, styp)) decs
   147       end;
   148 
   149 fun ext_constants None        = []
   150   | ext_constants (Some sext) = Syntax.constants sext;
   151 
   152 
   153 (*Could go to FOL, but it's hardly general*)
   154 val [def] = goal IFOL.thy "a==b ==> a=c <-> c=b";
   155 by (rewtac def);
   156 by (rtac iffI 1);
   157 by (REPEAT (etac sym 1));
   158 val def_swap_iff = result();
   159 
   160 val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
   161   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
   162 
   163 (*Delete needless equality assumptions*)
   164 val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
   165      (fn _ => [assume_tac 1]);
   166