diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_mutual.ML Thu Mar 13 09:21:31 2014 +0000 @@ -13,7 +13,6 @@ signature NOMINAL_FUNCTION_MUTUAL = sig - val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config -> string (* defname *) -> ((string * typ) * mixfix) list @@ -22,10 +21,8 @@ -> ((thm (* goalstate *) * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *) ) * local_theory) - end - structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL = struct @@ -95,8 +92,8 @@ val dresultTs = distinct (op =) resultTs val n' = length dresultTs - val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs - val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs + val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs + val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs val fsum_type = ST --> RST @@ -108,7 +105,7 @@ val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 - val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) + val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) val rew = (n, fold_rev lambda vars f_exp) @@ -124,8 +121,8 @@ val rhs' = rhs |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t) in - (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), - Envir.beta_norm (SumTree.mk_inj RST n' i' rhs')) + (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), + Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs')) end val qglrs = map convert_eqs fqgars @@ -205,8 +202,8 @@ |> export end -val inl_perm = @{lemma "x = Inl y ==> Sum_Type.Projl (permute p x) = permute p (Sum_Type.Projl x)" by simp} -val inr_perm = @{lemma "x = Inr y ==> Sum_Type.Projr (permute p x) = permute p (Sum_Type.Projr x)" by simp} +val inl_perm = @{lemma "x = Inl y ==> projl (permute p x) = permute p (projl x)" by simp} +val inr_perm = @{lemma "x = Inr y ==> projr (permute p x) = permute p (projr x)" by simp} fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, _) import (export : thm -> thm) sum_psimp_eq = @@ -224,13 +221,12 @@ val ([p], ctxt'') = ctxt' |> fold Variable.declare_term args - |> Variable.variant_fixes ["p"] + |> Variable.variant_fixes ["p"] val p = Free (p, @{typ perm}) val simpset = put_simpset HOL_basic_ss ctxt'' addsimps - @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @ - @{thms Projr.simps Projl.simps} @ + @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric] sum.sel} @ [(cond MRS eqvt_thm) RS @{thm sym}] @ [inl_perm, inr_perm, simp] val goal_lhs = mk_perm p (list_comb (f, args)) @@ -272,21 +268,21 @@ end val Ps = map2 mk_P parts newPs - val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps + val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps val induct_inst = Thm.forall_elim (cert case_exp) induct - |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) + |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs) fun project rule (MutualPart {cargTs, i, ...}) k = let val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) - val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) + val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) in (rule |> Thm.forall_elim (cert inj) - |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) + |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |> fold_rev (Thm.forall_intr o cert) (afs @ newPs), k + length cargTs) end @@ -427,13 +423,13 @@ let val (tys, ty) = strip_type T val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty) - val inj_fun = absdummy dummyT (SumTree.mk_inj RST n' i' (Bound 0)) + val inj_fun = absdummy dummyT (Sum_Tree.mk_inj RST n' i' (Bound 0)) in Syntax.check_term lthy'' (mk_comp_dummy inj_fun fun_var) end - val sum_case_exp = map mk_cases parts - |> SumTree.mk_sumcases RST + val case_sum_exp = map mk_cases parts + |> Sum_Tree.mk_sumcases RST val (G_name, G_type) = dest_Free G val G_name_aux = G_name ^ "_aux" @@ -441,7 +437,7 @@ val GIntros_aux = GIntro_thms |> map prop_of |> map (Term.subst_free subst) - |> map (subst_all sum_case_exp) + |> map (subst_all case_sum_exp) val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' @@ -456,10 +452,10 @@ fun mk_inj_goal (MutualPart {i', ...}) = let - val injs = SumTree.mk_inj ST n' i' (Bound 0) + val injs = Sum_Tree.mk_inj ST n' i' (Bound 0) val projs = y - |> SumTree.mk_proj RST n' i' - |> SumTree.mk_inj RST n' i' + |> Sum_Tree.mk_proj RST n' i' + |> Sum_Tree.mk_inj RST n' i' in Const (@{const_name "All"}, dummyT) $ absdummy dummyT (HOLogic.mk_imp (HOLogic.mk_eq(x, injs), HOLogic.mk_eq(projs, y))) @@ -474,7 +470,7 @@ val goal_iff2 = Logic.mk_implies (G_prem, G_aux_prem) |> all x |> all y - val simp_thms = @{thms Projl.simps Projr.simps sum.inject sum.cases sum.distinct o_apply} + val simp_thms = @{thms sum.sel sum.inject sum.case sum.distinct o_apply} val simpset0 = put_simpset HOL_basic_ss lthy''' addsimps simp_thms val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms