# HG changeset patch # User Christian Urban # Date 1323966042 0 # Node ID 51ef8a3cb6ef773ef1ead9a2b3f7866db5f85bc9 # Parent ade2f8fcf8e84c2be044a9df624f986b5934e98a updated to lates changes in the datatype package diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/Datatypes.thy --- a/Nominal/Ex/Datatypes.thy Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/Ex/Datatypes.thy Thu Dec 15 16:20:42 2011 +0000 @@ -8,7 +8,7 @@ atom_decl - example by John Matthews *) -nominal_datatype 'a Maybe = +nominal_datatype 'a::fs Maybe = Nothing | Just 'a diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/Finite_Alpha.thy --- a/Nominal/Ex/Finite_Alpha.thy Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/Ex/Finite_Alpha.thy Thu Dec 15 16:20:42 2011 +0000 @@ -8,7 +8,12 @@ and "p \ as = bs" shows "(as, x) \set (op =) supp p (bs, y)" using assms unfolding alphas - by (metis Diff_eqvt atom_set_perm_eq supp_eqvt) + apply(simp) + apply(clarify) + apply(simp only: Diff_eqvt[symmetric] supp_eqvt[symmetric]) + apply(simp only: atom_set_perm_eq) + done + lemma assumes "(supp x - set as) \* p" @@ -16,7 +21,11 @@ and "p \ as = bs" shows "(as, x) \lst (op =) supp p (bs, y)" using assms unfolding alphas - by (metis Diff_eqvt atom_set_perm_eq supp_eqvt supp_of_atom_list) + apply(simp) + apply(clarify) + apply(simp only: set_eqvt[symmetric] Diff_eqvt[symmetric] supp_eqvt[symmetric]) + apply(simp only: atom_set_perm_eq) + done lemma assumes "(supp x - as) \* p" @@ -32,8 +41,8 @@ apply (rule trans) apply (rule supp_perm_eq[symmetric, of _ p]) apply (simp add: supp_finite_atom_set fresh_star_def) - apply blast - apply (simp add: eqvts) + apply(auto)[1] + apply(simp only: Diff_eqvt inter_eqvt supp_eqvt) apply (simp add: fresh_star_def) apply blast done diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/Ex/Lambda.thy Thu Dec 15 16:20:42 2011 +0000 @@ -169,7 +169,7 @@ | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])" | "atom x \ (y, s) \ (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])" apply(simp add: eqvt_def subst'_graph_def) - apply (rule, perm_simp, rule) + apply(perm_simp, simp) apply(rule TrueI) apply(case_tac x) apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/LetRec2.thy --- a/Nominal/Ex/LetRec2.thy Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/Ex/LetRec2.thy Thu Dec 15 16:20:42 2011 +0000 @@ -22,6 +22,11 @@ thm trm_assn.eq_iff thm trm_assn.supp +ML {* +@{term Trueprop} ; +@{const_name HOL.eq} +*} + thm trm_assn.fv_defs thm trm_assn.eq_iff thm trm_assn.bn_defs diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/Ex/TypeVarsTest.thy Thu Dec 15 16:20:42 2011 +0000 @@ -17,9 +17,9 @@ instance nat :: s1 .. instance int :: s2 .. -nominal_datatype ('a, 'b, 'c) lam = +nominal_datatype ('a::"{s1,fs}", 'b::"{s2,fs}", 'c::at) lam = Var "name" -| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam" +| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam" | Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l | Foo "'a" "'b" | Bar x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *) @@ -41,11 +41,11 @@ nominal_datatype ('alpha, 'beta, 'gamma) psi = PsiNil -| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" +| Output "'alpha::fs" "'alpha::fs" "('alpha::fs, 'beta::fs, 'gamma::fs) psi" nominal_datatype 'a foo = - Node x::"name" f::"'a foo" binds x in f + Node x::"name" f::"('a::fs) foo" binds x in f | Leaf "'a" term "Leaf" diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/Nominal2.thy Thu Dec 15 16:20:42 2011 +0000 @@ -60,10 +60,10 @@ ML {* fun get_cnstrs dts = - map (fn (_, _, _, constrs) => constrs) dts + map snd dts fun get_typed_cnstrs dts = - flat (map (fn (_, bn, _, constrs) => + flat (map (fn ((bn, _, _), constrs) => (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) fun get_cnstr_strs dts = @@ -94,8 +94,8 @@ fun raw_dts_aux1 (bind, tys, _) = (raw_bind bind, map (replace_typ ty_ss) tys, NoSyn) - fun raw_dts_aux2 (ty_args, bind, _, constrs) = - (ty_args, raw_bind bind, NoSyn, map raw_dts_aux1 constrs) + fun raw_dts_aux2 ((bind, ty_args, _), constrs) = + ((raw_bind bind, ty_args, NoSyn), map raw_dts_aux1 constrs) in map raw_dts_aux2 dts end @@ -146,7 +146,7 @@ val thy = Local_Theory.exit_global lthy val thy_name = Context.theory_name thy - val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts + val dt_names = map (fn ((s, _, _), _) => Binding.name_of s) dts val dt_full_names = map (Long_Name.qualify thy_name) dt_names val dt_full_names' = add_raws dt_full_names val dts_env = dt_full_names ~~ dt_full_names' @@ -333,7 +333,7 @@ alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 val _ = trace_msg (K "Defining the quotient types...") - val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts + val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts val (qty_infos, lthy7) = let @@ -527,45 +527,58 @@ section {* Preparing and parsing of the specification *} +ML {* +fun parse_spec ctxt ((tname, tvs, mx), constrs) = +let + val tvs' = map (apsnd (Typedecl.read_constraint ctxt)) tvs + val constrs' = constrs + |> map (fn (c, Ts, mx', bns) => (c, map ((Syntax.parse_typ ctxt) o snd) Ts, mx')) +in + ((tname, tvs', mx), constrs') +end + +fun check_specs ctxt specs = + let + fun prep_spec ((tname, args, mx), constrs) tys = + let + val (args', tys1) = chop (length args) tys; + val (constrs', tys3) = (constrs, tys1) |-> fold_map (fn (cname, cargs, mx') => fn tys2 => + let val (cargs', tys3) = chop (length cargs) tys2; + in ((cname, cargs', mx'), tys3) end); + in + (((tname, map dest_TFree args', mx), constrs'), tys3) + end + + val all_tys = + specs |> maps (fn ((_, args, _), cs) => map TFree args @ maps #2 cs) + |> Syntax.check_typs ctxt; + + in + #1 (fold_map prep_spec specs all_tys) + end +*} + ML {* (* generates the parsed datatypes and declares the constructors *) fun prepare_dts dt_strs thy = let - fun inter_fs_sort thy (a, S) = - (a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S)) - - fun mk_type tname sorts (cname, cargs, mx) = - let - val full_tname = Sign.full_name thy tname - val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts) - in - (cname, cargs ---> ty, mx) - end + val ctxt = Proof_Context.init_global thy + |> fold (fn ((_, args, _), _) => fold (fn (a, _) => + Variable.declare_typ (TFree (a, dummyS))) args) dt_strs + + val dts = check_specs ctxt (map (parse_spec ctxt) dt_strs) + + fun mk_constr_trms ((tname, tvs, _), constrs) = + let + val full_tname = Sign.full_name thy tname + val ty = Type (full_tname, map TFree tvs) + in + map (fn (c, tys, mx) => (c, tys ---> ty, mx)) constrs + end - fun prep_constr (cname, cargs, mx, _) (constrs, sorts) = - let - val (cargs', sorts') = - fold_map (Datatype.read_typ thy) (map snd cargs) sorts - |>> map (map_type_tfree (TFree o inter_fs_sort thy)) - in - (constrs @ [(cname, cargs', mx)], sorts') - end - - fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) = - let - - val (constrs', sorts') = - fold prep_constr constrs ([], sorts) - - val constr_trms' = - map (mk_type tname (rev sorts')) constrs' - in - (constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts') - end - - val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []); + val constr_trms = flat (map mk_constr_trms dts) in thy |> Sign.add_consts_i constr_trms @@ -681,7 +694,7 @@ fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = let val pre_typs = - map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs + map (fn ((tname, tvs, mx), _) => (tname, length tvs, mx)) dt_strs (* this theory is used just for parsing *) val thy = Proof_Context.theory_of lthy @@ -707,6 +720,7 @@ structure S = Scan fun triple ((x, y), z) = (x, y, z) + fun triple2 ((x, y), z) = (y, x, z) fun tuple1 ((x, y, z), u) = (x, y, z, u) fun tuple2 (((x, y), z), u) = (x, y, u, z) fun tuple3 ((x, y), (z, u)) = (x, y, z, u) @@ -730,8 +744,8 @@ (* datatype parser *) val dt_parser = - (P.type_args -- P.binding -- P.opt_mixfix >> triple) -- - (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1 + (P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) -- + (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) (* binding function parser *) val bnfun_parser = @@ -748,11 +762,6 @@ (main_parser >> nominal_datatype2_cmd) *} -(* -ML {* -trace := true -*} -*) end diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/Nominal2_Base.thy Thu Dec 15 16:20:42 2011 +0000 @@ -2312,6 +2312,9 @@ qed qed + + + lemma supp_perm_perm_eq: assumes a: "\a \ supp x. p \ a = q \ a" shows "p \ x = q \ x" diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/nominal_dt_data.ML --- a/Nominal/nominal_dt_data.ML Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/nominal_dt_data.ML Thu Dec 15 16:20:42 2011 +0000 @@ -5,9 +5,6 @@ signature NOMINAL_DT_DATA = sig - (* info of raw datatypes *) - type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list - (* info of raw binding functions *) type bn_info = term * int * (int * term option) list list @@ -28,7 +25,7 @@ val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list datatype user_data = UserData of - {dts : dt_info, + {dts : Datatype.spec list, cn_names : string list, cn_tys : (string * string) list, bn_funs : (binding * typ * mixfix) list, @@ -37,7 +34,7 @@ datatype raw_dt_info = RawDtInfo of {raw_dt_names : string list, - raw_dts : dt_info, + raw_dts : Datatype.spec list, raw_tys : typ list, raw_ty_args : (string * sort) list, raw_cns_info : cns_info list, @@ -66,13 +63,6 @@ structure Nominal_Dt_Data: NOMINAL_DT_DATA = struct -(* string list - type variables of a datatype - binding - name of the datatype - mixfix - its mixfix - (binding * typ list * mixfix) list - datatype constructors of the type -*) -type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list - (* term - is constant of the bn-function int - is datatype number over which the bn-function is defined @@ -121,7 +111,7 @@ datatype user_data = UserData of - {dts : dt_info, + {dts : Datatype.spec list, cn_names : string list, cn_tys : (string * string) list, bn_funs : (binding * typ * mixfix) list, @@ -130,7 +120,7 @@ datatype raw_dt_info = RawDtInfo of {raw_dt_names : string list, - raw_dts : dt_info, + raw_dts : Datatype.spec list, raw_tys : typ list, raw_ty_args : (string * sort) list, raw_cns_info : cns_info list, diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Thu Dec 15 16:20:11 2011 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Thu Dec 15 16:20:42 2011 +0000 @@ -94,7 +94,7 @@ fun cntrs_order ((bn, dt_index), data) = let val dt = nth dts dt_index - val cts = (fn (_, _, _, x) => x) dt + val cts = snd dt val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts in (bn, (bn, dt_index, order (op=) ct_names data))