src/ZF/ind_syntax.ML
author lcp
Fri Aug 12 12:51:34 1994 +0200 (1994-08-12)
changeset 516 1957113f0d7d
parent 466 08d1cce222e1
child 543 e961b2092869
permissions -rw-r--r--
installation of new inductive/datatype sections
clasohm@0
     1
(*  Title: 	ZF/ind-syntax.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Abstract Syntax functions for Inductive Definitions
clasohm@0
     7
*)
clasohm@0
     8
lcp@516
     9
(*The structure protects these items from redeclaration (somewhat!).  The 
lcp@516
    10
  datatype definitions in theory files refer to these items by name!
lcp@516
    11
*)
lcp@516
    12
structure Ind_Syntax =
lcp@516
    13
struct
lcp@516
    14
(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
lcp@516
    15
fun mk_defpair (lhs, rhs) = 
clasohm@454
    16
  let val Const(name, _) = head_of lhs
clasohm@0
    17
      val dummy = assert (term_vars rhs subset term_vars lhs
clasohm@454
    18
		          andalso
clasohm@454
    19
		          term_frees rhs subset term_frees lhs
clasohm@454
    20
		          andalso
clasohm@454
    21
		          term_tvars rhs subset term_tvars lhs
clasohm@454
    22
		          andalso
clasohm@454
    23
		          term_tfrees rhs subset term_tfrees lhs)
clasohm@0
    24
	          ("Extra variables on RHS in definition of " ^ name)
clasohm@454
    25
  in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
clasohm@0
    26
lcp@516
    27
fun get_def thy s = get_axiom thy (s^"_def");
lcp@516
    28
clasohm@0
    29
fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
clasohm@0
    30
clasohm@0
    31
(*export to Pure/library?  *)
clasohm@0
    32
fun assert_all pred l msg_fn = 
clasohm@0
    33
  let fun asl [] = ()
clasohm@0
    34
	| asl (x::xs) = if pred x then asl xs
clasohm@0
    35
	                else error (msg_fn x)
clasohm@0
    36
  in  asl l  end;
clasohm@0
    37
clasohm@0
    38
clasohm@0
    39
(** Abstract syntax definitions for FOL and ZF **)
clasohm@0
    40
clasohm@0
    41
val iT = Type("i",[])
clasohm@0
    42
and oT = Type("o",[]);
clasohm@0
    43
clasohm@0
    44
fun ap t u = t$u;
clasohm@0
    45
fun app t (u1,u2) = t $ u1 $ u2;
clasohm@0
    46
clasohm@0
    47
(*Given u expecting arguments of types [T1,...,Tn], create term of 
clasohm@0
    48
  type T1*...*Tn => i using split*)
clasohm@0
    49
fun ap_split split u [ ]   = Abs("null", iT, u)
clasohm@0
    50
  | ap_split split u [_]   = u
clasohm@0
    51
  | ap_split split u [_,_] = split $ u
clasohm@0
    52
  | ap_split split u (T::Ts) = 
clasohm@0
    53
      split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
clasohm@0
    54
clasohm@0
    55
val conj = Const("op &", [oT,oT]--->oT)
clasohm@0
    56
and disj = Const("op |", [oT,oT]--->oT)
clasohm@0
    57
and imp = Const("op -->", [oT,oT]--->oT);
clasohm@0
    58
clasohm@0
    59
val eq_const = Const("op =", [iT,iT]--->oT);
clasohm@0
    60
clasohm@0
    61
val mem_const = Const("op :", [iT,iT]--->oT);
clasohm@0
    62
clasohm@0
    63
val exists_const = Const("Ex", [iT-->oT]--->oT);
clasohm@0
    64
fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
clasohm@0
    65
clasohm@0
    66
val all_const = Const("All", [iT-->oT]--->oT);
clasohm@0
    67
fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
clasohm@0
    68
clasohm@0
    69
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
clasohm@0
    70
fun mk_all_imp (A,P) = 
clasohm@0
    71
    all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
clasohm@0
    72
clasohm@0
    73
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
clasohm@0
    74
clasohm@0
    75
val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
clasohm@0
    76
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
clasohm@0
    77
clasohm@0
    78
val Trueprop = Const("Trueprop",oT-->propT);
clasohm@0
    79
fun mk_tprop P = Trueprop $ P;
clasohm@0
    80
clasohm@0
    81
(*Prove a goal stated as a term, with exception handling*)
clasohm@0
    82
fun prove_term sign defs (P,tacsf) = 
lcp@231
    83
    let val ct = cterm_of sign P
clasohm@0
    84
    in  prove_goalw_cterm defs ct tacsf
clasohm@0
    85
	handle e => (writeln ("Exception in proof of\n" ^
lcp@231
    86
			       string_of_cterm ct); 
clasohm@0
    87
		     raise e)
clasohm@0
    88
    end;
clasohm@0
    89
clasohm@0
    90
(*Read an assumption in the given theory*)
lcp@231
    91
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
clasohm@0
    92
lcp@516
    93
fun readtm sign T a = 
lcp@516
    94
    read_cterm sign (a,T) |> term_of
lcp@516
    95
    handle ERROR => error ("The error above occurred for " ^ a);
lcp@516
    96
lcp@516
    97
(*Skipping initial blanks, find the first identifier*)
lcp@516
    98
fun scan_to_id s = 
lcp@516
    99
    s |> explode |> take_prefix is_blank |> #2 |> Lexicon.scan_id |> #1
lcp@516
   100
    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
lcp@516
   101
lcp@516
   102
fun is_backslash c = c = "\\";
lcp@516
   103
lcp@516
   104
(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
lcp@516
   105
  Does not handle the \ddd form;  no error checking*)
lcp@516
   106
fun escape [] = []
lcp@516
   107
  | escape cs = (case take_prefix (not o is_backslash) cs of
lcp@516
   108
	 (front, []) => front
lcp@516
   109
       | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
lcp@516
   110
       | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
lcp@516
   111
       | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
lcp@516
   112
       | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
lcp@516
   113
       | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
lcp@516
   114
       | (front, b::c::rest) => 
lcp@516
   115
	   if is_blank c   (*remove any further blanks and the following \ *)
lcp@516
   116
	   then front @ escape (tl (snd (take_prefix is_blank rest)))
lcp@516
   117
	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
lcp@516
   118
lcp@516
   119
(*Remove the first and last charaters -- presumed to be quotes*)
lcp@516
   120
val trim = implode o escape o rev o tl o rev o tl o explode;
lcp@516
   121
lcp@516
   122
(*simple error-checking in the premises of an inductive definition*)
lcp@516
   123
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
lcp@516
   124
	error"Premises may not be conjuctive"
lcp@516
   125
  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
lcp@516
   126
	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
lcp@516
   127
  | chk_prem rec_hd t = 
lcp@516
   128
	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
lcp@516
   129
lcp@516
   130
lcp@516
   131
(*Inverse of varifyT.  Move to Pure/type.ML?*)
lcp@516
   132
fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
lcp@516
   133
  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
lcp@516
   134
  | unvarifyT T = T;
lcp@516
   135
lcp@516
   136
(*Inverse of varify.  Move to Pure/logic.ML?*)
lcp@516
   137
fun unvarify (Const(a,T))    = Const(a, unvarifyT T)
lcp@516
   138
  | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
lcp@516
   139
  | unvarify (Var(ixn,T))    = Var(ixn, unvarifyT T)	(*non-zero index!*)
lcp@516
   140
  | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
lcp@516
   141
  | unvarify (f$t) = unvarify f $ unvarify t
lcp@516
   142
  | unvarify t = t;
lcp@516
   143
lcp@516
   144
clasohm@0
   145
(*Make distinct individual variables a1, a2, a3, ..., an. *)
clasohm@0
   146
fun mk_frees a [] = []
clasohm@0
   147
  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
clasohm@0
   148
lcp@14
   149
(*Return the conclusion of a rule, of the form t:X*)
clasohm@0
   150
fun rule_concl rl = 
lcp@435
   151
    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
lcp@435
   152
		Logic.strip_imp_concl rl
lcp@435
   153
    in  (t,X)  end;
lcp@435
   154
lcp@435
   155
(*As above, but return error message if bad*)
lcp@435
   156
fun rule_concl_msg sign rl = rule_concl rl
lcp@435
   157
    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
lcp@435
   158
			  Sign.string_of_term sign rl);
clasohm@0
   159
clasohm@0
   160
(*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
clasohm@0
   161
  read_instantiate replaces a propositional variable by a formula variable*)
clasohm@0
   162
val equals_CollectD = 
clasohm@0
   163
    read_instantiate [("W","?Q")]
clasohm@0
   164
        (make_elim (equalityD1 RS subsetD RS CollectD2));
clasohm@0
   165
clasohm@0
   166
clasohm@0
   167
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
clasohm@0
   168
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
clasohm@0
   169
  | tryres (th, []) = raise THM("tryres", 0, [th]);
clasohm@0
   170
clasohm@0
   171
fun gen_make_elim elim_rls rl = 
clasohm@0
   172
      standard (tryres (rl, elim_rls @ [revcut_rl]));
clasohm@0
   173
lcp@516
   174
(** For datatype definitions **)
lcp@516
   175
lcp@516
   176
fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
lcp@516
   177
  | dest_mem _ = error "Constructor specifications must have the form x:A";
lcp@516
   178
lcp@516
   179
(*read a constructor specification*)
lcp@516
   180
fun read_construct sign (id, sprems, syn) =
lcp@516
   181
    let val prems = map (readtm sign oT) sprems
lcp@516
   182
	val args = map (#1 o dest_mem) prems
lcp@516
   183
	val T = (map (#2 o dest_Free) args) ---> iT
lcp@516
   184
		handle TERM _ => error 
lcp@516
   185
		    "Bad variable in constructor specification"
lcp@516
   186
        val name = const_name id syn  (*handle infix constructors*)
lcp@516
   187
    in ((id,T,syn), name, args, prems) end;
lcp@516
   188
lcp@516
   189
val read_constructs = map o map o read_construct;
clasohm@0
   190
lcp@516
   191
(*convert constructor specifications into introduction rules*)
lcp@516
   192
fun mk_intr_tms (rec_tm, constructs) =
lcp@516
   193
  let fun mk_intr ((id,T,syn), name, args, prems) =
lcp@516
   194
	  Logic.list_implies
lcp@516
   195
	      (map mk_tprop prems,
lcp@516
   196
	       mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
lcp@516
   197
  in  map mk_intr constructs  end;
lcp@516
   198
lcp@516
   199
val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
clasohm@0
   200
lcp@516
   201
val Un		= Const("op Un", [iT,iT]--->iT)
lcp@516
   202
and empty	= Const("0", iT)
lcp@516
   203
and univ	= Const("univ", iT-->iT)
lcp@516
   204
and quniv	= Const("quniv", iT-->iT);
clasohm@0
   205
lcp@516
   206
(*Make a datatype's domain: form the union of its set parameters*)
lcp@516
   207
fun union_params rec_tm =
lcp@516
   208
  let val (_,args) = strip_comb rec_tm
lcp@516
   209
  in  case (filter (fn arg => type_of arg = iT) args) of
lcp@516
   210
         []    => empty
lcp@516
   211
       | iargs => fold_bal (app Un) iargs
lcp@516
   212
  end;
lcp@516
   213
lcp@516
   214
fun data_domain rec_tms =
lcp@516
   215
  replicate (length rec_tms) (univ $ union_params (hd rec_tms));
lcp@516
   216
lcp@516
   217
fun Codata_domain rec_tms =
lcp@516
   218
  replicate (length rec_tms) (quniv $ union_params (hd rec_tms));
clasohm@0
   219
clasohm@0
   220
(*Could go to FOL, but it's hardly general*)
lcp@516
   221
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
lcp@516
   222
 (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
clasohm@0
   223
clasohm@0
   224
val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
clasohm@0
   225
  (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
clasohm@0
   226
lcp@55
   227
(*Delete needless equality assumptions*)
lcp@55
   228
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
lcp@55
   229
     (fn _ => [assume_tac 1]);
clasohm@0
   230
lcp@516
   231
end;
lcp@516
   232