author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1738  a70a5bc5e315 
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 

20 
(*Given u expecting arguments of types [T1,...,Tn], create term of 

21 
type T1*...*Tn => i using split*) 

22 
fun ap_split split u [ ] = Abs("null", iT, u) 

23 
 ap_split split u [_] = u 

24 
 ap_split split u [_,_] = split $ u 

25 
 ap_split split u (T::Ts) = 

26 
split $ (Abs("v", T, ap_split split (u $ Bound(length Ts  2)) Ts)); 

27 

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

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

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

31 

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

33 

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

35 

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

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

38 

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

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

41 

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

43 
fun mk_all_imp (A,P) = 

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

45 

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

47 

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

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

50 

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

52 
fun mk_tprop P = Trueprop $ P; 

53 

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

1461  56 
error"Premises may not be conjuctive" 
516  57 
 chk_prem rec_hd (Const("op :",_) $ t $ X) = 
1461  58 
deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" 
516  59 
 chk_prem rec_hd t = 
1461  60 
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; 
516  61 

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

62 
(*Return the conclusion of a rule, of the form t:X*) 
0  63 
fun rule_concl rl = 
435  64 
let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
1461  65 
Logic.strip_imp_concl rl 
435  66 
in (t,X) end; 
67 

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

69 
fun rule_concl_msg sign rl = rule_concl rl 

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

1461  71 
Sign.string_of_term sign rl); 
0  72 

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

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

75 
val equals_CollectD = 

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

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

78 

79 

516  80 
(** For datatype definitions **) 
81 

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

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

84 

85 
(*read a constructor specification*) 

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

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

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

90 
handle TERM _ => error 

91 
"Bad variable in constructor specification" 

568  92 
val name = Syntax.const_name id syn (*handle infix constructors*) 
516  93 
in ((id,T,syn), name, args, prems) end; 
94 

95 
val read_constructs = map o map o read_construct; 

0  96 

516  97 
(*convert constructor specifications into introduction rules*) 
98 
fun mk_intr_tms (rec_tm, constructs) = 

99 
let fun mk_intr ((id,T,syn), name, args, prems) = 

1461  100 
Logic.list_implies 
101 
(map mk_tprop prems, 

102 
mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 

516  103 
in map mk_intr constructs end; 
104 

105 
val mk_all_intr_tms = flat o map mk_intr_tms o op ~~; 

0  106 

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

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

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

0  111 

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

114 
let val (_,args) = strip_comb rec_tm 

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

116 
[] => empty 

117 
 iargs => fold_bal (app Un) iargs 

118 
end; 

119 

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

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

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

122 
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

123 
fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms); 
0  124 

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

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

0  128 

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

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

131 

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

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

0  135 

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

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

137 
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
1461  138 
Pair_neq_0, sym RS Pair_neq_0, Pair_inject, 
139 
make_elim succ_inject, 

140 
refl_thin, conjE, exE, disjE]; 

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

141 

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

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

143 
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

144 

516  145 
end; 
146 