src/ZF/ind_syntax.ML
author clasohm
Tue Jan 30 13:42:57 1996 +0100 (1996-01-30)
changeset 1461 6bcb44e4d6e5
parent 1418 f5f97ee67cbb
child 1738 a70a5bc5e315
permissions -rw-r--r--
expanded tabs
clasohm@1461
     1
(*  Title:      ZF/ind-syntax.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     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
clasohm@0
    14
clasohm@0
    15
(** Abstract syntax definitions for FOL and ZF **)
clasohm@0
    16
clasohm@0
    17
val iT = Type("i",[])
clasohm@0
    18
and oT = Type("o",[]);
clasohm@0
    19
clasohm@0
    20
(*Given u expecting arguments of types [T1,...,Tn], create term of 
clasohm@0
    21
  type T1*...*Tn => i using split*)
clasohm@0
    22
fun ap_split split u [ ]   = Abs("null", iT, u)
clasohm@0
    23
  | ap_split split u [_]   = u
clasohm@0
    24
  | ap_split split u [_,_] = split $ u
clasohm@0
    25
  | ap_split split u (T::Ts) = 
clasohm@0
    26
      split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
clasohm@0
    27
clasohm@0
    28
val conj = Const("op &", [oT,oT]--->oT)
clasohm@0
    29
and disj = Const("op |", [oT,oT]--->oT)
clasohm@0
    30
and imp = Const("op -->", [oT,oT]--->oT);
clasohm@0
    31
clasohm@0
    32
val eq_const = Const("op =", [iT,iT]--->oT);
clasohm@0
    33
clasohm@0
    34
val mem_const = Const("op :", [iT,iT]--->oT);
clasohm@0
    35
clasohm@0
    36
val exists_const = Const("Ex", [iT-->oT]--->oT);
clasohm@0
    37
fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
clasohm@0
    38
clasohm@0
    39
val all_const = Const("All", [iT-->oT]--->oT);
clasohm@0
    40
fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
clasohm@0
    41
clasohm@0
    42
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
clasohm@0
    43
fun mk_all_imp (A,P) = 
clasohm@0
    44
    all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
clasohm@0
    45
clasohm@0
    46
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
clasohm@0
    47
clasohm@0
    48
val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
clasohm@0
    49
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
clasohm@0
    50
clasohm@0
    51
val Trueprop = Const("Trueprop",oT-->propT);
clasohm@0
    52
fun mk_tprop P = Trueprop $ P;
clasohm@0
    53
lcp@516
    54
(*simple error-checking in the premises of an inductive definition*)
lcp@516
    55
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
clasohm@1461
    56
        error"Premises may not be conjuctive"
lcp@516
    57
  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
clasohm@1461
    58
        deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
lcp@516
    59
  | chk_prem rec_hd t = 
clasohm@1461
    60
        deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
lcp@516
    61
lcp@14
    62
(*Return the conclusion of a rule, of the form t:X*)
clasohm@0
    63
fun rule_concl rl = 
lcp@435
    64
    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
clasohm@1461
    65
                Logic.strip_imp_concl rl
lcp@435
    66
    in  (t,X)  end;
lcp@435
    67
lcp@435
    68
(*As above, but return error message if bad*)
lcp@435
    69
fun rule_concl_msg sign rl = rule_concl rl
lcp@435
    70
    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
clasohm@1461
    71
                          Sign.string_of_term sign rl);
clasohm@0
    72
clasohm@0
    73
(*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
clasohm@0
    74
  read_instantiate replaces a propositional variable by a formula variable*)
clasohm@0
    75
val equals_CollectD = 
clasohm@0
    76
    read_instantiate [("W","?Q")]
clasohm@0
    77
        (make_elim (equalityD1 RS subsetD RS CollectD2));
clasohm@0
    78
clasohm@0
    79
lcp@516
    80
(** For datatype definitions **)
lcp@516
    81
lcp@516
    82
fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
lcp@516
    83
  | dest_mem _ = error "Constructor specifications must have the form x:A";
lcp@516
    84
lcp@516
    85
(*read a constructor specification*)
lcp@516
    86
fun read_construct sign (id, sprems, syn) =
lcp@516
    87
    let val prems = map (readtm sign oT) sprems
clasohm@1461
    88
        val args = map (#1 o dest_mem) prems
clasohm@1461
    89
        val T = (map (#2 o dest_Free) args) ---> iT
clasohm@1461
    90
                handle TERM _ => error 
clasohm@1461
    91
                    "Bad variable in constructor specification"
wenzelm@568
    92
        val name = Syntax.const_name id syn  (*handle infix constructors*)
lcp@516
    93
    in ((id,T,syn), name, args, prems) end;
lcp@516
    94
lcp@516
    95
val read_constructs = map o map o read_construct;
clasohm@0
    96
lcp@516
    97
(*convert constructor specifications into introduction rules*)
lcp@516
    98
fun mk_intr_tms (rec_tm, constructs) =
lcp@516
    99
  let fun mk_intr ((id,T,syn), name, args, prems) =
clasohm@1461
   100
          Logic.list_implies
clasohm@1461
   101
              (map mk_tprop prems,
clasohm@1461
   102
               mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
lcp@516
   103
  in  map mk_intr constructs  end;
lcp@516
   104
lcp@516
   105
val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
clasohm@0
   106
clasohm@1461
   107
val Un          = Const("op Un", [iT,iT]--->iT)
clasohm@1461
   108
and empty       = Const("0", iT)
clasohm@1461
   109
and univ        = Const("univ", iT-->iT)
clasohm@1461
   110
and quniv       = Const("quniv", iT-->iT);
clasohm@0
   111
lcp@516
   112
(*Make a datatype's domain: form the union of its set parameters*)
lcp@516
   113
fun union_params rec_tm =
lcp@516
   114
  let val (_,args) = strip_comb rec_tm
lcp@516
   115
  in  case (filter (fn arg => type_of arg = iT) args) of
lcp@516
   116
         []    => empty
lcp@516
   117
       | iargs => fold_bal (app Un) iargs
lcp@516
   118
  end;
lcp@516
   119
lcp@742
   120
(*Previously these both did    replicate (length rec_tms);  however now
lcp@742
   121
  [q]univ itself constitutes the sum domain for mutual recursion!*)
lcp@742
   122
fun data_domain rec_tms = univ $ union_params (hd rec_tms);
lcp@742
   123
fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
clasohm@0
   124
clasohm@0
   125
(*Could go to FOL, but it's hardly general*)
lcp@516
   126
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
lcp@516
   127
 (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
clasohm@0
   128
clasohm@0
   129
val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
clasohm@0
   130
  (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
clasohm@0
   131
lcp@55
   132
(*Delete needless equality assumptions*)
lcp@55
   133
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
lcp@55
   134
     (fn _ => [assume_tac 1]);
clasohm@0
   135
paulson@1418
   136
(*Includes rules for succ and Pair since they are common constructions*)
paulson@1418
   137
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
clasohm@1461
   138
                Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
clasohm@1461
   139
                make_elim succ_inject, 
clasohm@1461
   140
                refl_thin, conjE, exE, disjE];
paulson@1418
   141
paulson@1418
   142
(*Turns iff rules into safe elimination rules*)
paulson@1418
   143
fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
paulson@1418
   144
lcp@516
   145
end;
lcp@516
   146