src/ZF/ind_syntax.ML
author lcp
Thu Aug 18 17:41:40 1994 +0200 (1994-08-18 ago)
changeset 543 e961b2092869
parent 516 1957113f0d7d
child 568 756b0e2a6cac
permissions -rw-r--r--
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and
Logic.unvarify
     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 (*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
    15 fun mk_defpair (lhs, rhs) = 
    16   let val Const(name, _) = head_of lhs
    17   in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
    18 
    19 fun get_def thy s = get_axiom thy (s^"_def");
    20 
    21 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
    22 
    23 (** Abstract syntax definitions for FOL and ZF **)
    24 
    25 val iT = Type("i",[])
    26 and oT = Type("o",[]);
    27 
    28 fun ap t u = t$u;
    29 fun app t (u1,u2) = t $ u1 $ u2;
    30 
    31 (*Given u expecting arguments of types [T1,...,Tn], create term of 
    32   type T1*...*Tn => i using split*)
    33 fun ap_split split u [ ]   = Abs("null", iT, u)
    34   | ap_split split u [_]   = u
    35   | ap_split split u [_,_] = split $ u
    36   | ap_split split u (T::Ts) = 
    37       split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
    38 
    39 val conj = Const("op &", [oT,oT]--->oT)
    40 and disj = Const("op |", [oT,oT]--->oT)
    41 and imp = Const("op -->", [oT,oT]--->oT);
    42 
    43 val eq_const = Const("op =", [iT,iT]--->oT);
    44 
    45 val mem_const = Const("op :", [iT,iT]--->oT);
    46 
    47 val exists_const = Const("Ex", [iT-->oT]--->oT);
    48 fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
    49 
    50 val all_const = Const("All", [iT-->oT]--->oT);
    51 fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
    52 
    53 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    54 fun mk_all_imp (A,P) = 
    55     all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
    56 
    57 val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    58 
    59 val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
    60 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
    61 
    62 val Trueprop = Const("Trueprop",oT-->propT);
    63 fun mk_tprop P = Trueprop $ P;
    64 
    65 (*Read an assumption in the given theory*)
    66 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    67 
    68 fun readtm sign T a = 
    69     read_cterm sign (a,T) |> term_of
    70     handle ERROR => error ("The error above occurred for " ^ a);
    71 
    72 (*Skipping initial blanks, find the first identifier*)
    73 fun scan_to_id s = 
    74     s |> explode |> take_prefix is_blank |> #2 |> Lexicon.scan_id |> #1
    75     handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
    76 
    77 fun is_backslash c = c = "\\";
    78 
    79 (*Apply string escapes to a quoted string; see Def of Standard ML, page 3
    80   Does not handle the \ddd form;  no error checking*)
    81 fun escape [] = []
    82   | escape cs = (case take_prefix (not o is_backslash) cs of
    83 	 (front, []) => front
    84        | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
    85        | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
    86        | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
    87        | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
    88        | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
    89        | (front, b::c::rest) => 
    90 	   if is_blank c   (*remove any further blanks and the following \ *)
    91 	   then front @ escape (tl (snd (take_prefix is_blank rest)))
    92 	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
    93 
    94 (*Remove the first and last charaters -- presumed to be quotes*)
    95 val trim = implode o escape o rev o tl o rev o tl o explode;
    96 
    97 (*simple error-checking in the premises of an inductive definition*)
    98 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    99 	error"Premises may not be conjuctive"
   100   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
   101 	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
   102   | chk_prem rec_hd t = 
   103 	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
   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 (*Return the conclusion of a rule, of the form t:X*)
   110 fun rule_concl rl = 
   111     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
   112 		Logic.strip_imp_concl rl
   113     in  (t,X)  end;
   114 
   115 (*As above, but return error message if bad*)
   116 fun rule_concl_msg sign rl = rule_concl rl
   117     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
   118 			  Sign.string_of_term sign rl);
   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 datatype definitions **)
   135 
   136 fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
   137   | dest_mem _ = error "Constructor specifications must have the form x:A";
   138 
   139 (*read a constructor specification*)
   140 fun read_construct sign (id, sprems, syn) =
   141     let val prems = map (readtm sign oT) sprems
   142 	val args = map (#1 o dest_mem) prems
   143 	val T = (map (#2 o dest_Free) args) ---> iT
   144 		handle TERM _ => error 
   145 		    "Bad variable in constructor specification"
   146         val name = const_name id syn  (*handle infix constructors*)
   147     in ((id,T,syn), name, args, prems) end;
   148 
   149 val read_constructs = map o map o read_construct;
   150 
   151 (*convert constructor specifications into introduction rules*)
   152 fun mk_intr_tms (rec_tm, constructs) =
   153   let fun mk_intr ((id,T,syn), name, args, prems) =
   154 	  Logic.list_implies
   155 	      (map mk_tprop prems,
   156 	       mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
   157   in  map mk_intr constructs  end;
   158 
   159 val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
   160 
   161 val Un		= Const("op Un", [iT,iT]--->iT)
   162 and empty	= Const("0", iT)
   163 and univ	= Const("univ", iT-->iT)
   164 and quniv	= Const("quniv", iT-->iT);
   165 
   166 (*Make a datatype's domain: form the union of its set parameters*)
   167 fun union_params rec_tm =
   168   let val (_,args) = strip_comb rec_tm
   169   in  case (filter (fn arg => type_of arg = iT) args) of
   170          []    => empty
   171        | iargs => fold_bal (app Un) iargs
   172   end;
   173 
   174 fun data_domain rec_tms =
   175   replicate (length rec_tms) (univ $ union_params (hd rec_tms));
   176 
   177 fun Codata_domain rec_tms =
   178   replicate (length rec_tms) (quniv $ union_params (hd rec_tms));
   179 
   180 (*Could go to FOL, but it's hardly general*)
   181 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
   182  (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
   183 
   184 val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
   185   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
   186 
   187 (*Delete needless equality assumptions*)
   188 val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
   189      (fn _ => [assume_tac 1]);
   190 
   191 end;
   192