# HG changeset patch # User Christian Urban # Date 1282698126 -28800 # Node ID 331873ebc5cd51f1e5f0976db8366ccaff895c2b # Parent a746d49b024058d411959c394453e727c4fa24fb can now deal with type variables in nominal datatype definitions diff -r a746d49b0240 -r 331873ebc5cd Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Sun Aug 22 14:02:49 2010 +0800 +++ b/Nominal/Ex/Lambda.thy Wed Aug 25 09:02:06 2010 +0800 @@ -3,14 +3,104 @@ begin atom_decl name -declare [[STEPS = 2]] +declare [[STEPS = 20]] -nominal_datatype 'a lam = +class s1 +class s2 + +nominal_datatype lambda: + ('a, 'b) lam = Var "name" -| App "'a lam" "'a lam" -| Lam x::"name" l::"'a lam" bind x in l +| App "('a::s1, 'b::s2) lam" "('a, 'b) lam" +| Lam x::"name" l::"('a, 'b) lam" bind x in l + +term Var_raw +term Var +term App_raw +term App +thm Var_def App_def Lam_def +term abs_lam + +thm distinct +thm lam_raw.inducts +thm lam_raw.exhaust +thm fv_defs +thm bn_defs +thm perm_simps +thm perm_laws +thm lam_raw.size +thm eq_iff +thm eq_iff_simps +thm fv_eqvt +thm bn_eqvt +thm size_eqvt + +ML {* + val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}] +*} + +ML {* + val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct}) +*} + +ML {* + val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct} +*} + +ML {* + val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust} +*} + +ML {* + val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs} +*} -ML {* Datatype.read_typ *} +ML {* + val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps} +*} + +ML {* + val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws} +*} + +ML {* + val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps + prod.cases} +*} + +(* HERE *) + +ML {* + val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff} +*} + +ML {* + val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps} +*} + + +ML {* + val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs} +*} + +ML {* + val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt} +*} + +ML {* + val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt} +*} + +ML {* + val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt} +*} + + + +ML {* + space_explode "_raw" "bla_raw2_foo_raw3.0" +*} + thm eq_iff diff -r a746d49b0240 -r 331873ebc5cd Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sun Aug 22 14:02:49 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Wed Aug 25 09:02:06 2010 +0800 @@ -6,8 +6,7 @@ declare [[STEPS = 20]] - -nominal_datatype trm = +nominal_datatype singlelet: trm = Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bind x in t @@ -23,8 +22,6 @@ "bn (As x y t) = {atom x}" -ML {* Function.prove_termination *} - text {* can lift *} thm distinct @@ -32,6 +29,7 @@ thm trm_raw.exhaust thm assg_raw.exhaust thm fv_defs +thm bn_defs thm perm_simps thm perm_laws thm trm_raw_assg_raw.size(9 - 16) @@ -42,8 +40,6 @@ thm bn_eqvt thm size_eqvt -ML {* lift_thm *} - ML {* val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct}) @@ -108,6 +104,7 @@ + lemma supp_fv: "supp t = fv_trm t" "supp b = fv_bn b" diff -r a746d49b0240 -r 331873ebc5cd Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sun Aug 22 14:02:49 2010 +0800 +++ b/Nominal/NewParser.thy Wed Aug 25 09:02:06 2010 +0800 @@ -5,11 +5,6 @@ "Perm" "Tacs" "Equivp" begin -(* TODO - - we need to also export a cases-rule for nominal datatypes - size function -*) section{* Interface for nominal_datatype *} @@ -38,16 +33,6 @@ *} -ML {* -fun add_datatype_wrapper dt_names dts = -let - val conf = Datatype.default_config -in - Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) -end -*} - - text {* Infrastructure for adding "_raw" to types and terms *} ML {* @@ -141,11 +126,12 @@ *} ML {* +(** definition of the raw binding functions **) + +(* TODO: needs cleaning *) fun find [] _ = error ("cannot find element") | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y -*} -ML {* fun prep_bn_info lthy dt_names dts eqs = let fun aux eq = @@ -182,12 +168,33 @@ in ordered' end + + +fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = + if null raw_bn_funs + then ([], [], [], [], lthy) + else + let + val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs + Function_Common.default_config (pat_completeness_simp constr_thms) lthy + + val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1) + val {fs, simps, inducts, ...} = info + + val raw_bn_induct = (the inducts) + val raw_bn_eqs = the simps + + val raw_bn_info = + prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) + in + (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) + end *} ML {* fun define_raw_dts dts bn_funs bn_eqs binds lthy = let - val thy = ProofContext.theory_of lthy + 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 @@ -212,36 +219,15 @@ val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds - val (raw_dt_full_names, lthy1) = - add_datatype_wrapper raw_dt_names raw_dts lthy + val (raw_dt_full_names, thy1) = + Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy + + val lthy1 = Named_Target.theory_init thy1 in (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) end *} -ML {* -(* should be in nominal_dt_rawfuns *) -fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = - if null raw_bn_funs - then ([], [], [], [], lthy) - else - let - val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs - Function_Common.default_config (pat_completeness_simp constr_thms) lthy - - val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1) - val {fs, simps, inducts, ...} = info - - val raw_bn_induct = (the inducts) - val raw_bn_eqs = the simps - - val raw_bn_info = - prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) - in - (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) - end -*} - ML {* (* for testing porposes - to exit the procedure early *) @@ -255,7 +241,7 @@ setup STEPS_setup ML {* -fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = +fun nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatypes *) val _ = warning "Definition of raw datatypes"; @@ -269,7 +255,10 @@ val raw_tys = all_dtyps descr sorts val raw_full_ty_names = map (fst o dest_Type) raw_tys - + val tvs = hd raw_tys + |> snd o dest_Type + |> map dest_TFree + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names val raw_cns_info = all_dtyp_constrs_types descr sorts @@ -289,7 +278,7 @@ val _ = warning "Definition of raw permutations"; val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = if get_STEPS lthy0 > 1 - then define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm lthy0 + then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0 else raise TEST lthy0 (* noting the raw permutations as eqvt theorems *) @@ -450,7 +439,7 @@ map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms val qperm_descr = - map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs + map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs val qsize_descr = map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms @@ -469,12 +458,12 @@ (* definition of the quotient permfunctions and pt-class *) val lthy9 = if get_STEPS lthy > 18 - then define_qperms qtys qty_full_names qperm_descr raw_perm_laws lthy8 + then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 else raise TEST lthy8 val lthy9a = if get_STEPS lthy > 19 - then define_qsizes qtys qty_full_names qsize_descr lthy9 + then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 else raise TEST lthy9 val qconstrs = map #qconst qconstrs_info @@ -482,10 +471,8 @@ val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info val qalpha_bns = map #qconst qalpha_bns_info - (* temporary theorem bindings *) - val (_, lthy9') = lthy9a |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) @@ -515,13 +502,13 @@ val bn_nos = map (fn (_, i, _) => i) raw_bn_info; val bns = raw_bns ~~ bn_nos; - val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy8; + val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy9'; val (bns_rsp_pre, lthy9) = fold_map ( fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => - resolve_tac bns_rsp_pre' 1)) bns lthy8; + resolve_tac bns_rsp_pre' 1)) bns lthy9'; val bns_rsp = flat (map snd bns_rsp_pre); - fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; + fun fv_rsp_tac _ = fvbv_rsp_tac alpha_induct raw_fv_defs lthy9' 1; val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos @@ -560,12 +547,12 @@ val _ = warning "Lifting permutations"; val perm_names = map (fn x => "permute_" ^ x) qty_names val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs - val lthy13 = define_qperms qtys qty_full_names dd raw_perm_laws lthy12c + val lthy13 = define_qperms qtys qty_full_names [] dd raw_perm_laws lthy12c val q_name = space_implode "_" qty_names; fun suffix_bind s = Binding.qualify true q_name (Binding.name s); val _ = warning "Lifting induction"; - val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; + val constr_names = map (Long_Name.base_name o fst o dest_Const) []; val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys [] raw_induct_thm); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); @@ -597,7 +584,7 @@ val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = warning "Supports"; - val supports = map (prove_supports lthy20 q_perm) qconstrs; + val supports = map (prove_supports lthy20 q_perm) []; val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); val thy3 = Local_Theory.exit_global lthy20; val _ = warning "Instantiating FS"; @@ -619,38 +606,46 @@ section {* Preparing and parsing of the specification *} ML {* -(* parsing the datatypes and declaring *) -(* constructors in the local theory *) -fun prepare_dts dt_strs lthy = +(* generates the parsed datatypes and + declares the constructors +*) +fun prepare_dts dt_strs thy = let - val thy = ProofContext.theory_of lthy - - fun mk_type full_tname tvrs = - Type (full_tname, map (fn a => TFree (a, @{sort "{pt, fs}"})) tvrs) + fun inter_fs_sort thy (a, S) = + (a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S)) - fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) = + fun mk_type tname sorts (cname, cargs, mx) = let - val tys = map (Syntax.read_typ lthy o snd) anno_tys - val ty = mk_type full_tname tvs + val full_tname = Sign.full_name thy tname + val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts) in - ((cname, tys ---> ty, mx), (cname, tys, mx)) + (cname, cargs ---> ty, mx) + 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_dt (tvs, tname, mx, cnstrs) = - let - val full_tname = Sign.full_name thy tname - val (cnstrs', cnstrs'') = - split_list (map (prep_cnstr full_tname tvs) cnstrs) - in - (cnstrs', (tvs, tname, mx, cnstrs'')) - end + fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) = + let + val (constrs', sorts') = + fold prep_constr constrs ([], sorts) - val (cnstrs, dts) = split_list (map prep_dt dt_strs) + val constr_trms' = + map (mk_type tname (rev sorts')) constrs' + in + (constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts') + end - val _ = tracing ("Contructors:\n" ^ cat_lines (map @{make_string} cnstrs)) + val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []); in - lthy - |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) + thy + |> Sign.add_consts_i constr_trms |> pair dts end *} @@ -658,17 +653,19 @@ ML {* (* parsing the binding function specification and *) (* declaring the functions in the local theory *) -fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = +fun prepare_bn_funs bn_fun_strs bn_eq_strs thy = let - val ((bn_funs, bn_eqs), _) = + val lthy = Named_Target.theory_init thy + + val ((bn_funs, bn_eqs), lthy') = Specification.read_spec bn_fun_strs bn_eq_strs lthy fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) val bn_funs' = map prep_bn_fun bn_funs in - lthy - |> Local_Theory.theory (Sign.add_consts_i bn_funs') + (Local_Theory.exit_global lthy') + |> Sign.add_consts_i bn_funs' |> pair (bn_funs', bn_eqs) end *} @@ -691,14 +688,14 @@ *} ML {* -fun prepare_bclauses dt_strs lthy = +fun prepare_bclauses dt_strs thy = let val annos_bclauses = get_cnstrs dt_strs |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) fun prep_binder env bn_str = - case (Syntax.read_term lthy bn_str) of + case (Syntax.read_term_global thy bn_str) of Free (x, _) => (NONE, index_lookup env x) | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") @@ -720,7 +717,7 @@ map (prep_bclause env) bclause_strs end in - map (map prep_bclauses) annos_bclauses + (map (map prep_bclauses) annos_bclauses, thy) end *} @@ -732,7 +729,8 @@ ML {* fun included i bcs = let - fun incl (BC (_, bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i) + fun incl (BC (_, bns, bds)) = + member (op =) (map snd bns) i orelse member (op =) bds i in exists incl bcs end @@ -757,17 +755,28 @@ *} ML {* -fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = +fun nominal_datatype2_cmd (opt_thm_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = let - fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) - val lthy0 = - Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy - val (dts, lthy1) = prepare_dts dt_strs lthy0 - val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 - val bclauses = prepare_bclauses dt_strs lthy2 - val bclauses' = complete dt_strs bclauses + val (pre_typ_names, pre_typs) = split_list + (map (fn (tvs, tname, mx, _) => + (Binding.name_of tname, (tname, length tvs, mx))) dt_strs) + + (* this theory is used just for parsing *) + val thy = ProofContext.theory_of lthy + val tmp_thy = Theory.copy thy + + val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = + tmp_thy + |> Sign.add_types pre_typs + |> prepare_dts dt_strs + ||>> prepare_bn_funs bn_fun_strs bn_eq_strs + ||>> prepare_bclauses dt_strs + + val bclauses' = complete dt_strs bclauses + val thm_name = + the_default (Binding.name (space_implode "_" pre_typ_names)) opt_thm_name in - timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd) + timeit (fn () => nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses' lthy |> snd) end *} @@ -777,33 +786,32 @@ structure P = Parse; structure S = Scan - fun triple1 ((x, y), z) = (x, y, z) - fun triple2 (x, (y, z)) = (x, y, z) - fun tuple ((x, y, z), u) = (x, y, z, u) - fun tswap (((x, y), z), u) = (x, y, u, z) + fun triple ((x, y), z) = (x, y, 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) in val _ = Keyword.keyword "bind" -val _ = Keyword.keyword "set" -val _ = Keyword.keyword "res" -val _ = Keyword.keyword "list" + +val opt_name = Scan.option (P.binding --| Args.colon) val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ val bind_mode = P.$$$ "bind" |-- S.optional (Args.parens - (P.$$$ "list" >> K Lst || P.$$$ "set" >> K Set || P.$$$ "res" >> K Res)) Lst + (Args.$$$ "list" >> K Lst || Args.$$$ "set" >> K Set || Args.$$$ "res" >> K Res)) Lst val bind_clauses = - P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) + P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple) val cnstr_parser = - P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap + P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2 (* datatype parser *) val dt_parser = - (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- - (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple + (P.type_args -- P.binding -- P.opt_mixfix >> triple) -- + (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1 (* binding function parser *) val bnfun_parser = @@ -811,12 +819,11 @@ (* main parser *) val main_parser = - P.and_list1 dt_parser -- bnfun_parser >> triple2 + opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 end (* Command Keyword *) - val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl (main_parser >> nominal_datatype2_cmd) *} diff -r a746d49b0240 -r 331873ebc5cd Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Sun Aug 22 14:02:49 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Wed Aug 25 09:02:06 2010 +0800 @@ -240,7 +240,7 @@ val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) - + val (alphas, lthy') = Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} @@ -252,12 +252,13 @@ val alpha_cases_loc = #elims alphas; val phi = ProofContext.export_morphism lthy' lthy; - val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc; + val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc + val (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy val alpha_induct = Morphism.thm phi alpha_induct_loc; val alpha_intros = map (Morphism.thm phi) alpha_intros_loc val alpha_cases = map (Morphism.thm phi) alpha_cases_loc - val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms + val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms' in (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') end @@ -289,12 +290,16 @@ fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys = let + (* proper import of type-variables does not work, + since ther are replaced by new variables, messing + up the ty_term assoc list *) + val distinct_thms' = map Thm.legacy_freezeT distinct_thms val ty_trm_assoc = alpha_tys ~~ alpha_trms fun mk_alpha_distinct distinct_trm = let val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt - val goal = mk_distinct_goal ty_trm_assoc trm' + val goal = mk_distinct_goal ty_trm_assoc distinct_trm in Goal.prove ctxt' [] [] goal (K (distinct_tac cases_thms distinct_thms 1)) @@ -302,7 +307,8 @@ end in - map (mk_alpha_distinct o prop_of) distinct_thms + map (mk_alpha_distinct o prop_of) distinct_thms' + |> map Thm.varifyT_global end diff -r a746d49b0240 -r 331873ebc5cd Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Sun Aug 22 14:02:49 2010 +0800 +++ b/Nominal/nominal_dt_quot.ML Wed Aug 25 09:02:06 2010 +0800 @@ -13,11 +13,11 @@ val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> Quotient_Info.qconsts_info list * local_theory - val define_qperms: typ list -> string list -> (string * term * mixfix) list -> - thm list -> local_theory -> local_theory + val define_qperms: typ list -> string list -> (string * sort) list -> + (string * term * mixfix) list -> thm list -> local_theory -> local_theory - val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> - local_theory -> local_theory + val define_qsizes: typ list -> string list -> (string * sort) list -> + (string * term * mixfix) list -> local_theory -> local_theory val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm end @@ -47,46 +47,62 @@ (* defines the quotient permutations and proves pt-class *) -fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws lthy = +fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = let - val lthy' = + val _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys)) + + val lthy1 = lthy |> Local_Theory.exit_global - |> Class.instantiation (qfull_ty_names, [], @{sort pt}) + |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) - val (_, lthy'') = define_qconsts qtys perm_specs lthy' + val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 + + val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 - val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys []) raw_perm_laws + val lifted_perm_laws = + map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' + |> Variable.exportT lthy3 lthy2 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac lifted_perm_laws)) in - lthy'' + lthy2 |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end (* defines the size functions and proves size-class *) -fun define_qsizes qtys qfull_ty_names size_specs lthy = +fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = let fun tac _ = Class.intro_classes_tac [] in lthy |> Local_Theory.exit_global - |> Class.instantiation (qfull_ty_names, [], @{sort size}) + |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) |> snd o (define_qconsts qtys size_specs) |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end -(* lifts a theorem and deletes all "_raw" suffixes *) +(* lifts a theorem and cleans all "_raw" instances + from variable names *) -fun unraw_str s = - unsuffix "_raw" s - handle Fail _ => s +local + val any = Scan.one (Symbol.not_eof) + val raw = Scan.this_string "_raw" + val exclude = + Scan.repeat (Scan.unless raw any) --| raw >> implode + val parser = Scan.repeat (exclude || any) +in + fun unraw_str s = + s |> explode + |> Scan.finite Symbol.stopper parser >> implode + |> fst +end fun unraw_vars_thm thm = let @@ -111,6 +127,7 @@ |> Quotient_Tacs.lifted ctxt qtys simps |> unraw_bounds_thm |> unraw_vars_thm + |> Drule.zero_var_indexes end (* structure *) diff -r a746d49b0240 -r 331873ebc5cd Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Sun Aug 22 14:02:49 2010 +0800 +++ b/Nominal/nominal_dt_rawfuns.ML Wed Aug 25 09:02:06 2010 +0800 @@ -7,9 +7,13 @@ signature NOMINAL_DT_RAWFUNS = sig - (* info of binding functions *) + (* 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) list + (* binding modes and binding clauses *) datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list @@ -24,6 +28,11 @@ val setify: Proof.context -> term -> term val listify: Proof.context -> term -> term + (* TODO: should be here + 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 * thm list * local_theory) *) + val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory @@ -34,6 +43,14 @@ structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = 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 int * term option - is number of the corresponding argument with possibly @@ -41,6 +58,7 @@ *) type bn_info = (term * int * (int * term option) list list) list + datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list @@ -127,6 +145,7 @@ else t + (** functions that construct the equations for fv and fv_bn **) fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = @@ -239,12 +258,12 @@ val {fs, simps, inducts, ...} = info; val morphism = ProofContext.export_morphism lthy'' lthy - val fs_exp = map (Morphism.term morphism) fs val simps_exp = map (Morphism.thm morphism) (the simps) val inducts_exp = map (Morphism.thm morphism) (the inducts) - val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp + + val (fvs', fv_bns') = chop (length fv_frees) fs in - (fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'') + (fvs', fv_bns', simps_exp, inducts_exp, lthy'') end diff -r a746d49b0240 -r 331873ebc5cd Nominal/nominal_dt_rawperm.ML --- a/Nominal/nominal_dt_rawperm.ML Sun Aug 22 14:02:49 2010 +0800 +++ b/Nominal/nominal_dt_rawperm.ML Wed Aug 25 09:02:06 2010 +0800 @@ -9,8 +9,8 @@ signature NOMINAL_DT_RAWPERM = sig - val define_raw_perms: string list -> typ list -> term list -> thm -> local_theory -> - (term list * thm list * thm list) * local_theory + val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm -> + local_theory -> (term list * thm list * thm list) * local_theory end @@ -90,7 +90,7 @@ end -fun define_raw_perms full_ty_names tys constrs induct_thm lthy = +fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = let val perm_fn_names = full_ty_names |> map Long_Name.base_name @@ -113,7 +113,7 @@ val ((perm_funs, perm_eq_thms), lthy') = lthy |> Local_Theory.exit_global - |> Class.instantiation (full_ty_names, [], @{sort pt}) + |> Class.instantiation (full_ty_names, tvs, @{sort pt}) |> Primrec.add_primrec perm_fn_binds perm_eqs val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'