author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 44241  7943b69f0188 
child 55143  04448228381d 
permissions  rwrr 
12243  1 
(* Title: ZF/ind_syntax.ML 
1461  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 

12243  5 
Abstract Syntax functions for Inductive Definitions. 
0  6 
*) 
7 

516  8 
structure Ind_Syntax = 
9 
struct 

0  10 

4804
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset

11 
(*Print tracing messages during processing of "inductive" theory sections*) 
32740  12 
val trace = Unsynchronized.ref false; 
4804
02b7c759159b
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
4352
diff
changeset

13 

26189  14 
fun traceIt msg thy t = 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26189
diff
changeset

15 
if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t) 
17988  16 
else t; 
17 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset

18 

4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset

19 
(** Abstract syntax definitions for ZF **) 
0  20 

38514  21 
val iT = Type(@{type_name i}, []); 
0  22 

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

26189  24 
fun mk_all_imp (A,P) = 
25 
FOLogic.all_const iT $ 

26 
Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $ 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

27 
Term.betapply(P, Bound 0)); 
0  28 

44241  29 
fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT) t; 
0  30 

516  31 
(*simple errorchecking in the premises of an inductive definition*) 
41310  32 
fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) = 
1461  33 
error"Premises may not be conjuctive" 
26189  34 
 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

35 
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ()) 
26189  36 
 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

37 
(Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ()); 
516  38 

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

39 
(*Return the conclusion of a rule, of the form t:X*) 
26189  40 
fun rule_concl rl = 
41 
let val Const (@{const_name Trueprop}, _) $ (Const (@{const_name mem}, _) $ t $ X) = 

1461  42 
Logic.strip_imp_concl rl 
435  43 
in (t,X) end; 
44 

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

46 
fun rule_concl_msg sign rl = rule_concl rl 

26189  47 
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

48 
Syntax.string_of_term_global sign rl); 
0  49 

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

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

26189  52 
val equals_CollectD = 
27239  53 
read_instantiate @{context} [(("W", 0), "?Q")] 
24893  54 
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2})); 
0  55 

56 

516  57 
(** For datatype definitions **) 
58 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset

59 
(*Constructor name, type, mixfix info; 
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset

60 
internal name from mixfix, datatype sets, full premises*) 
26189  61 
type constructor_spec = 
62 
(string * typ * mixfix) * string * term list * term list; 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
4972
diff
changeset

63 

26189  64 
fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A) 
516  65 
 dest_mem _ = error "Constructor specifications must have the form x:A"; 
66 

67 
(*read a constructor specification*) 

35129  68 
fun read_construct ctxt (id: string, sprems, syn: mixfix) = 
39288  69 
let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems 
27261
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
27239
diff
changeset

70 
> Syntax.check_terms ctxt 
1461  71 
val args = map (#1 o dest_mem) prems 
72 
val T = (map (#2 o dest_Free) args) > iT 

26189  73 
handle TERM _ => error 
1461  74 
"Bad variable in constructor specification" 
35129  75 
in ((id,T,syn), id, args, prems) end; 
516  76 

77 
val read_constructs = map o map o read_construct; 

0  78 

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

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

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

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

83 
Logic.list_implies 
4352
7ac9f3e8a97d
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
paulson
parents:
3925
diff
changeset

84 
(map FOLogic.mk_Trueprop prems, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

85 
FOLogic.mk_Trueprop 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

86 
(@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

87 
$ rec_tm)) 
516  88 
in map mk_intr constructs end; 
89 

32952  90 
fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg); 
0  91 

26189  92 
fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2; 
0  93 

516  94 
(*Make a datatype's domain: form the union of its set parameters*) 
6112  95 
fun union_params (rec_tm, cs) = 
516  96 
let val (_,args) = strip_comb rec_tm 
6112  97 
fun is_ind arg = (type_of arg = iT) 
33317  98 
in case filter is_ind (args @ cs) of 
41310  99 
[] => @{const zero} 
32765  100 
 u_args => Balanced_Tree.make mk_Un u_args 
516  101 
end; 
102 

0  103 

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

104 
(*Includes rules for succ and Pair since they are common constructions*) 
26189  105 
val elim_rls = 
106 
[@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0}, 

107 
@{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject}, 

108 
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

109 

7694  110 

111 
(*From HOL/ex/meson.ML: raises exception if no rules apply  unlike RL*) 

112 
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) 

113 
 tryres (th, []) = raise THM("tryres", 0, [th]); 

114 

26189  115 
fun gen_make_elim elim_rls rl = 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33317
diff
changeset

116 
Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl])); 
7694  117 

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

118 
(*Turns iff rules into safe elimination rules*) 
26189  119 
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

120 

516  121 
end; 
122 