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.10 +See also hologic.ML and ../Pure/section-utils.ML
    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 = 
   1.120 +    read_instantiate [("W","?Q")]
   1.121 +        (make_elim (equalityD1 RS subsetD RS CollectD));
   1.122 +
   1.123 +(*Delete needless equality assumptions*)
   1.124 +val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
   1.125 +     (fn _ => [assume_tac 1]);
   1.126 +
   1.127 +end;