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