author | wenzelm |
Sun, 29 Nov 1998 13:16:47 +0100 | |
changeset 5989 | 9670dae0143d |
parent 4972 | 7fe1d30c1374 |
child 6053 | 8a1059aa01f0 |
permissions | -rw-r--r-- |
1461 | 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 |
||
6 |
Abstract Syntax functions for Inductive Definitions |
|
7 |
*) |
|
8 |
||
516 | 9 |
(*The structure protects these items from redeclaration (somewhat!). The |
10 |
datatype definitions in theory files refer to these items by name! |
|
11 |
*) |
|
12 |
structure Ind_Syntax = |
|
13 |
struct |
|
0 | 14 |
|
4804
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
15 |
(*Print tracing messages during processing of "inductive" theory sections*) |
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
16 |
val trace = ref false; |
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
17 |
|
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
18 |
(** Abstract syntax definitions for ZF **) |
0 | 19 |
|
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
20 |
val iT = Type("i",[]); |
0 | 21 |
|
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
22 |
val mem_const = Const("op :", [iT,iT]--->FOLogic.oT); |
0 | 23 |
|
24 |
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
|
25 |
fun mk_all_imp (A,P) = |
|
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
26 |
FOLogic.all_const iT $ |
4972
7fe1d30c1374
mk_all_imp: no longer creates goals that have beta-redexes
paulson
parents:
4804
diff
changeset
|
27 |
Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ |
7fe1d30c1374
mk_all_imp: no longer creates goals that have beta-redexes
paulson
parents:
4804
diff
changeset
|
28 |
betapply(P, Bound 0)); |
0 | 29 |
|
30 |
val Part_const = Const("Part", [iT,iT-->iT]--->iT); |
|
31 |
||
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
32 |
val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT); |
0 | 33 |
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); |
34 |
||
516 | 35 |
(*simple error-checking in the premises of an inductive definition*) |
36 |
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = |
|
1461 | 37 |
error"Premises may not be conjuctive" |
516 | 38 |
| chk_prem rec_hd (Const("op :",_) $ t $ X) = |
1461 | 39 |
deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" |
516 | 40 |
| chk_prem rec_hd t = |
1461 | 41 |
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; |
516 | 42 |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
43 |
(*Return the conclusion of a rule, of the form t:X*) |
0 | 44 |
fun rule_concl rl = |
435 | 45 |
let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = |
1461 | 46 |
Logic.strip_imp_concl rl |
435 | 47 |
in (t,X) end; |
48 |
||
49 |
(*As above, but return error message if bad*) |
|
50 |
fun rule_concl_msg sign rl = rule_concl rl |
|
51 |
handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ |
|
1461 | 52 |
Sign.string_of_term sign rl); |
0 | 53 |
|
54 |
(*For deriving cases rules. CollectD2 discards the domain, which is redundant; |
|
55 |
read_instantiate replaces a propositional variable by a formula variable*) |
|
56 |
val equals_CollectD = |
|
57 |
read_instantiate [("W","?Q")] |
|
58 |
(make_elim (equalityD1 RS subsetD RS CollectD2)); |
|
59 |
||
60 |
||
516 | 61 |
(** For datatype definitions **) |
62 |
||
63 |
fun dest_mem (Const("op :",_) $ x $ A) = (x,A) |
|
64 |
| dest_mem _ = error "Constructor specifications must have the form x:A"; |
|
65 |
||
66 |
(*read a constructor specification*) |
|
67 |
fun read_construct sign (id, sprems, syn) = |
|
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
68 |
let val prems = map (readtm sign FOLogic.oT) sprems |
1461 | 69 |
val args = map (#1 o dest_mem) prems |
70 |
val T = (map (#2 o dest_Free) args) ---> iT |
|
71 |
handle TERM _ => error |
|
72 |
"Bad variable in constructor specification" |
|
568 | 73 |
val name = Syntax.const_name id syn (*handle infix constructors*) |
516 | 74 |
in ((id,T,syn), name, args, prems) end; |
75 |
||
76 |
val read_constructs = map o map o read_construct; |
|
0 | 77 |
|
516 | 78 |
(*convert constructor specifications into introduction rules*) |
3925
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
79 |
fun mk_intr_tms sg (rec_tm, constructs) = |
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
80 |
let |
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
81 |
fun mk_intr ((id,T,syn), name, args, prems) = |
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
82 |
Logic.list_implies |
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
83 |
(map FOLogic.mk_Trueprop prems, |
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
84 |
FOLogic.mk_Trueprop |
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
85 |
(mem_const $ list_comb (Const (Sign.full_name sg name, T), args) |
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset
|
86 |
$ rec_tm)) |
516 | 87 |
in map mk_intr constructs end; |
88 |
||
3925
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset
|
89 |
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg); |
0 | 90 |
|
1461 | 91 |
val Un = Const("op Un", [iT,iT]--->iT) |
92 |
and empty = Const("0", iT) |
|
93 |
and univ = Const("univ", iT-->iT) |
|
94 |
and quniv = Const("quniv", iT-->iT); |
|
0 | 95 |
|
516 | 96 |
(*Make a datatype's domain: form the union of its set parameters*) |
97 |
fun union_params rec_tm = |
|
98 |
let val (_,args) = strip_comb rec_tm |
|
99 |
in case (filter (fn arg => type_of arg = iT) args) of |
|
100 |
[] => empty |
|
101 |
| iargs => fold_bal (app Un) iargs |
|
102 |
end; |
|
103 |
||
742
faa3efc1d130
data_domain,Codata_domain: removed replicate; now return one
lcp
parents:
578
diff
changeset
|
104 |
(*Previously these both did replicate (length rec_tms); however now |
faa3efc1d130
data_domain,Codata_domain: removed replicate; now return one
lcp
parents:
578
diff
changeset
|
105 |
[q]univ itself constitutes the sum domain for mutual recursion!*) |
faa3efc1d130
data_domain,Codata_domain: removed replicate; now return one
lcp
parents:
578
diff
changeset
|
106 |
fun data_domain rec_tms = univ $ union_params (hd rec_tms); |
faa3efc1d130
data_domain,Codata_domain: removed replicate; now return one
lcp
parents:
578
diff
changeset
|
107 |
fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms); |
0 | 108 |
|
109 |
(*Could go to FOL, but it's hardly general*) |
|
516 | 110 |
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b" |
111 |
(fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]); |
|
0 | 112 |
|
113 |
val def_trans = prove_goal IFOL.thy "[| f==g; g(a)=b |] ==> f(a)=b" |
|
114 |
(fn [rew,prem] => [ rewtac rew, rtac prem 1 ]); |
|
115 |
||
55 | 116 |
(*Delete needless equality assumptions*) |
117 |
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P" |
|
118 |
(fn _ => [assume_tac 1]); |
|
0 | 119 |
|
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
120 |
(*Includes rules for succ and Pair since they are common constructions*) |
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
121 |
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, |
1461 | 122 |
Pair_neq_0, sym RS Pair_neq_0, Pair_inject, |
123 |
make_elim succ_inject, |
|
124 |
refl_thin, conjE, exE, disjE]; |
|
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
125 |
|
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
126 |
(*Turns iff rules into safe elimination rules*) |
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
127 |
fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]); |
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset
|
128 |
|
516 | 129 |
end; |
130 |
||
4804
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
131 |
|
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset
|
132 |
val trace_induct = Ind_Syntax.trace; |