|
1 (* Title: HOL/ind_syntax.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Abstract Syntax functions for Inductive Definitions |
|
7 See also ../Pure/section-utils.ML |
|
8 *) |
|
9 |
|
10 (*The structure protects these items from redeclaration (somewhat!). The |
|
11 datatype definitions in theory files refer to these items by name! |
|
12 *) |
|
13 structure Ind_Syntax = |
|
14 struct |
|
15 |
|
16 (** Abstract syntax definitions for HOL **) |
|
17 |
|
18 val termC: class = "term"; |
|
19 val termS: sort = [termC]; |
|
20 |
|
21 val termTVar = TVar(("'a",0),termS); |
|
22 |
|
23 val boolT = Type("bool",[]); |
|
24 val unitT = Type("unit",[]); |
|
25 |
|
26 val conj = Const("op &", [boolT,boolT]--->boolT) |
|
27 and disj = Const("op |", [boolT,boolT]--->boolT) |
|
28 and imp = Const("op -->", [boolT,boolT]--->boolT); |
|
29 |
|
30 fun eq_const T = Const("op =", [T,T]--->boolT); |
|
31 |
|
32 fun mk_set T = Type("set",[T]); |
|
33 |
|
34 fun dest_set (Type("set",[T])) = T |
|
35 | dest_set _ = error "dest_set: set type expected" |
|
36 |
|
37 fun mk_mem (x,A) = |
|
38 let val setT = fastype_of A |
|
39 in Const("op :", [dest_set setT, setT]--->boolT) $ x $ A |
|
40 end; |
|
41 |
|
42 fun Int_const T = |
|
43 let val sT = mk_set T |
|
44 in Const("op Int", [sT,sT]--->sT) end; |
|
45 |
|
46 fun exists_const T = Const("Ex", [T-->boolT]--->boolT); |
|
47 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); |
|
48 |
|
49 fun all_const T = Const("All", [T-->boolT]--->boolT); |
|
50 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); |
|
51 |
|
52 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
|
53 fun mk_all_imp (A,P) = |
|
54 let val T = dest_set (fastype_of A) |
|
55 in all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0)) |
|
56 end; |
|
57 |
|
58 (** Cartesian product type **) |
|
59 |
|
60 fun mk_prod (T1,T2) = Type("*", [T1,T2]); |
|
61 |
|
62 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2 |
|
63 | factors T = [T]; |
|
64 |
|
65 (*Make a correctly typed ordered pair*) |
|
66 fun mk_Pair (t1,t2) = |
|
67 let val T1 = fastype_of t1 |
|
68 and T2 = fastype_of t2 |
|
69 in Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2 end; |
|
70 |
|
71 fun split_const(Ta,Tb,Tc) = |
|
72 Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc); |
|
73 |
|
74 (*Given u expecting arguments of types [T1,...,Tn], create term of |
|
75 type T1*...*Tn => Tc using split. Here * associates to the LEFT*) |
|
76 fun ap_split_l Tc u [ ] = Abs("null", unitT, u) |
|
77 | ap_split_l Tc u [_] = u |
|
78 | ap_split_l Tc u (Ta::Tb::Ts) = ap_split_l Tc (split_const(Ta,Tb,Tc) $ u) |
|
79 (mk_prod(Ta,Tb) :: Ts); |
|
80 |
|
81 (*Given u expecting arguments of types [T1,...,Tn], create term of |
|
82 type T1*...*Tn => i using split. Here * associates to the RIGHT*) |
|
83 fun ap_split Tc u [ ] = Abs("null", unitT, u) |
|
84 | ap_split Tc u [_] = u |
|
85 | ap_split Tc u [Ta,Tb] = split_const(Ta,Tb,Tc) $ u |
|
86 | ap_split Tc u (Ta::Ts) = |
|
87 split_const(Ta, foldr1 mk_prod Ts, Tc) $ |
|
88 (Abs("v", Ta, ap_split Tc (u $ Bound(length Ts - 2)) Ts)); |
|
89 |
|
90 (** Disjoint sum type **) |
|
91 |
|
92 fun mk_sum (T1,T2) = Type("+", [T1,T2]); |
|
93 val Inl = Const("Inl", dummyT) |
|
94 and Inr = Const("Inr", dummyT); (*correct types added later!*) |
|
95 (*val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)*) |
|
96 |
|
97 fun summands (Type("+", [T1,T2])) = summands T1 @ summands T2 |
|
98 | summands T = [T]; |
|
99 |
|
100 (*Given the destination type, fills in correct types of an Inl/Inr nest*) |
|
101 fun mend_sum_types (h,T) = |
|
102 (case (h,T) of |
|
103 (Const("Inl",_) $ h1, Type("+", [T1,T2])) => |
|
104 Const("Inl", T1 --> T) $ (mend_sum_types (h1, T1)) |
|
105 | (Const("Inr",_) $ h2, Type("+", [T1,T2])) => |
|
106 Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2)) |
|
107 | _ => h); |
|
108 |
|
109 fun Collect_const T = Const("Collect", [T-->boolT] ---> mk_set T); |
|
110 fun mk_Collect (a,T,t) = Collect_const T $ absfree(a, T, t); |
|
111 |
|
112 val Trueprop = Const("Trueprop",boolT-->propT); |
|
113 fun mk_tprop P = Trueprop $ P; |
|
114 |
|
115 |
|
116 (*simple error-checking in the premises of an inductive definition*) |
|
117 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = |
|
118 error"Premises may not be conjuctive" |
|
119 | chk_prem rec_hd (Const("op :",_) $ t $ X) = |
|
120 deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" |
|
121 | chk_prem rec_hd t = |
|
122 deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; |
|
123 |
|
124 (*Return the conclusion of a rule, of the form t:X*) |
|
125 fun rule_concl rl = |
|
126 let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = |
|
127 Logic.strip_imp_concl rl |
|
128 in (t,X) end; |
|
129 |
|
130 (*As above, but return error message if bad*) |
|
131 fun rule_concl_msg sign rl = rule_concl rl |
|
132 handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ |
|
133 Sign.string_of_term sign rl); |
|
134 |
|
135 (*For simplifying the elimination rule*) |
|
136 val sumprod_free_SEs = |
|
137 Pair_inject :: |
|
138 map make_elim [Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject]; |
|
139 |
|
140 (*For deriving cases rules. |
|
141 read_instantiate replaces a propositional variable by a formula variable*) |
|
142 val equals_CollectD = |
|
143 read_instantiate [("W","?Q")] |
|
144 (make_elim (equalityD1 RS subsetD RS CollectD)); |
|
145 |
|
146 (*Delete needless equality assumptions*) |
|
147 val refl_thin = prove_goal HOL.thy "!!P. [| a=a; P |] ==> P" |
|
148 (fn _ => [assume_tac 1]); |
|
149 |
|
150 end; |
|
151 |