src/ZF/ind_syntax.ML
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 23419 8c30dd4b3b22
child 24826 78e6a3cea367
permissions -rw-r--r--
added Tools/lin_arith.ML;
wenzelm@12243
     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
wenzelm@12243
     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
paulson@4804
    15
(*Print tracing messages during processing of "inductive" theory sections*)
paulson@4804
    16
val trace = ref false;
paulson@4804
    17
wenzelm@17988
    18
fun traceIt msg thy t = 
wenzelm@17988
    19
  if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
wenzelm@17988
    20
  else t;
wenzelm@17988
    21
paulson@6053
    22
paulson@4352
    23
(** Abstract syntax definitions for ZF **)
clasohm@0
    24
paulson@4352
    25
val iT = Type("i",[]);
clasohm@0
    26
paulson@4352
    27
val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
clasohm@0
    28
clasohm@0
    29
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
clasohm@0
    30
fun mk_all_imp (A,P) = 
paulson@4352
    31
    FOLogic.all_const iT $ 
paulson@4972
    32
      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ 
wenzelm@18176
    33
	           Term.betapply(P, Bound 0));
clasohm@0
    34
clasohm@0
    35
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
clasohm@0
    36
paulson@6053
    37
val apply_const = Const("op `", [iT,iT]--->iT);
paulson@6053
    38
wenzelm@6093
    39
val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
paulson@6053
    40
paulson@4352
    41
val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
clasohm@0
    42
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
clasohm@0
    43
lcp@516
    44
(*simple error-checking in the premises of an inductive definition*)
lcp@516
    45
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
clasohm@1461
    46
        error"Premises may not be conjuctive"
lcp@516
    47
  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
wenzelm@22567
    48
        (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
lcp@516
    49
  | chk_prem rec_hd t = 
wenzelm@22567
    50
        (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
lcp@516
    51
lcp@14
    52
(*Return the conclusion of a rule, of the form t:X*)
clasohm@0
    53
fun rule_concl rl = 
lcp@435
    54
    let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
clasohm@1461
    55
                Logic.strip_imp_concl rl
lcp@435
    56
    in  (t,X)  end;
lcp@435
    57
lcp@435
    58
(*As above, but return error message if bad*)
lcp@435
    59
fun rule_concl_msg sign rl = rule_concl rl
lcp@435
    60
    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
clasohm@1461
    61
                          Sign.string_of_term sign rl);
clasohm@0
    62
clasohm@0
    63
(*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
clasohm@0
    64
  read_instantiate replaces a propositional variable by a formula variable*)
clasohm@0
    65
val equals_CollectD = 
clasohm@0
    66
    read_instantiate [("W","?Q")]
clasohm@0
    67
        (make_elim (equalityD1 RS subsetD RS CollectD2));
clasohm@0
    68
clasohm@0
    69
lcp@516
    70
(** For datatype definitions **)
lcp@516
    71
paulson@6053
    72
(*Constructor name, type, mixfix info;
paulson@6053
    73
  internal name from mixfix, datatype sets, full premises*)
paulson@6053
    74
type constructor_spec = 
paulson@6053
    75
    ((string * typ * mixfix) * string * term list * term list);
paulson@6053
    76
lcp@516
    77
fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
lcp@516
    78
  | dest_mem _ = error "Constructor specifications must have the form x:A";
lcp@516
    79
lcp@516
    80
(*read a constructor specification*)
lcp@516
    81
fun read_construct sign (id, sprems, syn) =
wenzelm@8819
    82
    let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
clasohm@1461
    83
        val args = map (#1 o dest_mem) prems
clasohm@1461
    84
        val T = (map (#2 o dest_Free) args) ---> iT
clasohm@1461
    85
                handle TERM _ => error 
clasohm@1461
    86
                    "Bad variable in constructor specification"
wenzelm@568
    87
        val name = Syntax.const_name id syn  (*handle infix constructors*)
lcp@516
    88
    in ((id,T,syn), name, args, prems) end;
lcp@516
    89
lcp@516
    90
val read_constructs = map o map o read_construct;
clasohm@0
    91
lcp@516
    92
(*convert constructor specifications into introduction rules*)
wenzelm@3925
    93
fun mk_intr_tms sg (rec_tm, constructs) =
wenzelm@3925
    94
  let
wenzelm@3925
    95
    fun mk_intr ((id,T,syn), name, args, prems) =
wenzelm@3925
    96
      Logic.list_implies
paulson@4352
    97
        (map FOLogic.mk_Trueprop prems,
paulson@4352
    98
	 FOLogic.mk_Trueprop
paulson@4352
    99
	    (mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
paulson@4352
   100
	               $ rec_tm))
lcp@516
   101
  in  map mk_intr constructs  end;
lcp@516
   102
wenzelm@3925
   103
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
clasohm@0
   104
wenzelm@7694
   105
fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
wenzelm@7694
   106
wenzelm@7694
   107
val empty       = Const("0", iT)
wenzelm@6093
   108
and univ        = Const("Univ.univ", iT-->iT)
wenzelm@6093
   109
and quniv       = Const("QUniv.quniv", iT-->iT);
clasohm@0
   110
lcp@516
   111
(*Make a datatype's domain: form the union of its set parameters*)
paulson@6112
   112
fun union_params (rec_tm, cs) =
lcp@516
   113
  let val (_,args) = strip_comb rec_tm
paulson@6112
   114
      fun is_ind arg = (type_of arg = iT)
skalberg@15570
   115
  in  case List.filter is_ind (args @ cs) of
paulson@6112
   116
         []     => empty
wenzelm@23419
   117
       | u_args => BalancedTree.make mk_Un u_args
lcp@516
   118
  end;
lcp@516
   119
paulson@6112
   120
(*univ or quniv constitutes the sum domain for mutual recursion;
paulson@6112
   121
  it is applied to the datatype parameters and to Consts occurring in the
paulson@6112
   122
  definition other than Nat.nat and the datatype sets themselves.
paulson@6112
   123
  FIXME: could insert all constant set expressions, e.g. nat->nat.*)
paulson@6112
   124
fun data_domain co (rec_tms, con_ty_lists) = 
paulson@13150
   125
    let val rec_hds = map head_of rec_tms
paulson@13150
   126
        val dummy = assert_all is_Const rec_hds
paulson@13150
   127
          (fn t => "Datatype set not previously declared as constant: " ^
wenzelm@23156
   128
                   Sign.string_of_term @{theory IFOL} t);
paulson@13150
   129
        val rec_names = (*nat doesn't have to be added*)
paulson@13150
   130
	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
paulson@6112
   131
	val u = if co then quniv else univ
wenzelm@16867
   132
	val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
wenzelm@16867
   133
          (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
wenzelm@16867
   134
            | _ => I)) con_ty_lists [];
paulson@6112
   135
    in  u $ union_params (hd rec_tms, cs)  end;
paulson@6112
   136
clasohm@0
   137
clasohm@0
   138
(*Could go to FOL, but it's hardly general*)
wenzelm@21539
   139
val def_swap_iff = prove_goal (the_context ()) "a==b ==> a=c <-> c=b"
wenzelm@21539
   140
  (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
clasohm@0
   141
wenzelm@21539
   142
val def_trans = prove_goal (the_context ()) "[| f==g;  g(a)=b |] ==> f(a)=b"
clasohm@0
   143
  (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
clasohm@0
   144
lcp@55
   145
(*Delete needless equality assumptions*)
wenzelm@21539
   146
val refl_thin = prove_goal (the_context ()) "!!P. [| a=a;  P |] ==> P"
lcp@55
   147
     (fn _ => [assume_tac 1]);
clasohm@0
   148
paulson@1418
   149
(*Includes rules for succ and Pair since they are common constructions*)
wenzelm@21539
   150
val elim_rls = [asm_rl, FalseE, thm "succ_neq_0", sym RS thm "succ_neq_0",
wenzelm@21539
   151
                thm "Pair_neq_0", sym RS thm "Pair_neq_0", thm "Pair_inject",
wenzelm@21539
   152
                make_elim (thm "succ_inject"),
clasohm@1461
   153
                refl_thin, conjE, exE, disjE];
paulson@1418
   154
wenzelm@7694
   155
wenzelm@7694
   156
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
wenzelm@7694
   157
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
wenzelm@7694
   158
  | tryres (th, []) = raise THM("tryres", 0, [th]);
wenzelm@7694
   159
wenzelm@7694
   160
fun gen_make_elim elim_rls rl = 
wenzelm@7694
   161
      standard (tryres (rl, elim_rls @ [revcut_rl]));
wenzelm@7694
   162
paulson@1418
   163
(*Turns iff rules into safe elimination rules*)
paulson@1418
   164
fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
paulson@1418
   165
lcp@516
   166
end;
lcp@516
   167
paulson@6112
   168
paulson@6112
   169
(*For convenient access by the user*)
paulson@6112
   170
val trace_induct = Ind_Syntax.trace;