src/HOL/ind_syntax.ML
 changeset 923 ff1574a81019 child 1430 439e1476a7f8
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ind_syntax.ML	Fri Mar 03 12:02:25 1995 +0100
1.3 @@ -0,0 +1,124 @@
1.4 +(*  Title: 	HOL/ind_syntax.ML
1.5 +    ID:         \$Id\$
1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   1994  University of Cambridge
1.8 +
1.9 +Abstract Syntax functions for Inductive Definitions
1.11 +*)
1.12 +
1.13 +(*The structure protects these items from redeclaration (somewhat!).  The
1.14 +  datatype definitions in theory files refer to these items by name!
1.15 +*)
1.16 +structure Ind_Syntax =
1.17 +struct
1.18 +
1.19 +(** Abstract syntax definitions for HOL **)
1.20 +
1.21 +open HOLogic;
1.22 +
1.23 +fun Int_const T =
1.24 +  let val sT = mk_setT T
1.25 +  in  Const("op Int", [sT,sT]--->sT)  end;
1.26 +
1.27 +fun mk_exists (Free(x,T),P) = exists_const T \$ (absfree (x,T,P));
1.28 +
1.29 +fun mk_all (Free(x,T),P) = all_const T \$ (absfree (x,T,P));
1.30 +
1.31 +(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
1.32 +fun mk_all_imp (A,P) =
1.33 +  let val T = dest_setT (fastype_of A)
1.34 +  in  all_const T \$ Abs("v", T, imp \$ (mk_mem (Bound 0, A)) \$ (P \$ Bound 0))
1.35 +  end;
1.36 +
1.37 +(** Cartesian product type **)
1.38 +
1.39 +val unitT = Type("unit",[]);
1.40 +
1.41 +fun mk_prod (T1,T2) = Type("*", [T1,T2]);
1.42 +
1.43 +(*Maps the type T1*...*Tn to [T1,...,Tn], if nested to the right*)
1.44 +fun factors (Type("*", [T1,T2])) = T1 :: factors T2
1.45 +  | factors T                    = [T];
1.46 +
1.47 +(*Make a correctly typed ordered pair*)
1.48 +fun mk_Pair (t1,t2) =
1.49 +  let val T1 = fastype_of t1
1.50 +      and T2 = fastype_of t2
1.51 +  in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) \$ t1 \$ t2  end;
1.52 +
1.53 +fun split_const(Ta,Tb,Tc) =
1.54 +    Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
1.55 +
1.56 +(*Given u expecting arguments of types [T1,...,Tn], create term of
1.57 +  type T1*...*Tn => Tc using split.  Here * associates to the LEFT*)
1.58 +fun ap_split_l Tc u [ ]   = Abs("null", unitT, u)
1.59 +  | ap_split_l Tc u [_]   = u
1.60 +  | ap_split_l Tc u (Ta::Tb::Ts) = ap_split_l Tc (split_const(Ta,Tb,Tc) \$ u)
1.61 +                                              (mk_prod(Ta,Tb) :: Ts);
1.62 +
1.63 +(*Given u expecting arguments of types [T1,...,Tn], create term of
1.64 +  type T1*...*Tn => i using split.  Here * associates to the RIGHT*)
1.65 +fun ap_split Tc u [ ]   = Abs("null", unitT, u)
1.66 +  | ap_split Tc u [_]   = u
1.67 +  | ap_split Tc u [Ta,Tb] = split_const(Ta,Tb,Tc) \$ u
1.68 +  | ap_split Tc u (Ta::Ts) =
1.69 +      split_const(Ta, foldr1 mk_prod Ts, Tc) \$
1.70 +      (Abs("v", Ta, ap_split Tc (u \$ Bound(length Ts - 2)) Ts));
1.71 +
1.72 +(** Disjoint sum type **)
1.73 +
1.74 +fun mk_sum (T1,T2) = Type("+", [T1,T2]);
1.75 +val Inl	= Const("Inl", dummyT)
1.76 +and Inr	= Const("Inr", dummyT);		(*correct types added later!*)
1.77 +(*val elim	= Const("case", [iT-->iT, iT-->iT, iT]--->iT)*)
1.78 +
1.79 +fun summands (Type("+", [T1,T2])) = summands T1 @ summands T2
1.80 +  | summands T                    = [T];
1.81 +
1.82 +(*Given the destination type, fills in correct types of an Inl/Inr nest*)
1.83 +fun mend_sum_types (h,T) =
1.84 +    (case (h,T) of
1.85 +	 (Const("Inl",_) \$ h1, Type("+", [T1,T2])) =>
1.86 +	     Const("Inl", T1 --> T) \$ (mend_sum_types (h1, T1))
1.87 +       | (Const("Inr",_) \$ h2, Type("+", [T1,T2])) =>
1.88 +	     Const("Inr", T2 --> T) \$ (mend_sum_types (h2, T2))
1.89 +       | _ => h);
1.90 +
1.91 +
1.92 +
1.93 +(*simple error-checking in the premises of an inductive definition*)
1.94 +fun chk_prem rec_hd (Const("op &",_) \$ _ \$ _) =
1.95 +	error"Premises may not be conjuctive"
1.96 +  | chk_prem rec_hd (Const("op :",_) \$ t \$ X) =
1.97 +	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
1.98 +  | chk_prem rec_hd t =
1.99 +	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
1.100 +
1.101 +(*Return the conclusion of a rule, of the form t:X*)
1.102 +fun rule_concl rl =
1.103 +    let val Const("Trueprop",_) \$ (Const("op :",_) \$ t \$ X) =
1.104 +		Logic.strip_imp_concl rl
1.105 +    in  (t,X)  end;
1.106 +
1.107 +(*As above, but return error message if bad*)
1.108 +fun rule_concl_msg sign rl = rule_concl rl
1.109 +    handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
1.110 +			  Sign.string_of_term sign rl);
1.111 +
1.112 +(*For simplifying the elimination rule*)
1.113 +val sumprod_free_SEs =
1.114 +    Pair_inject ::
1.115 +    map make_elim [(*Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject*)];
1.116 +
1.117 +(*For deriving cases rules.
1.118 +  read_instantiate replaces a propositional variable by a formula variable*)
1.119 +val equals_CollectD =