author | wenzelm |
Mon, 22 Jun 1998 17:26:46 +0200 | |
changeset 5069 | 3ea049f7979d |
parent 4972 | 7fe1d30c1374 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ind_syntax.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
Abstract Syntax functions for Inductive Definitions |
|
7 |
See also hologic.ML and ../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 |
||
4807
013ba4c43832
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
1746
diff
changeset
|
16 |
(*Print tracing messages during processing of "inductive" theory sections*) |
013ba4c43832
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
1746
diff
changeset
|
17 |
val trace = ref false; |
013ba4c43832
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
1746
diff
changeset
|
18 |
|
923 | 19 |
(** Abstract syntax definitions for HOL **) |
20 |
||
21 |
open HOLogic; |
|
22 |
||
23 |
fun Int_const T = |
|
24 |
let val sT = mk_setT T |
|
25 |
in Const("op Int", [sT,sT]--->sT) end; |
|
26 |
||
27 |
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); |
|
28 |
||
29 |
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); |
|
30 |
||
31 |
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
|
32 |
fun mk_all_imp (A,P) = |
|
33 |
let val T = dest_setT (fastype_of A) |
|
4972
7fe1d30c1374
mk_all_imp: no longer creates goals that have beta-redexes
paulson
parents:
4807
diff
changeset
|
34 |
in all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ |
7fe1d30c1374
mk_all_imp: no longer creates goals that have beta-redexes
paulson
parents:
4807
diff
changeset
|
35 |
betapply(P, Bound 0)) |
923 | 36 |
end; |
37 |
||
38 |
(** Disjoint sum type **) |
|
39 |
||
40 |
fun mk_sum (T1,T2) = Type("+", [T1,T2]); |
|
1465 | 41 |
val Inl = Const("Inl", dummyT) |
42 |
and Inr = Const("Inr", dummyT); (*correct types added later!*) |
|
43 |
(*val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)*) |
|
923 | 44 |
|
45 |
fun summands (Type("+", [T1,T2])) = summands T1 @ summands T2 |
|
46 |
| summands T = [T]; |
|
47 |
||
48 |
(*Given the destination type, fills in correct types of an Inl/Inr nest*) |
|
49 |
fun mend_sum_types (h,T) = |
|
50 |
(case (h,T) of |
|
1465 | 51 |
(Const("Inl",_) $ h1, Type("+", [T1,T2])) => |
52 |
Const("Inl", T1 --> T) $ (mend_sum_types (h1, T1)) |
|
923 | 53 |
| (Const("Inr",_) $ h2, Type("+", [T1,T2])) => |
1465 | 54 |
Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2)) |
923 | 55 |
| _ => h); |
56 |
||
57 |
||
58 |
||
59 |
(*simple error-checking in the premises of an inductive definition*) |
|
60 |
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = |
|
1465 | 61 |
error"Premises may not be conjuctive" |
923 | 62 |
| chk_prem rec_hd (Const("op :",_) $ t $ X) = |
1465 | 63 |
deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" |
923 | 64 |
| chk_prem rec_hd t = |
1465 | 65 |
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; |
923 | 66 |
|
67 |
(*Return the conclusion of a rule, of the form t:X*) |
|
68 |
fun rule_concl rl = |
|
69 |
let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = |
|
1465 | 70 |
Logic.strip_imp_concl rl |
923 | 71 |
in (t,X) end; |
72 |
||
73 |
(*As above, but return error message if bad*) |
|
74 |
fun rule_concl_msg sign rl = rule_concl rl |
|
75 |
handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ |
|
1465 | 76 |
Sign.string_of_term sign rl); |
923 | 77 |
|
78 |
(*For simplifying the elimination rule*) |
|
79 |
val sumprod_free_SEs = |
|
80 |
Pair_inject :: |
|
81 |
map make_elim [(*Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject*)]; |
|
82 |
||
83 |
(*For deriving cases rules. |
|
84 |
read_instantiate replaces a propositional variable by a formula variable*) |
|
85 |
val equals_CollectD = |
|
86 |
read_instantiate [("W","?Q")] |
|
87 |
(make_elim (equalityD1 RS subsetD RS CollectD)); |
|
88 |
||
89 |
(*Delete needless equality assumptions*) |
|
90 |
val refl_thin = prove_goal HOL.thy "!!P. [| a=a; P |] ==> P" |
|
91 |
(fn _ => [assume_tac 1]); |
|
92 |
||
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
93 |
(*Includes rules for Suc and Pair since they are common constructions*) |
1433 | 94 |
val elim_rls = [asm_rl, FalseE, (*Suc_neq_Zero, Zero_neq_Suc, |
1465 | 95 |
make_elim Suc_inject, *) |
96 |
refl_thin, conjE, exE, disjE]; |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
97 |
|
923 | 98 |
end; |
4807
013ba4c43832
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
1746
diff
changeset
|
99 |
|
013ba4c43832
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
1746
diff
changeset
|
100 |
|
013ba4c43832
Fixed bug in inductive sections to allow disjunctive premises;
paulson
parents:
1746
diff
changeset
|
101 |
val trace_induct = Ind_Syntax.trace; |