src/ZF/ind_syntax.ML
author paulson
Fri, 22 Dec 1995 11:09:28 +0100
changeset 1418 f5f97ee67cbb
parent 742 faa3efc1d130
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule. intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of generating a new one. Inductive defs no longer export sumprod_free_SEs ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store. Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items no longer exported. mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ind-syntax.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Abstract Syntax functions for Inductive Definitions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
     9
(*The structure protects these items from redeclaration (somewhat!).  The 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    10
  datatype definitions in theory files refer to these items by name!
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    11
*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    12
structure Ind_Syntax =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    13
struct
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(** Abstract syntax definitions for FOL and ZF **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val iT = Type("i",[])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
and oT = Type("o",[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
(*Given u expecting arguments of types [T1,...,Tn], create term of 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  type T1*...*Tn => i using split*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
fun ap_split split u [ ]   = Abs("null", iT, u)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  | ap_split split u [_]   = u
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  | ap_split split u [_,_] = split $ u
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  | ap_split split u (T::Ts) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
      split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val conj = Const("op &", [oT,oT]--->oT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
and disj = Const("op |", [oT,oT]--->oT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
and imp = Const("op -->", [oT,oT]--->oT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
val eq_const = Const("op =", [iT,iT]--->oT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val mem_const = Const("op :", [iT,iT]--->oT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val exists_const = Const("Ex", [iT-->oT]--->oT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val all_const = Const("All", [iT-->oT]--->oT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
fun mk_all_imp (A,P) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
    all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val Trueprop = Const("Trueprop",oT-->propT);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun mk_tprop P = Trueprop $ P;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    54
(*simple error-checking in the premises of an inductive definition*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    55
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    56
	error"Premises may not be conjuctive"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    57
  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    58
	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    59
  | chk_prem rec_hd t = 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    60
	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    61
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    62
(*Return the conclusion of a rule, of the form t:X*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
fun rule_concl rl = 
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    64
    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    65
		Logic.strip_imp_concl rl
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    66
    in  (t,X)  end;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    67
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    68
(*As above, but return error message if bad*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    69
fun rule_concl_msg sign rl = rule_concl rl
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    70
    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    71
			  Sign.string_of_term sign rl);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
(*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  read_instantiate replaces a propositional variable by a formula variable*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val equals_CollectD = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    read_instantiate [("W","?Q")]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
        (make_elim (equalityD1 RS subsetD RS CollectD2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    80
(** For datatype definitions **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    81
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    82
fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    83
  | dest_mem _ = error "Constructor specifications must have the form x:A";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    84
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    85
(*read a constructor specification*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    86
fun read_construct sign (id, sprems, syn) =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    87
    let val prems = map (readtm sign oT) sprems
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    88
	val args = map (#1 o dest_mem) prems
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    89
	val T = (map (#2 o dest_Free) args) ---> iT
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    90
		handle TERM _ => error 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    91
		    "Bad variable in constructor specification"
568
756b0e2a6cac replaced Lexicon.scan_id by Scanner.scan_id;
wenzelm
parents: 543
diff changeset
    92
        val name = Syntax.const_name id syn  (*handle infix constructors*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    93
    in ((id,T,syn), name, args, prems) end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    94
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    95
val read_constructs = map o map o read_construct;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    97
(*convert constructor specifications into introduction rules*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    98
fun mk_intr_tms (rec_tm, constructs) =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    99
  let fun mk_intr ((id,T,syn), name, args, prems) =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   100
	  Logic.list_implies
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   101
	      (map mk_tprop prems,
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   102
	       mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   103
  in  map mk_intr constructs  end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   104
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   105
val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   107
val Un		= Const("op Un", [iT,iT]--->iT)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   108
and empty	= Const("0", iT)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   109
and univ	= Const("univ", iT-->iT)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   110
and quniv	= Const("quniv", iT-->iT);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   112
(*Make a datatype's domain: form the union of its set parameters*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   113
fun union_params rec_tm =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   114
  let val (_,args) = strip_comb rec_tm
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   115
  in  case (filter (fn arg => type_of arg = iT) args) of
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   116
         []    => empty
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   117
       | iargs => fold_bal (app Un) iargs
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   118
  end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   119
742
faa3efc1d130 data_domain,Codata_domain: removed replicate; now return one
lcp
parents: 578
diff changeset
   120
(*Previously these both did    replicate (length rec_tms);  however now
faa3efc1d130 data_domain,Codata_domain: removed replicate; now return one
lcp
parents: 578
diff changeset
   121
  [q]univ itself constitutes the sum domain for mutual recursion!*)
faa3efc1d130 data_domain,Codata_domain: removed replicate; now return one
lcp
parents: 578
diff changeset
   122
fun data_domain rec_tms = univ $ union_params (hd rec_tms);
faa3efc1d130 data_domain,Codata_domain: removed replicate; now return one
lcp
parents: 578
diff changeset
   123
fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*Could go to FOL, but it's hardly general*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   126
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   127
 (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
  (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 14
diff changeset
   132
(*Delete needless equality assumptions*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 14
diff changeset
   133
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 14
diff changeset
   134
     (fn _ => [assume_tac 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   136
(*Includes rules for succ and Pair since they are common constructions*)
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   137
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   138
		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   139
		make_elim succ_inject, 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   140
		refl_thin, conjE, exE, disjE];
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   141
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   142
(*Turns iff rules into safe elimination rules*)
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   143
fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   144
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   145
end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   146