author  wenzelm 
Fri, 17 Oct 1997 17:42:39 +0200  
changeset 3925  90f499226ab9 
parent 2266  82aef6857c5b 
child 4352  7ac9f3e8a97d 
permissions  rwrr 
1461  1 
(* Title: ZF/indsyntax.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 

15 
(** Abstract syntax definitions for FOL and ZF **) 

16 

17 
val iT = Type("i",[]) 

18 
and oT = Type("o",[]); 

19 

1738  20 

21 
(** Logical constants **) 

0  22 

23 
val conj = Const("op &", [oT,oT]>oT) 

24 
and disj = Const("op ", [oT,oT]>oT) 

25 
and imp = Const("op >", [oT,oT]>oT); 

26 

27 
val eq_const = Const("op =", [iT,iT]>oT); 

28 

29 
val mem_const = Const("op :", [iT,iT]>oT); 

30 

31 
val exists_const = Const("Ex", [iT>oT]>oT); 

32 
fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P)); 

33 

34 
val all_const = Const("All", [iT>oT]>oT); 

35 
fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P)); 

36 

37 
(*Creates All(%v.v:A > P(v)) rather than Ball(A,P) *) 

38 
fun mk_all_imp (A,P) = 

39 
all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0)); 

40 

41 
val Part_const = Const("Part", [iT,iT>iT]>iT); 

42 

43 
val Collect_const = Const("Collect", [iT,iT>oT]>iT); 

44 
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); 

45 

46 
val Trueprop = Const("Trueprop",oT>propT); 

47 
fun mk_tprop P = Trueprop $ P; 

48 

516  49 
(*simple errorchecking in the premises of an inductive definition*) 
50 
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = 

1461  51 
error"Premises may not be conjuctive" 
516  52 
 chk_prem rec_hd (Const("op :",_) $ t $ X) = 
1461  53 
deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" 
516  54 
 chk_prem rec_hd t = 
1461  55 
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; 
516  56 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

57 
(*Return the conclusion of a rule, of the form t:X*) 
0  58 
fun rule_concl rl = 
435  59 
let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
1461  60 
Logic.strip_imp_concl rl 
435  61 
in (t,X) end; 
62 

63 
(*As above, but return error message if bad*) 

64 
fun rule_concl_msg sign rl = rule_concl rl 

65 
handle Bind => error ("Illformed conclusion of introduction rule: " ^ 

1461  66 
Sign.string_of_term sign rl); 
0  67 

68 
(*For deriving cases rules. CollectD2 discards the domain, which is redundant; 

69 
read_instantiate replaces a propositional variable by a formula variable*) 

70 
val equals_CollectD = 

71 
read_instantiate [("W","?Q")] 

72 
(make_elim (equalityD1 RS subsetD RS CollectD2)); 

73 

74 

516  75 
(** For datatype definitions **) 
76 

77 
fun dest_mem (Const("op :",_) $ x $ A) = (x,A) 

78 
 dest_mem _ = error "Constructor specifications must have the form x:A"; 

79 

80 
(*read a constructor specification*) 

81 
fun read_construct sign (id, sprems, syn) = 

82 
let val prems = map (readtm sign oT) sprems 

1461  83 
val args = map (#1 o dest_mem) prems 
84 
val T = (map (#2 o dest_Free) args) > iT 

85 
handle TERM _ => error 

86 
"Bad variable in constructor specification" 

568  87 
val name = Syntax.const_name id syn (*handle infix constructors*) 
516  88 
in ((id,T,syn), name, args, prems) end; 
89 

90 
val read_constructs = map o map o read_construct; 

0  91 

516  92 
(*convert constructor specifications into introduction rules*) 
3925
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset

93 
fun mk_intr_tms sg (rec_tm, constructs) = 
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset

94 
let 
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset

95 
fun mk_intr ((id,T,syn), name, args, prems) = 
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset

96 
Logic.list_implies 
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset

97 
(map mk_tprop prems, 
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset

98 
mk_tprop (mem_const $ list_comb (Const (Sign.full_name sg name, T), args) $ rec_tm)) 
516  99 
in map mk_intr constructs end; 
100 

3925
90f499226ab9
(co) inductive / datatype package adapted to qualified names;
wenzelm
parents:
2266
diff
changeset

101 
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg); 
0  102 

1461  103 
val Un = Const("op Un", [iT,iT]>iT) 
104 
and empty = Const("0", iT) 

105 
and univ = Const("univ", iT>iT) 

106 
and quniv = Const("quniv", iT>iT); 

0  107 

516  108 
(*Make a datatype's domain: form the union of its set parameters*) 
109 
fun union_params rec_tm = 

110 
let val (_,args) = strip_comb rec_tm 

111 
in case (filter (fn arg => type_of arg = iT) args) of 

112 
[] => empty 

113 
 iargs => fold_bal (app Un) iargs 

114 
end; 

115 

742
faa3efc1d130
data_domain,Codata_domain: removed replicate; now return one
lcp
parents:
578
diff
changeset

116 
(*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

117 
[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

118 
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

119 
fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms); 
0  120 

121 
(*Could go to FOL, but it's hardly general*) 

516  122 
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <> c=b" 
123 
(fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]); 

0  124 

125 
val def_trans = prove_goal IFOL.thy "[ f==g; g(a)=b ] ==> f(a)=b" 

126 
(fn [rew,prem] => [ rewtac rew, rtac prem 1 ]); 

127 

55  128 
(*Delete needless equality assumptions*) 
129 
val refl_thin = prove_goal IFOL.thy "!!P. [ a=a; P ] ==> P" 

130 
(fn _ => [assume_tac 1]); 

0  131 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset

132 
(*Includes rules for succ and Pair since they are common constructions*) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset

133 
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
1461  134 
Pair_neq_0, sym RS Pair_neq_0, Pair_inject, 
135 
make_elim succ_inject, 

136 
refl_thin, conjE, exE, disjE]; 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset

137 

f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset

138 
(*Turns iff rules into safe elimination rules*) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
742
diff
changeset

139 
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

140 

516  141 
end; 
142 