# HG changeset patch # User berghofe # Date 1149867052 -7200 # Node ID 3a3f591c838dc744fcfc7dea73b9e81390468a18 # Parent 1a09f25410da0681c2ede6c08da754fb30c8f0cd - Changed naming scheme: names of "internal" constructors now have "_Rep" as suffix - no need to set unique_names to false any longer - Cleaned up a bit (removed occurrences of strip_option and replace_types') diff -r 1a09f25410da -r 3a3f591c838d src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri Jun 09 16:25:05 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Fri Jun 09 17:30:52 2006 +0200 @@ -181,12 +181,8 @@ Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts) | replace_types T = T; - fun replace_types' (Type (s, Ts)) = - Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts) - | replace_types' T = T; - val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn, - map (fn (cname, cargs, mx) => (cname, + map (fn (cname, cargs, mx) => (cname ^ "_Rep", map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts'; val new_type_names' = map (fn n => n ^ "_Rep") new_type_names; @@ -665,7 +661,7 @@ let val SOME index = AList.lookup op = ty_idxs i; val (constrs1, constrs2) = ListPair.unzip - (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 cname)) + (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname))) (foldl_map (fn (dts, dt) => let val (dts', dt') = strip_option dt in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end) @@ -680,7 +676,11 @@ fun partition_cargs idxs xs = map (fn (i, j) => (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs; - val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts'; + val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts, + map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs)) + (constrs ~~ idxss)))) (descr'' ~~ ndescr); + + fun nth_dtyp' i = typ_of_dtyp descr'' sorts' (DtRec i); val rep_names = map (fn s => Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names; @@ -696,25 +696,22 @@ val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names; - fun make_constr_def tname T T' ((thy, defs, eqns), ((cname, cargs), (cname', mx))) = + fun make_constr_def tname T T' ((thy, defs, eqns), + (((cname_rep, _), (cname, cargs)), (cname', mx))) = let - fun constr_arg (dt, (j, l_args, r_args)) = + fun constr_arg ((dts, dt), (j, l_args, r_args)) = let - val x' = mk_Free "x" (typ_of_dtyp' dt) j; - val (dts, dt') = strip_option dt; - val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp' dt) i) + val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts' dt) i) (dts ~~ (j upto j + length dts - 1)) - val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts) - val (dts', dt'') = strip_dtyp dt' + val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts) in (j + length dts + 1, xs @ x :: l_args, foldr mk_abs_fun - (case dt'' of + (case dt of DtRec k => if k < length new_type_names then - list_abs (map (pair "z" o typ_of_dtyp') dts', - Const (List.nth (rep_names, k), typ_of_dtyp' dt'' --> - typ_of_dtyp descr sorts' dt'') $ app_bnds x (length dts')) + Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts' dt --> + typ_of_dtyp descr sorts' dt) $ x else error "nested recursion not (yet) supported" | _ => x) xs :: r_args) end @@ -723,9 +720,8 @@ val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname); val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname); val constrT = map fastype_of l_args ---> T; - val lhs = list_comb (Const (Sign.full_name thy (Sign.base_name cname), - constrT), l_args); - val rhs = list_comb (Const (cname, map fastype_of r_args ---> T'), r_args); + val lhs = list_comb (Const (cname, constrT), l_args); + val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args); val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs); val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> T') $ lhs, rhs)); @@ -735,20 +731,21 @@ (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)] in (thy', defs @ [def_thm], eqns @ [eqn]) end; - fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), - (((((_, (_, _, constrs)), tname), T), T'), constr_syntax)) = + fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)), + (_, (_, _, constrs'))), tname), T), T'), constr_syntax)) = let val rep_const = cterm_of thy (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T')); val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T') - ((Theory.add_path tname thy, defs, []), constrs ~~ constr_syntax) + ((Theory.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax) in (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) end; val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs ((thy7, [], [], []), List.take (descr, length new_type_names) ~~ + List.take (pdescr, length new_type_names) ~~ new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax); val abs_inject_thms = map (fn tname => @@ -824,7 +821,7 @@ val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *) val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) => - let val T = replace_types' (nth_dtyp i) + let val T = nth_dtyp' i in List.concat (map (fn (atom, perm_closed_thms) => map (fn ((cname, dts), constr_rep_thm) => let @@ -837,15 +834,12 @@ let val T = fastype_of t in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end; - fun constr_arg (dt, (j, l_args, r_args)) = + fun constr_arg ((dts, dt), (j, l_args, r_args)) = let - val x' = mk_Free "x" (typ_of_dtyp' dt) j; - val (dts, dt') = strip_option dt; - val Ts = map typ_of_dtyp' dts; + val Ts = map (typ_of_dtyp descr'' sorts') dts; val xs = map (fn (T, i) => mk_Free "x" T i) (Ts ~~ (j upto j + length dts - 1)) - val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts); - val (dts', dt'') = strip_dtyp dt'; + val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts) in (j + length dts + 1, xs @ x :: l_args, @@ -868,7 +862,7 @@ (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @ perm_closed_thms)) 1)])) end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss)) - end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); + end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); (** prove injectivity of constructors **) @@ -879,24 +873,20 @@ val supp_def = PureThy.get_thm thy8 (Name "supp_def"); val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) => - let val T = replace_types' (nth_dtyp i) + let val T = nth_dtyp' i in List.mapPartial (fn ((cname, dts), constr_rep_thm) => if null dts then NONE else SOME let val cname = Sign.intern_const thy8 (NameSpace.append tname (Sign.base_name cname)); - fun make_inj (dt, (j, args1, args2, eqs)) = + fun make_inj ((dts, dt), (j, args1, args2, eqs)) = let - val x' = mk_Free "x" (typ_of_dtyp' dt) j; - val y' = mk_Free "y" (typ_of_dtyp' dt) j; - val (dts, dt') = strip_option dt; - val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1); + val Ts_idx = map (typ_of_dtyp descr'' sorts') dts ~~ (j upto j + length dts - 1); val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx; - val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts); - val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts); - val (dts', dt'') = strip_dtyp dt'; + val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts); + val y = mk_Free "y" (typ_of_dtyp descr'' sorts' dt) (j + length dts) in (j + length dts + 1, xs @ (x :: args1), ys @ (y :: args2), @@ -920,7 +910,7 @@ TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def :: expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])) end) (constrs ~~ constr_rep_thms) - end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); + end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); (** equations for support and freshness **) @@ -931,21 +921,18 @@ val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') => - let val T = replace_types' (nth_dtyp i) + let val T = nth_dtyp' i in List.concat (map (fn (cname, dts) => map (fn atom => let val cname = Sign.intern_const thy8 (NameSpace.append tname (Sign.base_name cname)); val atomT = Type (atom, []); - fun process_constr (dt, (j, args1, args2)) = + fun process_constr ((dts, dt), (j, args1, args2)) = let - val x' = mk_Free "x" (typ_of_dtyp' dt) j; - val (dts, dt') = strip_option dt; - val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1); + val Ts_idx = map (typ_of_dtyp descr'' sorts') dts ~~ (j upto j + length dts - 1); val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; - val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts); - val (dts', dt'') = strip_dtyp dt'; + val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts) in (j + length dts + 1, xs @ (x :: args1), foldr mk_abs_fun x xs :: args2) @@ -978,33 +965,10 @@ (fn _ => simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1))) end) atoms) constrs) - end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps'))); + end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps'))); (**** weak induction theorem ****) - val arities = get_arities descr''; - - fun mk_funs_inv thm = - let - val {sign, prop, ...} = rep_thm thm; - val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $ - (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; - val used = add_term_tfree_names (a, []); - - fun mk_thm i = - let - val Ts = map (TFree o rpair HOLogic.typeS) - (variantlist (replicate i "'t", used)); - val f = Free ("f", Ts ---> U) - in standard (Goal.prove sign [] [] (Logic.mk_implies - (HOLogic.mk_Trueprop (HOLogic.list_all - (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))), - HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, - r $ (a $ app_bnds f i)), f)))) - (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])) - end - in map (fn r => r RS subst) (thm :: map mk_thm arities) end; - fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) = let val Rep_t = Const (List.nth (rep_names, i), T --> U) $ @@ -1036,7 +1000,7 @@ val indrule_lemma' = cterm_instantiate (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma; - val Abs_inverse_thms' = List.concat (map mk_funs_inv Abs_inverse_thms); + val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms; val dt_induct_prop = DatatypeProp.make_ind descr' sorts'; val dt_induct = standard (Goal.prove thy8 []