author | wenzelm |
Thu, 19 Jun 2008 20:48:01 +0200 | |
changeset 27277 | 7b7ce2d7fafe |
parent 27261 | 5b3101338f42 |
child 28965 | 1de908189869 |
permissions | -rw-r--r-- |
12243 | 1 |
(* Title: ZF/ind_syntax.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
12243 | 6 |
Abstract Syntax functions for Inductive Definitions. |
0 | 7 |
*) |
8 |
||
516 | 9 |
structure Ind_Syntax = |
10 |
struct |
|
0 | 11 |
|
4804
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
12 |
(*Print tracing messages during processing of "inductive" theory sections*) |
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
13 |
val trace = ref false; |
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
14 |
|
26189 | 15 |
fun traceIt msg thy t = |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26189
diff
changeset
|
16 |
if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t) |
17988 | 17 |
else t; |
18 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset
|
19 |
|
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
20 |
(** Abstract syntax definitions for ZF **) |
0 | 21 |
|
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
22 |
val iT = Type("i",[]); |
0 | 23 |
|
24 |
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
|
26189 | 25 |
fun mk_all_imp (A,P) = |
26 |
FOLogic.all_const iT $ |
|
27 |
Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $ |
|
18176 | 28 |
Term.betapply(P, Bound 0)); |
0 | 29 |
|
26189 | 30 |
fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t); |
0 | 31 |
|
516 | 32 |
(*simple error-checking in the premises of an inductive definition*) |
26189 | 33 |
fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) = |
1461 | 34 |
error"Premises may not be conjuctive" |
26189 | 35 |
| 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
|
36 |
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ()) |
26189 | 37 |
| 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
|
38 |
(Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ()); |
516 | 39 |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
40 |
(*Return the conclusion of a rule, of the form t:X*) |
26189 | 41 |
fun rule_concl rl = |
42 |
let val Const (@{const_name Trueprop}, _) $ (Const (@{const_name mem}, _) $ t $ X) = |
|
1461 | 43 |
Logic.strip_imp_concl rl |
435 | 44 |
in (t,X) end; |
45 |
||
46 |
(*As above, but return error message if bad*) |
|
47 |
fun rule_concl_msg sign rl = rule_concl rl |
|
26189 | 48 |
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
|
49 |
Syntax.string_of_term_global sign rl); |
0 | 50 |
|
51 |
(*For deriving cases rules. CollectD2 discards the domain, which is redundant; |
|
52 |
read_instantiate replaces a propositional variable by a formula variable*) |
|
26189 | 53 |
val equals_CollectD = |
27239 | 54 |
read_instantiate @{context} [(("W", 0), "?Q")] |
24893 | 55 |
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2})); |
0 | 56 |
|
57 |
||
516 | 58 |
(** For datatype definitions **) |
59 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset
|
60 |
(*Constructor name, type, mixfix info; |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset
|
61 |
internal name from mixfix, datatype sets, full premises*) |
26189 | 62 |
type constructor_spec = |
63 |
(string * typ * mixfix) * string * term list * term list; |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset
|
64 |
|
26189 | 65 |
fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A) |
516 | 66 |
| dest_mem _ = error "Constructor specifications must have the form x:A"; |
67 |
||
68 |
(*read a constructor specification*) |
|
27261
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
27239
diff
changeset
|
69 |
fun read_construct ctxt (id, sprems, syn) = |
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
27239
diff
changeset
|
70 |
let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems |
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
27239
diff
changeset
|
71 |
|> Syntax.check_terms ctxt |
1461 | 72 |
val args = map (#1 o dest_mem) prems |
73 |
val T = (map (#2 o dest_Free) args) ---> iT |
|
26189 | 74 |
handle TERM _ => error |
1461 | 75 |
"Bad variable in constructor specification" |
568 | 76 |
val name = Syntax.const_name id syn (*handle infix constructors*) |
516 | 77 |
in ((id,T,syn), name, args, prems) end; |
78 |
||
79 |
val read_constructs = map o map o read_construct; |
|
0 | 80 |
|
516 | 81 |
(*convert constructor specifications into introduction rules*) |
3925
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
82 |
fun mk_intr_tms sg (rec_tm, constructs) = |
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
83 |
let |
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
84 |
fun mk_intr ((id,T,syn), name, args, prems) = |
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
85 |
Logic.list_implies |
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
86 |
(map FOLogic.mk_Trueprop prems, |
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
87 |
FOLogic.mk_Trueprop |
26189 | 88 |
(@{const mem} $ list_comb (Const (Sign.full_name sg name, T), args) |
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
89 |
$ rec_tm)) |
516 | 90 |
in map mk_intr constructs end; |
91 |
||
3925
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
92 |
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg); |
0 | 93 |
|
26189 | 94 |
fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2; |
0 | 95 |
|
516 | 96 |
(*Make a datatype's domain: form the union of its set parameters*) |
6112 | 97 |
fun union_params (rec_tm, cs) = |
516 | 98 |
let val (_,args) = strip_comb rec_tm |
6112 | 99 |
fun is_ind arg = (type_of arg = iT) |
15570 | 100 |
in case List.filter is_ind (args @ cs) of |
26189 | 101 |
[] => @{const 0} |
23419 | 102 |
| u_args => BalancedTree.make mk_Un u_args |
516 | 103 |
end; |
104 |
||
0 | 105 |
|
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
106 |
(*Includes rules for succ and Pair since they are common constructions*) |
26189 | 107 |
val elim_rls = |
108 |
[@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0}, |
|
109 |
@{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject}, |
|
110 |
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
|
111 |
|
7694 | 112 |
|
113 |
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*) |
|
114 |
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) |
|
115 |
| tryres (th, []) = raise THM("tryres", 0, [th]); |
|
116 |
||
26189 | 117 |
fun gen_make_elim elim_rls rl = |
7694 | 118 |
standard (tryres (rl, elim_rls @ [revcut_rl])); |
119 |
||
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
120 |
(*Turns iff rules into safe elimination rules*) |
26189 | 121 |
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
|
122 |
|
516 | 123 |
end; |
124 |