# HG changeset patch # User Cezary Kaliszyk # Date 1272631693 -7200 # Node ID f18b8e8a490915eb38072a6c325ab0af6d57ea69 # Parent 4df3441aa0b4d660f4c158913d2580949c1bc536 Merged nominal_datatype into NewParser until eqvts diff -r 4df3441aa0b4 -r f18b8e8a4909 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Fri Apr 30 13:57:59 2010 +0200 +++ b/Nominal/NewFv.thy Fri Apr 30 14:48:13 2010 +0200 @@ -271,17 +271,20 @@ Function.prove_termination NONE (Lexicographic_Order.lexicographic_order_tac true lthy) lthy - val (info, lthy') = Function.add_function all_fv_names all_fv_eqs + val (_, lthy') = Function.add_function all_fv_names all_fv_eqs Function_Common.default_config pat_completeness_auto lthy - val lthy'' = prove_termination (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination (Local_Theory.restore lthy') + + val {fs, simps, ...} = info; val morphism = ProofContext.export_morphism lthy'' lthy - val fv_frees_exp = map (Morphism.term morphism) fv_frees - val fv_bns_exp = map (Morphism.term morphism) fv_bns + val fs_exp = map (Morphism.term morphism) fs + val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp + val simps_exp = Morphism.fact morphism (the simps) in - ((fv_frees_exp, fv_bns_exp), @{thms refl}, lthy'') + ((fv_frees_exp, fv_bns_exp), simps_exp, lthy'') end *} diff -r 4df3441aa0b4 -r f18b8e8a4909 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri Apr 30 13:57:59 2010 +0200 +++ b/Nominal/NewParser.thy Fri Apr 30 14:48:13 2010 +0200 @@ -2,7 +2,7 @@ imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Perm" "NewFv" "NewAlpha" + "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" begin section{* Interface for nominal_datatype *} @@ -266,6 +266,8 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); val {descr, sorts, ...} = dtinfo; + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + val raw_tys = map (fn (i, _) => nth_dtyp i) descr; val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; @@ -283,16 +285,29 @@ fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); + val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc val thy = Local_Theory.exit_global lthy2; val lthy3 = Theory_Target.init NONE thy; + val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a; val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts - + val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); + val bn_tys = map (domain_type o fastype_of) raw_bn_funs; + val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; + val bns = raw_bn_funs ~~ bn_nos; + val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) + (rel_distinct ~~ alpha_ts_nobn)); + val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) + ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) + val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 + val _ = tracing "Proving equivariance"; + val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 + val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 in - ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) + ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy6) end *} @@ -540,6 +555,7 @@ All xs::"name fset" ty::"ty_raw" bind_res xs in ty thm fv_tys_raw.simps thm alpha_tys_raw.intros +thm eqvts (* some further tests *) diff -r 4df3441aa0b4 -r f18b8e8a4909 Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Apr 30 13:57:59 2010 +0200 +++ b/Nominal/Parser.thy Fri Apr 30 14:48:13 2010 +0200 @@ -391,8 +391,7 @@ define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; val (fv, fvbn) = chop (length perms) fv_ts; - val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts - val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct; + val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); val bn_tys = map (domain_type o fastype_of) raw_bn_funs; val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; @@ -476,7 +475,7 @@ snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; - val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct + val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; val q_perm = map (lift_thm qtys lthy14) raw_perm_def; val lthy15 = note_simp_suffix "perm" q_perm lthy14a;