author  wenzelm 
Tue, 29 Sep 2009 22:48:24 +0200  
changeset 32765  3032c0308019 
parent 32740  9dd0a2f83429 
child 32952  aeb1e44fbc19 
permissions  rwrr 
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*) 
32740  13 
val trace = Unsynchronized.ref false; 
4804
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 errorchecking 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 ("Illformed 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" 
30345  76 
val name = Syntax.const_name syn id 
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 
28965  88 
(@{const mem} $ list_comb (Const (Sign.full_bname 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} 
32765  102 
 u_args => Balanced_Tree.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 