# HG changeset patch # User Christian Urban # Date 1292112640 0 # Node ID 7430e07a5d619bfd7f44be0fbd80b5e45a5789a3 # Parent 6f9735c15d18cecb4f922401543bc7544b9838b5 moved setify and listify functions into the library; introduced versions that have a type argument diff -r 6f9735c15d18 -r 7430e07a5d61 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Fri Dec 10 19:01:44 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Sun Dec 12 00:10:40 2010 +0000 @@ -24,9 +24,10 @@ "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" -term "bn" - - +ML {* + Variable.import; + Variable.import true @{thms foo.exhaust} @{context} +*} thm foo.bn_defs thm foo.permute_bn @@ -42,7 +43,7 @@ thm foo.fv_defs thm foo.bn_defs thm foo.perm_simps -thm foo.eq_iff(5) +thm foo.eq_iff thm foo.fv_bn_eqvt thm foo.size_eqvt thm foo.supports @@ -52,6 +53,7 @@ +text {* *} diff -r 6f9735c15d18 -r 7430e07a5d61 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Fri Dec 10 19:01:44 2010 +0000 +++ b/Nominal/Nominal2.thy Sun Dec 12 00:10:40 2010 +0000 @@ -15,6 +15,8 @@ use "nominal_dt_quot.ML" ML {* open Nominal_Dt_Quot *} +text {* TEST *} + ML {* fun strip_prems_concl trm = (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) @@ -23,10 +25,29 @@ | strip_outer_params B = ([], B) *} + +ML {* +fun binders bclauses = + let + fun aux1 (NONE, i) = Bound i + | aux1 (SOME bn, i) = bn $ Bound i + in + bclauses + |> map (fn (BC (_, x, _)) => x) + |> flat + |> map aux1 + end +*} + ML {* fun prove_strong_exhausts lthy qexhausts qtrms bclausess = let - val (cses, main_concls) = qexhausts + val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy + + val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' + val c = Free (c, TFree (a, @{sort fs})) + + val (cses, main_concls) = qexhausts' |> map prop_of |> map strip_prems_concl |> split_list @@ -36,12 +57,15 @@ val (params, (body, concl)) = cse |> strip_outer_params ||> Logic.dest_implies + + (*val bnds = HOLogic.mk_tuple (binders bclauses)*) + val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (c, c)) in - Logic.mk_implies (body, concl) + Logic.mk_implies (prem, Logic.mk_implies (body, concl)) end val cses' = map2 (map2 process_case) cses bclausess - |> map (map (Syntax.string_of_term lthy)) + |> map (map (Syntax.string_of_term lthy'')) |> map commas |> cat_lines diff -r 6f9735c15d18 -r 7430e07a5d61 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Fri Dec 10 19:01:44 2010 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Sun Dec 12 00:10:40 2010 +0000 @@ -18,21 +18,10 @@ datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list - val is_atom: Proof.context -> typ -> bool - val is_atom_set: Proof.context -> typ -> bool - val is_atom_fset: Proof.context -> typ -> bool - val is_atom_list: Proof.context -> typ -> bool - val mk_atom_set: term -> term - val mk_atom_fset: term -> term - - val setify: Proof.context -> term -> term - val listify: Proof.context -> term -> term - val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> (term list * thm list * bn_info list * thm list * local_theory) - val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory @@ -71,83 +60,6 @@ fun lookup xs x = the (AList.lookup (op=) xs x) -(* testing for concrete atom types *) -fun is_atom ctxt ty = - Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) - -fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t - | is_atom_set _ _ = false; - -fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t - | is_atom_fset _ _ = false; - -fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t - | is_atom_list _ _ = false - - -(* functions for producing sets, fsets and lists of general atom type - out from concrete atom types *) -fun mk_atom_set t = - let - val ty = fastype_of t; - val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; - val img_ty = atom_ty --> ty --> @{typ "atom set"}; - in - Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t - end - - -fun dest_fsetT (Type (@{type_name fset}, [T])) = T - | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); - -fun mk_atom_fset t = - let - val ty = fastype_of t; - val atom_ty = dest_fsetT ty - val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; - val fset = @{term "fset :: atom fset => atom set"} - in - fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t) - end - - fun mk_atom_list t = - let - val ty = fastype_of t - val atom_ty = dest_listT ty - val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} - in - Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t - end - -(* functions that coerces singletons, sets and fsets of concrete atoms - into sets of general atoms *) -fun setify ctxt t = - let - val ty = fastype_of t; - in - if is_atom ctxt ty - then HOLogic.mk_set @{typ atom} [mk_atom t] - else if is_atom_set ctxt ty - then mk_atom_set t - else if is_atom_fset ctxt ty - then mk_atom_fset t - else raise TERM ("setify", [t]) - end - -(* functions that coerces singletons and lists of concrete atoms - into lists of general atoms *) -fun listify ctxt t = - let - val ty = fastype_of t; - in - if is_atom ctxt ty - then HOLogic.mk_list @{typ atom} [mk_atom t] - else if is_atom_list ctxt ty - then mk_atom_list t - else raise TERM ("listify", [t]) - end - - (** functions that define the raw binding functions **) (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or diff -r 6f9735c15d18 -r 7430e07a5d61 Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Fri Dec 10 19:01:44 2010 +0000 +++ b/Nominal/nominal_library.ML Sun Dec 12 00:10:40 2010 +0000 @@ -12,6 +12,7 @@ val is_true: term -> bool val dest_listT: typ -> typ + val dest_fsetT: typ -> typ val mk_id: term -> term @@ -34,6 +35,28 @@ val mk_atom_ty: typ -> term -> term val mk_atom: term -> term + val mk_atom_set_ty: typ -> term -> term + val mk_atom_set: term -> term + val mk_atom_fset_ty: typ -> term -> term + val mk_atom_fset: term -> term + val mk_atom_list_ty: typ -> term -> term + val mk_atom_list: term -> term + + val is_atom: Proof.context -> typ -> bool + val is_atom_set: Proof.context -> typ -> bool + val is_atom_fset: Proof.context -> typ -> bool + val is_atom_list: Proof.context -> typ -> bool + + val setify_ty: Proof.context -> typ -> term -> term + val setify: Proof.context -> term -> term + val listify_ty: Proof.context -> typ -> term -> term + val listify: Proof.context -> term -> term + + val fresh_ty: typ -> typ -> typ + val fresh_star_const: typ -> typ -> term + val mk_fresh_star_ty: typ -> typ -> term -> term -> term + val mk_fresh_star: term -> term -> term + val supp_ty: typ -> typ val supp_const: typ -> term val mk_supp_ty: typ -> term -> term @@ -110,6 +133,10 @@ fun dest_listT (Type (@{type_name list}, [T])) = T | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) +fun dest_fsetT (Type (@{type_name fset}, [T])) = T + | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); + + fun mk_id trm = let val ty = fastype_of trm @@ -150,6 +177,79 @@ fun mk_atom_ty ty t = atom_const ty $ t; fun mk_atom t = mk_atom_ty (fastype_of t) t; +fun mk_atom_set_ty ty t = + let + val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; + val img_ty = atom_ty --> ty --> @{typ "atom set"}; + in + Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t + end + +fun mk_atom_fset_ty ty t = + let + val atom_ty = dest_fsetT ty + val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; + val fset = @{term "fset :: atom fset => atom set"} + in + fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t) + end + +fun mk_atom_list_ty ty t = + let + val atom_ty = dest_listT ty + val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} + in + Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t + end + +fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t +fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t +fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t + + + +(* testing for concrete atom types *) +fun is_atom ctxt ty = + Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) + +fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t + | is_atom_set _ _ = false; + +fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t + | is_atom_fset _ _ = false; + +fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t + | is_atom_list _ _ = false + + +(* functions that coerces singletons, sets and fsets of concrete atoms + into sets of general atoms *) +fun setify_ty ctxt ty t = + if is_atom ctxt ty + then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] + else if is_atom_set ctxt ty + then mk_atom_set_ty ty t + else if is_atom_fset ctxt ty + then mk_atom_fset_ty ty t + else raise TERM ("setify", [t]) + +(* functions that coerces singletons and lists of concrete atoms + into lists of general atoms *) +fun listify_ty ctxt ty t = + if is_atom ctxt ty + then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] + else if is_atom_list ctxt ty + then mk_atom_list_ty ty t + else raise TERM ("listify", [t]) + +fun setify ctxt t = setify_ty ctxt (fastype_of t) t +fun listify ctxt t = listify_ty ctxt (fastype_of t) t + +fun fresh_ty ty1 ty2 = [ty1, ty2] ---> @{typ bool} +fun fresh_star_const ty1 ty2 = Const (@{const_name fresh_star}, fresh_ty ty1 ty2) +fun mk_fresh_star_ty ty1 ty2 t1 t2 = fresh_star_const ty1 ty2 $ t1 $ t2 +fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t1) (fastype_of t2) t1 t2 + fun supp_ty ty = ty --> @{typ "atom set"}; fun supp_const ty = Const (@{const_name supp}, supp_ty ty) fun mk_supp_ty ty t = supp_const ty $ t