--- 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