# HG changeset patch # User Christian Urban # Date 1293802299 0 # Node ID d1d09177ec8985ce968a2f36fccae06902891790 # Parent e8732350a29f9e375c2b518599d075312186f5a9 added proper case names for all induct and exhaust theorems diff -r e8732350a29f -r d1d09177ec89 Nominal/Ex/Height.thy --- a/Nominal/Ex/Height.thy Fri Dec 31 12:12:59 2010 +0000 +++ b/Nominal/Ex/Height.thy Fri Dec 31 13:31:39 2010 +0000 @@ -14,7 +14,6 @@ | App "lam" "lam" | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100) -thm lam.strong_induct text {* Definition of the height-function on lambda-terms. *} @@ -84,17 +83,17 @@ theorem height_subst: shows "height (e[x::=e']) \ ((height e) - 1) + (height e')" proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) - case (1 y) + case (Var y) have "1 \ height e'" by (rule height_ge_one) then show "height (Var y[x::=e']) \ height (Var y) - 1 + height e'" by simp next - case (3 y e1) + case (Lam y e1) have ih: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" by fact moreover have vc: "atom y \ x" "atom y \ e'" by fact+ (* usual variable convention *) ultimately show "height ((Lam [y].e1)[x::=e']) \ height (Lam [y].e1) - 1 + height e'" by simp next - case (2 e1 e2) + case (App e1 e2) have ih1: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" and ih2: "height (e2[x::=e']) \ ((height e2) - 1) + (height e')" by fact+ then show "height ((App e1 e2)[x::=e']) \ height (App e1 e2) - 1 + height e'" by simp diff -r e8732350a29f -r d1d09177ec89 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Fri Dec 31 12:12:59 2010 +0000 +++ b/Nominal/Nominal2.thy Fri Dec 31 13:31:39 2010 +0000 @@ -131,12 +131,12 @@ val dt_full_names' = add_raws dt_full_names val dts_env = dt_full_names ~~ dt_full_names' - val cnstrs = get_cnstr_strs dts - val cnstrs_ty = get_typed_cnstrs dts - val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs - val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name - (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty - val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' + val cnstr_names = get_cnstr_strs dts + val cnstr_tys = get_typed_cnstrs dts + val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names + val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name + (Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys + val cnstrs_env = cnstr_full_names ~~ cnstr_full_names' val bn_fun_strs = get_bn_fun_strs bn_funs val bn_fun_strs' = add_raws bn_fun_strs @@ -153,7 +153,7 @@ val lthy1 = Named_Target.theory_init thy1 in - (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) + (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy1) end *} @@ -174,7 +174,7 @@ let (* definition of the raw datatypes *) val _ = warning "Definition of raw datatypes"; - val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = + val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = if get_STEPS lthy > 0 then define_raw_dts dts bn_funs bn_eqs bclauses lthy else raise TEST lthy @@ -540,7 +540,7 @@ val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms - val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses + val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses (* noting the theorems *) @@ -549,6 +549,7 @@ val thms_name = the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name fun thms_suffix s = Binding.qualified true s thms_name + val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) val (_, lthy9') = lthyC |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) @@ -559,11 +560,11 @@ ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) - ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) - ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) - ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) - ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms) - ||>> Local_Theory.note ((thms_suffix "strong_induct", []), qstrong_induct_thms) + ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) + ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts) + ||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts) + ||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms) + ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms) ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)