src/ZF/ind_syntax.ML
author wenzelm
Sun Feb 07 19:33:34 2010 +0100 (2010-02-07)
changeset 35021 c839a4c670c6
parent 33317 b4534348b8fd
child 35129 ed24ba6f69aa
permissions -rw-r--r--
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm@12243
     1
(*  Title:      ZF/ind_syntax.ML
clasohm@1461
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1993  University of Cambridge
clasohm@0
     4
wenzelm@12243
     5
Abstract Syntax functions for Inductive Definitions.
clasohm@0
     6
*)
clasohm@0
     7
lcp@516
     8
structure Ind_Syntax =
lcp@516
     9
struct
clasohm@0
    10
paulson@4804
    11
(*Print tracing messages during processing of "inductive" theory sections*)
wenzelm@32740
    12
val trace = Unsynchronized.ref false;
paulson@4804
    13
wenzelm@26189
    14
fun traceIt msg thy t =
wenzelm@26939
    15
  if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
wenzelm@17988
    16
  else t;
wenzelm@17988
    17
paulson@6053
    18
paulson@4352
    19
(** Abstract syntax definitions for ZF **)
clasohm@0
    20
paulson@4352
    21
val iT = Type("i",[]);
clasohm@0
    22
clasohm@0
    23
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
wenzelm@26189
    24
fun mk_all_imp (A,P) =
wenzelm@26189
    25
    FOLogic.all_const iT $
wenzelm@26189
    26
      Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
wenzelm@32960
    27
                   Term.betapply(P, Bound 0));
clasohm@0
    28
wenzelm@26189
    29
fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
clasohm@0
    30
lcp@516
    31
(*simple error-checking in the premises of an inductive definition*)
wenzelm@26189
    32
fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
clasohm@1461
    33
        error"Premises may not be conjuctive"
wenzelm@26189
    34
  | chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
wenzelm@22567
    35
        (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
wenzelm@26189
    36
  | chk_prem rec_hd t =
wenzelm@22567
    37
        (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
lcp@516
    38
lcp@14
    39
(*Return the conclusion of a rule, of the form t:X*)
wenzelm@26189
    40
fun rule_concl rl =
wenzelm@26189
    41
    let val Const (@{const_name Trueprop}, _) $ (Const (@{const_name mem}, _) $ t $ X) =
clasohm@1461
    42
                Logic.strip_imp_concl rl
lcp@435
    43
    in  (t,X)  end;
lcp@435
    44
lcp@435
    45
(*As above, but return error message if bad*)
lcp@435
    46
fun rule_concl_msg sign rl = rule_concl rl
wenzelm@26189
    47
    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
wenzelm@26939
    48
                          Syntax.string_of_term_global sign rl);
clasohm@0
    49
clasohm@0
    50
(*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
clasohm@0
    51
  read_instantiate replaces a propositional variable by a formula variable*)
wenzelm@26189
    52
val equals_CollectD =
wenzelm@27239
    53
    read_instantiate @{context} [(("W", 0), "?Q")]
wenzelm@24893
    54
        (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
clasohm@0
    55
clasohm@0
    56
lcp@516
    57
(** For datatype definitions **)
lcp@516
    58
paulson@6053
    59
(*Constructor name, type, mixfix info;
paulson@6053
    60
  internal name from mixfix, datatype sets, full premises*)
wenzelm@26189
    61
type constructor_spec =
wenzelm@26189
    62
    (string * typ * mixfix) * string * term list * term list;
paulson@6053
    63
wenzelm@26189
    64
fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A)
lcp@516
    65
  | dest_mem _ = error "Constructor specifications must have the form x:A";
lcp@516
    66
lcp@516
    67
(*read a constructor specification*)
wenzelm@27261
    68
fun read_construct ctxt (id, sprems, syn) =
wenzelm@27261
    69
    let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
wenzelm@27261
    70
          |> Syntax.check_terms ctxt
clasohm@1461
    71
        val args = map (#1 o dest_mem) prems
clasohm@1461
    72
        val T = (map (#2 o dest_Free) args) ---> iT
wenzelm@26189
    73
                handle TERM _ => error
clasohm@1461
    74
                    "Bad variable in constructor specification"
wenzelm@30345
    75
        val name = Syntax.const_name syn id
lcp@516
    76
    in ((id,T,syn), name, args, prems) end;
lcp@516
    77
lcp@516
    78
val read_constructs = map o map o read_construct;
clasohm@0
    79
lcp@516
    80
(*convert constructor specifications into introduction rules*)
wenzelm@3925
    81
fun mk_intr_tms sg (rec_tm, constructs) =
wenzelm@3925
    82
  let
wenzelm@3925
    83
    fun mk_intr ((id,T,syn), name, args, prems) =
wenzelm@3925
    84
      Logic.list_implies
paulson@4352
    85
        (map FOLogic.mk_Trueprop prems,
wenzelm@32960
    86
         FOLogic.mk_Trueprop
wenzelm@32960
    87
            (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
wenzelm@32960
    88
                       $ rec_tm))
lcp@516
    89
  in  map mk_intr constructs  end;
lcp@516
    90
wenzelm@32952
    91
fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
clasohm@0
    92
wenzelm@26189
    93
fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;
clasohm@0
    94
lcp@516
    95
(*Make a datatype's domain: form the union of its set parameters*)
paulson@6112
    96
fun union_params (rec_tm, cs) =
lcp@516
    97
  let val (_,args) = strip_comb rec_tm
paulson@6112
    98
      fun is_ind arg = (type_of arg = iT)
wenzelm@33317
    99
  in  case filter is_ind (args @ cs) of
wenzelm@33317
   100
         [] => @{const 0}
wenzelm@32765
   101
       | u_args => Balanced_Tree.make mk_Un u_args
lcp@516
   102
  end;
lcp@516
   103
clasohm@0
   104
paulson@1418
   105
(*Includes rules for succ and Pair since they are common constructions*)
wenzelm@26189
   106
val elim_rls =
wenzelm@26189
   107
  [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0},
wenzelm@26189
   108
   @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject},
wenzelm@26189
   109
   make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}];
paulson@1418
   110
wenzelm@7694
   111
wenzelm@7694
   112
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
wenzelm@7694
   113
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
wenzelm@7694
   114
  | tryres (th, []) = raise THM("tryres", 0, [th]);
wenzelm@7694
   115
wenzelm@26189
   116
fun gen_make_elim elim_rls rl =
wenzelm@35021
   117
  Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
wenzelm@7694
   118
paulson@1418
   119
(*Turns iff rules into safe elimination rules*)
wenzelm@26189
   120
fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
paulson@1418
   121
lcp@516
   122
end;
lcp@516
   123