src/HOL/ind_syntax.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1465 5d7a7e439cec
child 1728 01beef6262aa
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     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 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 
    16 (** Abstract syntax definitions for HOL **)
    17 
    18 open HOLogic;
    19 
    20 fun Int_const T = 
    21   let val sT = mk_setT T
    22   in  Const("op Int", [sT,sT]--->sT)  end;
    23 
    24 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
    25 
    26 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
    27 
    28 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    29 fun mk_all_imp (A,P) = 
    30   let val T = dest_setT (fastype_of A)
    31   in  all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0))
    32   end;
    33 
    34 (** Cartesian product type **)
    35 
    36 val unitT = Type("unit",[]);
    37 
    38 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
    39 
    40 (*Maps the type T1*...*Tn to [T1,...,Tn], if nested to the right*)
    41 fun factors (Type("*", [T1,T2])) = T1 :: factors T2
    42   | factors T                    = [T];
    43 
    44 (*Make a correctly typed ordered pair*)
    45 fun mk_Pair (t1,t2) = 
    46   let val T1 = fastype_of t1
    47       and T2 = fastype_of t2
    48   in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
    49    
    50 fun split_const(Ta,Tb,Tc) = 
    51     Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
    52 
    53 (*Given u expecting arguments of types [T1,...,Tn], create term of 
    54   type T1*...*Tn => Tc using split.  Here * associates to the LEFT*)
    55 fun ap_split_l Tc u [ ]   = Abs("null", unitT, u)
    56   | ap_split_l Tc u [_]   = u
    57   | ap_split_l Tc u (Ta::Tb::Ts) = ap_split_l Tc (split_const(Ta,Tb,Tc) $ u) 
    58                                               (mk_prod(Ta,Tb) :: Ts);
    59 
    60 (*Given u expecting arguments of types [T1,...,Tn], create term of 
    61   type T1*...*Tn => i using split.  Here * associates to the RIGHT*)
    62 fun ap_split Tc u [ ]   = Abs("null", unitT, u)
    63   | ap_split Tc u [_]   = u
    64   | ap_split Tc u [Ta,Tb] = split_const(Ta,Tb,Tc) $ u
    65   | ap_split Tc u (Ta::Ts) = 
    66       split_const(Ta, foldr1 mk_prod Ts, Tc) $ 
    67       (Abs("v", Ta, ap_split Tc (u $ Bound(length Ts - 2)) Ts));
    68 
    69 (** Disjoint sum type **)
    70 
    71 fun mk_sum (T1,T2) = Type("+", [T1,T2]);
    72 val Inl = Const("Inl", dummyT)
    73 and Inr = Const("Inr", dummyT);         (*correct types added later!*)
    74 (*val elim      = Const("case", [iT-->iT, iT-->iT, iT]--->iT)*)
    75 
    76 fun summands (Type("+", [T1,T2])) = summands T1 @ summands T2
    77   | summands T                    = [T];
    78 
    79 (*Given the destination type, fills in correct types of an Inl/Inr nest*)
    80 fun mend_sum_types (h,T) =
    81     (case (h,T) of
    82          (Const("Inl",_) $ h1, Type("+", [T1,T2])) =>
    83              Const("Inl", T1 --> T) $ (mend_sum_types (h1, T1))
    84        | (Const("Inr",_) $ h2, Type("+", [T1,T2])) =>
    85              Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2))
    86        | _ => h);
    87 
    88 
    89 
    90 (*simple error-checking in the premises of an inductive definition*)
    91 fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    92         error"Premises may not be conjuctive"
    93   | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
    94         deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
    95   | chk_prem rec_hd t = 
    96         deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
    97 
    98 (*Return the conclusion of a rule, of the form t:X*)
    99 fun rule_concl rl = 
   100     let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
   101                 Logic.strip_imp_concl rl
   102     in  (t,X)  end;
   103 
   104 (*As above, but return error message if bad*)
   105 fun rule_concl_msg sign rl = rule_concl rl
   106     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 
   107                           Sign.string_of_term sign rl);
   108 
   109 (*For simplifying the elimination rule*)
   110 val sumprod_free_SEs = 
   111     Pair_inject ::
   112     map make_elim [(*Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject*)];
   113 
   114 (*For deriving cases rules.  
   115   read_instantiate replaces a propositional variable by a formula variable*)
   116 val equals_CollectD = 
   117     read_instantiate [("W","?Q")]
   118         (make_elim (equalityD1 RS subsetD RS CollectD));
   119 
   120 (*Delete needless equality assumptions*)
   121 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
   122      (fn _ => [assume_tac 1]);
   123 
   124 (*Includes rules for Suc and Pair since they are common constructions*)
   125 val elim_rls = [asm_rl, FalseE, (*Suc_neq_Zero, Zero_neq_Suc,
   126                 make_elim Suc_inject, *)
   127                 refl_thin, conjE, exE, disjE];
   128 
   129 end;