# HG changeset patch # User Christian Urban # Date 1311098946 -3600 # Node ID c8acaded17775e12e69a2a11840f1575c031eb46 # Parent e239c9f18144171602d7f2bf54a6e821daad5128 temporary fix diff -r e239c9f18144 -r c8acaded1777 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue Jul 19 10:43:43 2011 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Tue Jul 19 19:09:06 2011 +0100 @@ -53,6 +53,16 @@ apply(simp_all) done +lemma TEST1: + assumes "x = Inl y" + shows "(p \ Sum_Type.Projl x) = Sum_Type.Projl (p \ x)" +using assms by simp + +lemma TEST2: + assumes "x = Inr y" + shows "(p \ Sum_Type.Projr x) = Sum_Type.Projr (p \ x)" +using assms by simp + lemma test: assumes a: "\y. f x = Inl y" shows "(p \ (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \ f) (p \ x))" @@ -275,6 +285,30 @@ apply blast done + +termination (eqvt) by lexicographic_order + +thm subst_substs.eqvt[no_vars] +thm subst_def +thm substs_def +thm Sum_Type.Projr.simps + +lemma + shows "(p \ subst x y) = subst (p \ x) (p \ y)" + and "(p \ substs x' y') = substs (p \ x') (p \ y')" +unfolding subst_def substs_def +thm permute_fun_app_eq +thm Sum_Type.Projl_def sum_rec_def +apply(simp add: permute_fun_def) +unfolding subst_substs_sumC_def +thm subst_substs.eqvt +apply(case_tac x) +apply(simp) +apply(case_tac a) +apply(simp) +thm subst_def +apply(simp) + section {* defined as two separate nominal datatypes *} nominal_datatype ty2 = diff -r e239c9f18144 -r c8acaded1777 Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Tue Jul 19 10:43:43 2011 +0200 +++ b/Nominal/nominal_mutual.ML Tue Jul 19 19:09:06 2011 +0100 @@ -193,9 +193,56 @@ in Goal.prove ctxt [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) - (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) + (fn _ => print_tac "start" + THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs) + THEN (print_tac "second") THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 - THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *) + THEN (print_tac "third") + THEN (simp_tac (simpset_of ctxt)) 1 + THEN (print_tac "fourth") + ) (* FIXME: global simpset?!! *) + |> restore_cond + |> export + end + +val test1 = @{lemma "x = Inl y ==> permute p (Sum_Type.Projl x) = Sum_Type.Projl (permute p x)" by simp} +val test2 = @{lemma "x = Inr y ==> permute p (Sum_Type.Projr x) = Sum_Type.Projr (permute p x)" by simp} + +fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, rhs) + import (export : thm -> thm) sum_psimp_eq = + let + val (MutualPart {f=SOME f, ...}) = get_part fname parts + + val psimp = import sum_psimp_eq + val (simp, restore_cond) = + case cprems_of psimp of + [] => (psimp, I) + | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) + | _ => raise General.Fail "Too many conditions" + + val eqvt_thm' = import eqvt_thm + val (simp', restore_cond') = + case cprems_of eqvt_thm' of + [] => (eqvt_thm, I) + | [cond] => (Thm.implies_elim eqvt_thm' (Thm.assume cond), Thm.implies_intr cond) + | _ => raise General.Fail "Too many conditions" + + val _ = tracing ("sum_psimp:\n" ^ @{make_string} sum_psimp_eq) + val _ = tracing ("psimp:\n" ^ @{make_string} psimp) + val _ = tracing ("simp:\n" ^ @{make_string} simp) + val _ = tracing ("eqvt:\n" ^ @{make_string} eqvt_thm) + + val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt + val p = Free (p, @{typ perm}) + val ss = HOL_basic_ss addsimps [simp RS test1, simp'] + in + Goal.prove ctxt' [] [] + (HOLogic.Trueprop $ + HOLogic.mk_eq (mk_perm p (list_comb (f, args)), list_comb (f, map (mk_perm p) args))) + (fn _ => print_tac "eqvt start" + THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs) + THEN (asm_full_simp_tac ss 1) + THEN all_tac) |> restore_cond |> export end @@ -295,12 +342,15 @@ fun mk_mpsimp fqgar sum_psimp = in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp + fun mk_meqvts fqgar sum_psimp = + in_context lthy fqgar (recover_mutual_eqvt eqvt all_orig_fdefs parts) sum_psimp + val rew_ss = HOL_basic_ss addsimps all_f_defs val mpsimps = map2 mk_mpsimp fqgars psimps val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m val mtermination = full_simplify rew_ss termination val mdomintros = Option.map (map (full_simplify rew_ss)) domintros - val meqvts = [eqvt] (*mk_meqvts lthy eqvt all_f_defs*) + val meqvts = map2 mk_meqvts fqgars psimps in NominalFunctionResult { fs=fs, G=G, R=R, psimps=mpsimps, simple_pinducts=minducts, diff -r e239c9f18144 -r c8acaded1777 Nominal/nominal_termination.ML --- a/Nominal/nominal_termination.ML Tue Jul 19 10:43:43 2011 +0200 +++ b/Nominal/nominal_termination.ML Tue Jul 19 19:09:06 2011 +0100 @@ -52,7 +52,12 @@ val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition pinducts val teqvts = map remove_domain_condition eqvts - + + val _ = tracing ("tot psimps1:\n" ^ cat_lines (map @{make_string} psimps)) + val _ = tracing ("tot psimps2:\n" ^ cat_lines (map @{make_string} tsimps)) + val _ = tracing ("tot induct1:\n" ^ cat_lines (map @{make_string} pinducts)) + val _ = tracing ("tot induct2:\n" ^ cat_lines (map @{make_string} tinduct)) + fun qualify n = Binding.name n |> Binding.qualify true defname in @@ -66,7 +71,7 @@ |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy => let val info' = { is_partial=false, defname=defname, add_simps=add_simps, case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, - simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=eqvts } + simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts } in (info', lthy