1 (*  Title:      nominal_library.ML

     2     Author:     Christian Urban

     3 

     4   Basic functions for nominal.

     5 *)

     6 

     7 signature NOMINAL_LIBRARY =

     8 sig

     9   val is_true: term -> bool

    10 

    11   val last2: 'a list -> 'a * 'a

    12 

    13   val dest_listT: typ -> typ

    14 

    15   val size_const: typ -> term 

    16 

    17   val sum_case_const: typ -> typ -> typ -> term

    18   val mk_sum_case: term -> term -> term

    19  

    20   val mk_minus: term -> term

    21   val mk_plus: term -> term -> term

    22 

    23   val perm_ty: typ -> typ 

    24   val mk_perm_ty: typ -> term -> term -> term

    25   val mk_perm: term -> term -> term

    26   val dest_perm: term -> term * term

    27 

    28   val mk_sort_of: term -> term

    29   val atom_ty: typ -> typ

    30   val mk_atom_ty: typ -> term -> term

    31   val mk_atom: term -> term

    32 

    33   val supp_ty: typ -> typ

    34   val supp_const: typ -> term

    35   val mk_supp_ty: typ -> term -> term

    36   val mk_supp: term -> term

    37 

    38   val supp_rel_ty: typ -> typ

    39   val supp_rel_const: typ -> term

    40   val mk_supp_rel_ty: typ -> term -> term -> term

    41   val mk_supp_rel: term -> term -> term		       

    42 

    43   val supports_const: typ -> term

    44   val mk_supports_ty: typ -> term -> term -> term

    45   val mk_supports: term -> term -> term

    46 

    47   val finite_const: typ -> term

    48   val mk_finite_ty: typ -> term -> term

    49   val mk_finite: term -> term

    50 

    51 

    52   val mk_equiv: thm -> thm

    53   val safe_mk_equiv: thm -> thm

    54 

    55   val mk_diff: term * term -> term

    56   val mk_append: term * term -> term

    57   val mk_union: term * term -> term

    58   val fold_union: term list -> term

    59   val fold_append: term list -> term

    60   val mk_conj: term * term -> term

    61   val fold_conj: term list -> term

    62 

    63   (* fresh arguments for a term *)

    64   val fresh_args: Proof.context -> term -> term list

    65 

    66   (* datatype operations *)

    67   type cns_info = (term * typ * typ list * bool list) list

    68 

    69   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list

    70   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ

    71   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list

    72   val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info

    73   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list

    74 

    75   (* tactics for function package *)

    76   val pat_completeness_simp: thm list -> Proof.context -> tactic

    77   val prove_termination: thm list -> Proof.context -> Function.info * local_theory

    78 

    79   (* transformations of premises in inductions *)

    80   val transform_prem1: Proof.context -> string list -> thm -> thm

    81   val transform_prem2: Proof.context -> string list -> thm -> thm

    82 

    83   (* transformation into the object logic *)

    84   val atomize: thm -> thm

    85 

    86 end

    87 

    88 

    89 structure Nominal_Library: NOMINAL_LIBRARY =

    90 struct

    91 

    92 fun is_true @{term "Trueprop True"} = true

    93   | is_true _ = false 

    94 

    95 fun last2 [] = raise Empty

    96   | last2 [_] = raise Empty

    97   | last2 [x, y] = (x, y)

    98   | last2 (_ :: xs) = last2 xs

    99 

   100 fun dest_listT (Type (@{type_name list}, [T])) = T

   101   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])

   102 

   103 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})

   104 

   105 fun sum_case_const ty1 ty2 ty3 = 

   106   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)

   107 fun mk_sum_case trm1 trm2 =

   108   let

   109     val ([ty1], ty3) = strip_type (fastype_of trm1)

   110     val ty2 = domain_type (fastype_of trm2)

   111   in

   112     sum_case_const ty1 ty2 ty3 $ trm1 $ trm2

   113   end 

   114 

   115 

   116 

   117 fun mk_minus p = @{term "uminus::perm => perm"} $ p

   118 

   119 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q

   120 

   121 fun perm_ty ty = @{typ "perm"} --> ty --> ty

   122 fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm

   123 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm

   124 

   125 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)

   126   | dest_perm t = raise TERM ("dest_perm", [t]);

   127 

   128 fun mk_sort_of t = @{term "sort_of"} $ t;

   129 

   130 fun atom_ty ty = ty --> @{typ "atom"};

   131 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;

   132 fun mk_atom t = mk_atom_ty (fastype_of t) t;

   133 

   134 

   135 fun supp_ty ty = ty --> @{typ "atom set"};

   136 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)

   137 fun mk_supp_ty ty t = supp_const ty $ t

   138 fun mk_supp t = mk_supp_ty (fastype_of t) t

   139 

   140 fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"};

   141 fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty)

   142 fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t

   143 fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t

   144 

   145 fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool});

   146 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2;

   147 fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2;

   148 

   149 fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool})

   150 fun mk_finite_ty ty t = finite_const ty $ t

   151 fun mk_finite t = mk_finite_ty (fastype_of t) t

   152 

   153 

   154 fun mk_equiv r = r RS @{thm eq_reflection};

   155 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;

   156 

   157 

   158 (* functions that construct differences, appends and unions

   159    but avoid producing empty atom sets or empty atom lists *)

   160 

   161 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}

   162   | mk_diff (t1, @{term "{}::atom set"}) = t1

   163   | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"}

   164   | mk_diff (t1, @{term "set ([]::atom list)"}) = t1

   165   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)

   166 

   167 fun mk_append (t1, @{term "[]::atom list"}) = t1

   168   | mk_append (@{term "[]::atom list"}, t2) = t2

   169   | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) 

   170 

   171 fun mk_union (t1, @{term "{}::atom set"}) = t1

   172   | mk_union (@{term "{}::atom set"}, t2) = t2

   173   | mk_union (t1, @{term "set ([]::atom list)"}) = t1

   174   | mk_union (@{term "set ([]::atom list)"}, t2) = t2

   175   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  

   176  

   177 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}

   178 fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"}

   179 

   180 fun mk_conj (t1, @{term "True"}) = t1

   181   | mk_conj (@{term "True"}, t2) = t2

   182   | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)

   183 

   184 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}

   185 

   186 

   187 (* produces fresh arguments for a term *)

   188 

   189 fun fresh_args ctxt f =

   190     f |> fastype_of

   191       |> binder_types

   192       |> map (pair "z")

   193       |> Variable.variant_frees ctxt [f]

   194       |> map Free

   195 

   196 

   197 

   198 (** datatypes **)

   199 

   200 (* constructor infos *)

   201 type cns_info = (term * typ * typ list * bool list) list

   202 

   203 (* returns the type of the nth datatype *)

   204 fun all_dtyps descr sorts = 

   205   map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))

   206 

   207 fun nth_dtyp descr sorts n = 

   208   Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);

   209 

   210 (* returns info about constructors in a datatype *)

   211 fun all_dtyp_constrs_info descr = 

   212   map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr

   213 

   214 (* returns the constants of the constructors plus the 

   215    corresponding type and types of arguments *)

   216 fun all_dtyp_constrs_types descr sorts = 

   217   let

   218     fun aux ((ty_name, vs), (cname, args)) =

   219       let

   220         val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs

   221         val ty = Type (ty_name, vs_tys)

   222         val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args

   223         val is_rec = map Datatype_Aux.is_rec_type args

   224       in

   225         (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)

   226       end

   227   in

   228     map (map aux) (all_dtyp_constrs_info descr)

   229   end

   230 

   231 fun nth_dtyp_constrs_types descr sorts n =

   232   nth (all_dtyp_constrs_types descr sorts) n

   233 

   234 

   235 (* generates for every datatype a name str ^ dt_name 

   236    plus and index for multiple occurences of a string *)

   237 fun prefix_dt_names descr sorts str = 

   238   let

   239     fun get_nth_name (i, _) = 

   240       Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 

   241   in

   242     Datatype_Prop.indexify_names 

   243       (map (prefix str o get_nth_name) descr)

   244   end

   245 

   246 

   247 

   248 (** function package tactics **)

   249 

   250 fun pat_completeness_simp simps lthy =

   251   let

   252     val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)

   253   in

   254     Pat_Completeness.pat_completeness_tac lthy 1

   255       THEN ALLGOALS (asm_full_simp_tac simp_set)

   256   end

   257 

   258 

   259 fun prove_termination_tac size_simps ctxt =

   260   let

   261     val natT = @{typ nat}

   262     fun prod_size_const fT sT = 

   263       let

   264         val fT_fun = fT --> natT

   265         val sT_fun = sT --> natT

   266         val prodT = Type (@{type_name prod}, [fT, sT])

   267       in

   268         Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT)

   269       end

   270 

   271     fun mk_size_measure T =

   272       case T of    

   273         (Type (@{type_name Sum_Type.sum}, [fT, sT])) =>

   274            SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT)

   275       | (Type (@{type_name Product_Type.prod}, [fT, sT])) =>

   276            prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT)

   277       | _ => size_const T

   278 

   279     fun mk_measure_trm T = 

   280       HOLogic.dest_setT T

   281       |> fst o HOLogic.dest_prodT

   282       |> mk_size_measure 

   283       |> curry (op $) (Const (@{const_name "measure"}, dummyT))

   284       |> Syntax.check_term ctxt

   285       

   286     val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 

   287       zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps 

   288     val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals

   289   in

   290     Function_Relation.relation_tac ctxt mk_measure_trm

   291     THEN_ALL_NEW simp_tac ss'

   292   end

   293 

   294 fun prove_termination size_simps ctxt = 

   295   Function.prove_termination NONE 

   296     (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt

   297 

   298 (** transformations of premises (in inductive proofs) **)

   299 

   300 (* 

   301  given the theorem F[t]; proves the theorem F[f t] 

   302 

   303   - F needs to be monotone

   304   - f returns either SOME for a term it fires on 

   305     and NONE elsewhere 

   306 *)

   307 fun map_term f t = 

   308   (case f t of

   309      NONE => map_term' f t 

   310    | x => x)

   311 and map_term' f (t $ u) = 

   312     (case (map_term f t, map_term f u) of

   313         (NONE, NONE) => NONE

   314       | (SOME t'', NONE) => SOME (t'' $ u)

   315       | (NONE, SOME u'') => SOME (t $ u'')

   316       | (SOME t'', SOME u'') => SOME (t'' $ u''))

   317   | map_term' f (Abs (s, T, t)) = 

   318       (case map_term f t of

   319         NONE => NONE

   320       | SOME t'' => SOME (Abs (s, T, t'')))

   321   | map_term' _ _  = NONE;

   322 

   323 fun map_thm_tac ctxt tac thm =

   324   let

   325     val monos = Inductive.get_monos ctxt

   326     val simps = HOL_basic_ss addsimps @{thms split_def}

   327   in

   328     EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 

   329       REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),

   330       REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]

   331   end

   332 

   333 fun map_thm ctxt f tac thm =

   334   let

   335     val opt_goal_trm = map_term f (prop_of thm)

   336   in

   337     case opt_goal_trm of

   338       NONE => thm

   339     | SOME goal =>

   340         Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) 

   341   end

   342 

   343 (*

   344  inductive premises can be of the form

   345  R ... /\ P ...; split_conj_i picks out

   346  the part R or P part

   347 *)

   348 fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = 

   349   (case head_of f1 of

   350      Const (name, _) => if member (op =) names name then SOME f1 else NONE

   351    | _ => NONE)

   352 | split_conj1 _ _ = NONE;

   353 

   354 fun split_conj2 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = 

   355   (case head_of f1 of

   356      Const (name, _) => if member (op =) names name then SOME f2 else NONE

   357    | _ => NONE)

   358 | split_conj2 _ _ = NONE;

   359 

   360 fun transform_prem1 ctxt names thm =

   361   map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm

   362 

   363 fun transform_prem2 ctxt names thm =

   364   map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm

   365 

   366 

   367 (* transformes a theorem into one of the object logic *)

   368 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars

   369 

   370 end (* structure *)

   371 

   372 open Nominal_Library;