--- a/src/ZF/ind-syntax.ML Sat Apr 05 16:18:58 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(* Title: ZF/ind-syntax.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Abstract Syntax functions for Inductive Definitions
-*)
-
-
-(*SHOULD BE ABLE TO DELETE THESE!*)
-fun flatten_typ sign T =
- let val {syn,...} = Sign.rep_sg sign
- in Pretty.str_of (Syntax.pretty_typ syn T)
- end;
-fun flatten_term sign t = Pretty.str_of (Sign.pretty_term sign t);
-
-(*Add constants to a theory*)
-infix addconsts;
-fun thy addconsts const_decs =
- extend_theory thy (space_implode "_" (flat (map #1 const_decs))
- ^ "_Theory")
- ([], [], [], [], const_decs, None) [];
-
-
-(*Make a definition, lhs==rhs, checking that vars on lhs contain *)
-fun mk_defpair sign (lhs,rhs) =
- let val Const(name,_) = head_of lhs
- val dummy = assert (term_vars rhs subset term_vars lhs
- andalso
- term_frees rhs subset term_frees lhs
- andalso
- term_tvars rhs subset term_tvars lhs
- andalso
- term_tfrees rhs subset term_tfrees lhs)
- ("Extra variables on RHS in definition of " ^ name)
- in (name ^ "_def",
- flatten_term sign (Logic.mk_equals (lhs,rhs)))
- end;
-
-fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
-
-(*export to Pure/library? *)
-fun assert_all pred l msg_fn =
- let fun asl [] = ()
- | asl (x::xs) = if pred x then asl xs
- else error (msg_fn x)
- in asl l end;
-
-
-(** Abstract syntax definitions for FOL and ZF **)
-
-val iT = Type("i",[])
-and oT = Type("o",[]);
-
-fun ap t u = t$u;
-fun app t (u1,u2) = t $ u1 $ u2;
-
-(*Given u expecting arguments of types [T1,...,Tn], create term of
- type T1*...*Tn => i using split*)
-fun ap_split split u [ ] = Abs("null", iT, u)
- | ap_split split u [_] = u
- | ap_split split u [_,_] = split $ u
- | ap_split split u (T::Ts) =
- split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
-
-val conj = Const("op &", [oT,oT]--->oT)
-and disj = Const("op |", [oT,oT]--->oT)
-and imp = Const("op -->", [oT,oT]--->oT);
-
-val eq_const = Const("op =", [iT,iT]--->oT);
-
-val mem_const = Const("op :", [iT,iT]--->oT);
-
-val exists_const = Const("Ex", [iT-->oT]--->oT);
-fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
-
-val all_const = Const("All", [iT-->oT]--->oT);
-fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
-
-(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
-fun mk_all_imp (A,P) =
- all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
-
-
-val Part_const = Const("Part", [iT,iT-->iT]--->iT);
-
-val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
-fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
-
-val Trueprop = Const("Trueprop",oT-->propT);
-fun mk_tprop P = Trueprop $ P;
-fun dest_tprop (Const("Trueprop",_) $ P) = P;
-
-(*Prove a goal stated as a term, with exception handling*)
-fun prove_term sign defs (P,tacsf) =
- let val ct = Sign.cterm_of sign P
- in prove_goalw_cterm defs ct tacsf
- handle e => (writeln ("Exception in proof of\n" ^
- Sign.string_of_cterm ct);
- raise e)
- end;
-
-(*Read an assumption in the given theory*)
-fun assume_read thy a = assume (Sign.read_cterm (sign_of thy) (a,propT));
-
-(*Make distinct individual variables a1, a2, a3, ..., an. *)
-fun mk_frees a [] = []
- | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
-
-(*Used by intr-elim.ML and in individual datatype definitions*)
-val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
- ex_mono, Collect_mono, Part_mono, in_mono];
-
-(*Return the conclusion of a rule, of the form t:X*)
-fun rule_concl rl =
- case dest_tprop (Logic.strip_imp_concl rl) of
- Const("op :",_) $ t $ X => (t,X)
- | _ => error "Conclusion of rule should be a set membership";
-
-(*For deriving cases rules. CollectD2 discards the domain, which is redundant;
- read_instantiate replaces a propositional variable by a formula variable*)
-val equals_CollectD =
- read_instantiate [("W","?Q")]
- (make_elim (equalityD1 RS subsetD RS CollectD2));
-
-
-(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
-fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
- | tryres (th, []) = raise THM("tryres", 0, [th]);
-
-fun gen_make_elim elim_rls rl =
- standard (tryres (rl, elim_rls @ [revcut_rl]));
-
-(** For constructor.ML **)
-
-(*Avoids duplicate definitions by removing constants already declared mixfix*)
-fun remove_mixfixes None decs = decs
- | remove_mixfixes (Some sext) decs =
- let val mixtab = Symtab.st_of_declist(Syntax.constants sext, Symtab.null)
- fun is_mix c = case Symtab.lookup(mixtab,c) of
- None=>false | Some _ => true
- in map (fn (cs,styp)=> (filter_out is_mix cs, styp)) decs
- end;
-
-fun ext_constants None = []
- | ext_constants (Some sext) = Syntax.constants sext;
-
-
-(*Could go to FOL, but it's hardly general*)
-val [def] = goal IFOL.thy "a==b ==> a=c <-> c=b";
-by (rewtac def);
-by (rtac iffI 1);
-by (REPEAT (etac sym 1));
-val def_swap_iff = result();
-
-val def_trans = prove_goal IFOL.thy "[| f==g; g(a)=b |] ==> f(a)=b"
- (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
-
-(*Delete needless equality assumptions*)
-val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P"
- (fn _ => [assume_tac 1]);
-