9 val last2: 'a list -> 'a * 'a |
9 val last2: 'a list -> 'a * 'a |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
11 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
12 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
12 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
13 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
13 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
|
14 val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a |
14 |
15 |
15 |
|
16 val is_true: term -> bool |
16 val is_true: term -> bool |
17 |
17 |
18 val dest_listT: typ -> typ |
18 val dest_listT: typ -> typ |
19 val dest_fsetT: typ -> typ |
19 val dest_fsetT: typ -> typ |
20 |
20 |
92 val fold_union: term list -> term |
92 val fold_union: term list -> term |
93 val fold_append: term list -> term |
93 val fold_append: term list -> term |
94 val mk_conj: term * term -> term |
94 val mk_conj: term * term -> term |
95 val fold_conj: term list -> term |
95 val fold_conj: term list -> term |
96 |
96 |
|
97 (* functions for de-Bruijn open terms *) |
|
98 val mk_binop_env: typ list -> string -> term * term -> term |
|
99 val mk_union_env: typ list -> term * term -> term |
|
100 val fold_union_env: typ list -> term list -> term |
|
101 |
97 (* fresh arguments for a term *) |
102 (* fresh arguments for a term *) |
98 val fresh_args: Proof.context -> term -> term list |
103 val fresh_args: Proof.context -> term -> term list |
|
104 |
|
105 (* some logic operations *) |
|
106 val strip_full_horn: term -> (string * typ) list * term list * term |
|
107 val mk_full_horn: (string * typ) list -> term list -> term -> term |
99 |
108 |
100 (* datatype operations *) |
109 (* datatype operations *) |
101 type cns_info = (term * typ * typ list * bool list) list |
110 type cns_info = (term * typ * typ list * bool list) list |
102 |
111 |
103 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
112 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
115 val transform_prem2: Proof.context -> string list -> thm -> thm |
124 val transform_prem2: Proof.context -> string list -> thm -> thm |
116 |
125 |
117 (* transformation into the object logic *) |
126 (* transformation into the object logic *) |
118 val atomize: thm -> thm |
127 val atomize: thm -> thm |
119 |
128 |
|
129 (* applies a tactic to a formula composed of conjunctions *) |
|
130 val conj_tac: (int -> tactic) -> int -> tactic |
120 end |
131 end |
121 |
132 |
122 |
133 |
123 structure Nominal_Library: NOMINAL_LIBRARY = |
134 structure Nominal_Library: NOMINAL_LIBRARY = |
124 struct |
135 struct |
341 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
358 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
342 |
359 |
343 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
360 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
344 |
361 |
345 |
362 |
|
363 (* functions for de-Bruijn open terms *) |
|
364 |
|
365 fun mk_binop_env tys c (t, u) = |
|
366 let |
|
367 val ty = fastype_of1 (tys, t) |
|
368 in |
|
369 Const (c, [ty, ty] ---> ty) $ t $ u |
|
370 end |
|
371 |
|
372 fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 |
|
373 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 |
|
374 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 |
|
375 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 |
|
376 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) |
|
377 |
|
378 fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} |
|
379 |
|
380 |
346 (* produces fresh arguments for a term *) |
381 (* produces fresh arguments for a term *) |
347 |
382 |
348 fun fresh_args ctxt f = |
383 fun fresh_args ctxt f = |
349 f |> fastype_of |
384 f |> fastype_of |
350 |> binder_types |
385 |> binder_types |
351 |> map (pair "z") |
386 |> map (pair "z") |
352 |> Variable.variant_frees ctxt [f] |
387 |> Variable.variant_frees ctxt [f] |
353 |> map Free |
388 |> map Free |
354 |
389 |
355 |
390 |
|
391 (** some logic operations **) |
|
392 |
|
393 (* decompses a formula into params, premises and a conclusion *) |
|
394 fun strip_full_horn trm = |
|
395 let |
|
396 fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
|
397 | strip_outer_params B = ([], B) |
|
398 |
|
399 val (params, body) = strip_outer_params trm |
|
400 val (prems, concl) = Logic.strip_horn body |
|
401 in |
|
402 (params, prems, concl) |
|
403 end |
|
404 |
|
405 (* composes a formula out of params, premises and a conclusion *) |
|
406 fun mk_full_horn params prems concl = |
|
407 Logic.list_implies (prems, concl) |
|
408 |> fold_rev mk_all params |
356 |
409 |
357 (** datatypes **) |
410 (** datatypes **) |
358 |
411 |
359 (* constructor infos *) |
412 (* constructor infos *) |
360 type cns_info = (term * typ * typ list * bool list) list |
413 type cns_info = (term * typ * typ list * bool list) list |
530 |
583 |
531 |
584 |
532 (* transformes a theorem into one of the object logic *) |
585 (* transformes a theorem into one of the object logic *) |
533 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
586 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
534 |
587 |
|
588 (* applies a tactic to a formula composed of conjunctions *) |
|
589 fun conj_tac tac i = |
|
590 let |
|
591 fun select (trm, i) = |
|
592 case trm of |
|
593 @{term "Trueprop"} $ t' => select (t', i) |
|
594 | @{term "op &"} $ _ $ _ => EVERY' [rtac @{thm conjI}, RANGE [conj_tac tac, conj_tac tac]] i |
|
595 | _ => tac i |
|
596 in |
|
597 SUBGOAL select i |
|
598 end |
|
599 |
|
600 |
535 end (* structure *) |
601 end (* structure *) |
536 |
602 |
537 open Nominal_Library; |
603 open Nominal_Library; |