src/ZF/ind_syntax.ML
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 44241 7943b69f0188
child 55143 04448228381d
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12243
wenzelm
parents: 8819
diff changeset
     1
(*  Title:      ZF/ind_syntax.ML
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
12243
wenzelm
parents: 8819
diff changeset
     5
Abstract Syntax functions for Inductive Definitions.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
     8
structure Ind_Syntax =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
     9
struct
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
4804
02b7c759159b Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents: 4352
diff changeset
    11
(*Print tracing messages during processing of "inductive" theory sections*)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30345
diff changeset
    12
val trace = Unsynchronized.ref false;
4804
02b7c759159b Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents: 4352
diff changeset
    13
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    14
fun traceIt msg thy t =
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26189
diff changeset
    15
  if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
17988
47f81afce1b4 traceIt: plain term;
wenzelm
parents: 16867
diff changeset
    16
  else t;
47f81afce1b4 traceIt: plain term;
wenzelm
parents: 16867
diff changeset
    17
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 4972
diff changeset
    18
4352
7ac9f3e8a97d Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents: 3925
diff changeset
    19
(** Abstract syntax definitions for ZF **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
38514
bd9c4e8281ec deglobalization
haftmann
parents: 37145
diff changeset
    21
val iT = Type(@{type_name i}, []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    24
fun mk_all_imp (A,P) =
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    25
    FOLogic.all_const iT $
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    26
      Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32957
diff changeset
    27
                   Term.betapply(P, Bound 0));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41310
diff changeset
    29
fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT) t;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    31
(*simple error-checking in the premises of an inductive definition*)
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 39288
diff changeset
    32
fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    33
        error"Premises may not be conjuctive"
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    34
  | chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
22567
1565d476a9e2 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents: 21539
diff changeset
    35
        (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    36
  | chk_prem rec_hd t =
22567
1565d476a9e2 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents: 21539
diff changeset
    37
        (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    38
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    39
(*Return the conclusion of a rule, of the form t:X*)
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    40
fun rule_concl rl =
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    41
    let val Const (@{const_name Trueprop}, _) $ (Const (@{const_name mem}, _) $ t $ X) =
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    42
                Logic.strip_imp_concl rl
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    43
    in  (t,X)  end;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    44
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    45
(*As above, but return error message if bad*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 231
diff changeset
    46
fun rule_concl_msg sign rl = rule_concl rl
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    47
    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26189
diff changeset
    48
                          Syntax.string_of_term_global sign rl);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
(*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  read_instantiate replaces a propositional variable by a formula variable*)
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    52
val equals_CollectD =
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27230
diff changeset
    53
    read_instantiate @{context} [(("W", 0), "?Q")]
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24826
diff changeset
    54
        (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    57
(** For datatype definitions **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    58
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 4972
diff changeset
    59
(*Constructor name, type, mixfix info;
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 4972
diff changeset
    60
  internal name from mixfix, datatype sets, full premises*)
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    61
type constructor_spec =
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    62
    (string * typ * mixfix) * string * term list * term list;
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 4972
diff changeset
    63
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    64
fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    65
  | dest_mem _ = error "Constructor specifications must have the form x:A";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    66
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    67
(*read a constructor specification*)
35129
ed24ba6f69aa discontinued unnamed infix syntax;
wenzelm
parents: 35021
diff changeset
    68
fun read_construct ctxt (id: string, sprems, syn: mixfix) =
39288
f1ae2493d93f eliminated aliases of Type.constraint;
wenzelm
parents: 38514
diff changeset
    69
    let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
27261
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 27239
diff changeset
    70
          |> Syntax.check_terms ctxt
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    71
        val args = map (#1 o dest_mem) prems
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    72
        val T = (map (#2 o dest_Free) args) ---> iT
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    73
                handle TERM _ => error
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1418
diff changeset
    74
                    "Bad variable in constructor specification"
35129
ed24ba6f69aa discontinued unnamed infix syntax;
wenzelm
parents: 35021
diff changeset
    75
    in ((id,T,syn), id, args, prems) end;
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    76
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    77
val read_constructs = map o map o read_construct;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    79
(*convert constructor specifications into introduction rules*)
3925
90f499226ab9 (co) inductive / datatype package adapted to qualified names;
wenzelm
parents: 2266
diff changeset
    80
fun mk_intr_tms sg (rec_tm, constructs) =
90f499226ab9 (co) inductive / datatype package adapted to qualified names;
wenzelm
parents: 2266
diff changeset
    81
  let
90f499226ab9 (co) inductive / datatype package adapted to qualified names;
wenzelm
parents: 2266
diff changeset
    82
    fun mk_intr ((id,T,syn), name, args, prems) =
90f499226ab9 (co) inductive / datatype package adapted to qualified names;
wenzelm
parents: 2266
diff changeset
    83
      Logic.list_implies
4352
7ac9f3e8a97d Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents: 3925
diff changeset
    84
        (map FOLogic.mk_Trueprop prems,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32957
diff changeset
    85
         FOLogic.mk_Trueprop
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32957
diff changeset
    86
            (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32957
diff changeset
    87
                       $ rec_tm))
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    88
  in  map mk_intr constructs  end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    89
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32765
diff changeset
    90
fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
    92
fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    94
(*Make a datatype's domain: form the union of its set parameters*)
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    95
fun union_params (rec_tm, cs) =
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
    96
  let val (_,args) = strip_comb rec_tm
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    97
      fun is_ind arg = (type_of arg = iT)
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 32960
diff changeset
    98
  in  case filter is_ind (args @ cs) of
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 39288
diff changeset
    99
         [] => @{const zero}
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 32740
diff changeset
   100
       | u_args => Balanced_Tree.make mk_Un u_args
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   101
  end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   102
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   104
(*Includes rules for succ and Pair since they are common constructions*)
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
   105
val elim_rls =
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
   106
  [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0},
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
   107
   @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject},
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
   108
   make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}];
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   109
7694
20121c9dc1a6 tryres, gen_make_elim moved here;
wenzelm
parents: 6112
diff changeset
   110
20121c9dc1a6 tryres, gen_make_elim moved here;
wenzelm
parents: 6112
diff changeset
   111
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
20121c9dc1a6 tryres, gen_make_elim moved here;
wenzelm
parents: 6112
diff changeset
   112
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
20121c9dc1a6 tryres, gen_make_elim moved here;
wenzelm
parents: 6112
diff changeset
   113
  | tryres (th, []) = raise THM("tryres", 0, [th]);
20121c9dc1a6 tryres, gen_make_elim moved here;
wenzelm
parents: 6112
diff changeset
   114
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
   115
fun gen_make_elim elim_rls rl =
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33317
diff changeset
   116
  Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
7694
20121c9dc1a6 tryres, gen_make_elim moved here;
wenzelm
parents: 6112
diff changeset
   117
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   118
(*Turns iff rules into safe elimination rules*)
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26059
diff changeset
   119
fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 742
diff changeset
   120
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   121
end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 466
diff changeset
   122