# HG changeset patch # User Christian Urban # Date 1274010087 -3600 # Node ID c39d4fe31100fba43a8cbc261ace16c80bbc517e # Parent b9292bbcffb6f169b98c4f0ba21f160e00237cfa moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat diff -r b9292bbcffb6 -r c39d4fe31100 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Sun May 16 11:00:44 2010 +0100 +++ b/Nominal/Ex/CoreHaskell.thy Sun May 16 12:41:27 2010 +0100 @@ -84,7 +84,7 @@ | "bv_tvs TvsNil = []" | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" | "bv_cvs CvsNil = []" -| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" +| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] @@ -191,13 +191,13 @@ done lemma alpha_perm_bn: - "alpha_bv pat (permute_bv q pat)" - apply(induct pat rule: inducts(9)) + "alpha_bv pt (permute_bv q pt)" + apply(induct pt rule: inducts(9)) apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) done lemma ACons_subst: - "supp (Abs_lst (bv pat) trm) \* q \ (ACons pat trm al) = ACons (permute_bv q pat) (q \ trm) al" + "supp (Abs_lst (bv pt) trm) \* q \ (ACons pt trm al) = ACons (permute_bv q pt) (q \ trm) al" apply (simp only: eq_iff) apply (simp add: alpha_perm_bn) apply (rule_tac x="q" in exI) @@ -352,8 +352,8 @@ and a35: "\trm assoc_lst b. \\c. P7 c trm; \c. P8 c assoc_lst\ \ P7 b (Case trm assoc_lst)" and a36: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (Cast trm ty)" and a37: "\b. P8 b ANil" - and a38: "\pat trm assoc_lst b. \\c. P9 c pat; \c. P7 c trm; \c. P8 c assoc_lst; set (bv (pat)) \* b\ - \ P8 b (ACons pat trm assoc_lst)" + and a38: "\pt trm assoc_lst b. \\c. P9 c pt; \c. P7 c trm; \c. P8 c assoc_lst; set (bv (pt)) \* b\ + \ P8 b (ACons pt trm assoc_lst)" and a39: "\string tvars cvars vars b. \\c. P11 c tvars; \c. P12 c cvars; \c. P10 c vars\ \ P9 b (Kpat string tvars cvars vars)" and a40: "\b. P10 b VsNil" @@ -372,12 +372,12 @@ P6 (f :: 'f :: pt) co_lst \ P7 (g :: 'g :: {pt,fs}) trm \ P8 (h :: 'h :: {pt,fs}) assoc_lst \ - P9 (i :: 'i :: pt) pat \ + P9 (i :: 'i :: pt) pt \ P10 (j :: 'j :: pt) vars \ P11 (k :: 'k :: pt) tvars \ P12 (l :: 'l :: pt) cvars" proof - - have a1: "(\p a. P1 a (p \ tkind))" and "(\p b. P2 b (p \ ckind))" and "(\p c. P3 c (p \ ty))" and "(\p d. P4 d (p \ ty_lst))" and "(\p e. P5 e (p \ co))" and " (\p f. P6 f (p \ co_lst))" and "(\p g. P7 g (p \ trm))" and "(\p h. P8 h (p \ assoc_lst))" and a1:"(\p q i. P9 i (permute_bv p (q \ pat)))" and a2:"(\p q j. P10 j (permute_bv_vs q (p \ vars)))" and a3:"(\p q k. P11 k ( permute_bv_tvs q (p \ tvars)))" and a4:"(\p q l. P12 l (permute_bv_cvs q (p \ cvars)))" + have a1: "(\p a. P1 a (p \ tkind))" and "(\p b. P2 b (p \ ckind))" and "(\p c. P3 c (p \ ty))" and "(\p d. P4 d (p \ ty_lst))" and "(\p e. P5 e (p \ co))" and " (\p f. P6 f (p \ co_lst))" and "(\p g. P7 g (p \ trm))" and "(\p h. P8 h (p \ assoc_lst))" and a1:"(\p q i. P9 i (permute_bv p (q \ pt)))" and a2:"(\p q j. P10 j (permute_bv_vs q (p \ vars)))" and a3:"(\p q k. P11 k ( permute_bv_tvs q (p \ tvars)))" and a4:"(\p q l. P12 l (permute_bv_cvs q (p \ cvars)))" apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts) apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) @@ -637,7 +637,7 @@ apply (simp add: fresh_star_def fresh_def supp_abs eqvts) done then have b: "P1 a (0 \ tkind)" and "P2 b (0 \ ckind)" "P3 c (0 \ ty)" and "P4 d (0 \ ty_lst)" and "P5 e (0 \ co)" and "P6 f (0 \ co_lst)" and "P7 g (0 \ trm)" and "P8 h (0 \ assoc_lst)" by (blast+) - moreover have "P9 i (permute_bv 0 (0 \ pat))" and "P10 j (permute_bv_vs 0 (0 \ vars))" and "P11 k (permute_bv_tvs 0 (0 \ tvars))" and "P12 l (permute_bv_cvs 0 (0 \ cvars))" using a1 a2 a3 a4 by (blast+) + moreover have "P9 i (permute_bv 0 (0 \ pt))" and "P10 j (permute_bv_vs 0 (0 \ vars))" and "P11 k (permute_bv_tvs 0 (0 \ tvars))" and "P12 l (permute_bv_cvs 0 (0 \ cvars))" using a1 a2 a3 a4 by (blast+) ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) qed diff -r b9292bbcffb6 -r c39d4fe31100 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sun May 16 11:00:44 2010 +0100 +++ b/Nominal/NewParser.thy Sun May 16 12:41:27 2010 +0100 @@ -204,22 +204,6 @@ in (dt_index, (bn_fun, (cnstr_head, included))) end - fun aux2 eq = - let - val (lhs, rhs) = eq - |> strip_qnt_body "all" - |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq - val (bn_fun, [cnstr]) = strip_comb lhs - val (_, ty) = dest_Free bn_fun - val (ty_name, _) = dest_Type (domain_type ty) - val dt_index = find_index (fn x => x = ty_name) dt_names - val (cnstr_head, cnstr_args) = strip_comb cnstr - val rhs_elements = strip_bn_fun rhs - val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements - in - (bn_fun, dt_index, (cnstr_head, included)) - end fun order dts i ts = let val dt = nth dts i @@ -235,13 +219,14 @@ val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) - val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs)) + (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) val _ = tracing ("ordered'\n" ^ @{make_string} ordered') in ordered' end *} +ML {* add_primrec_wrapper *} ML {* fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = let @@ -271,14 +256,16 @@ 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_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) - val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) + val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy + val ((raw_bn_funs, raw_bn_eqs), lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 + + val morphism_2_0 = ProofContext.export_morphism lthy2 lthy + fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); + val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; in - lthy - |> add_datatype_wrapper raw_dt_names raw_dts - ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs - ||>> pair raw_bclauses - ||>> pair raw_bns + (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2) end *} @@ -388,7 +375,7 @@ fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatype and raw bn-functions *) - val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = + val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) = if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy else raise TEST lthy @@ -413,32 +400,25 @@ then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 else raise TEST lthy1 - (* definition of raw fv_functions *) - val morphism_2_0 = ProofContext.export_morphism lthy2 lthy - fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); - val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; - val (_, lthy2a) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; val thy = Local_Theory.exit_global lthy2a; val thy_name = Context.theory_name thy + (* definition of raw fv_functions *) val lthy3 = Theory_Target.init NONE thy; - val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; + val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; - val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) - val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) - val ((fv, fvbn), fv_def, lthy3a) = if get_STEPS lthy > 3 - then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 + then define_raw_fv descr sorts raw_bns raw_bclauses lthy3 else raise TEST lthy3 (* definition of raw alphas *) val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = if get_STEPS lthy > 4 - then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a + then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a else raise TEST lthy3a val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts diff -r b9292bbcffb6 -r c39d4fe31100 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Sun May 16 11:00:44 2010 +0100 +++ b/Nominal/ROOT.ML Sun May 16 12:41:27 2010 +0100 @@ -13,7 +13,7 @@ "Ex/Modules", "Ex/ExPS3", "Ex/ExPS7", - (*"Ex/CoreHaskell",*) + "Ex/CoreHaskell", "Ex/Test", "Manual/Term4" ];