# HG changeset patch # User berghofe # Date 1131384774 -3600 # Node ID ee6b4d3af498f704beb7f0381f89ac34bce464f4 # Parent 836135c8acb27efc0af3cb0a8a42538532e40a57 Added strong induction theorem (currently only axiomatized!). diff -r 836135c8acb2 -r ee6b4d3af498 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Mon Nov 07 15:19:03 2005 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Mon Nov 07 18:32:54 2005 +0100 @@ -136,8 +136,10 @@ val SOME {descr, ...} = Symtab.lookup (DatatypePackage.get_datatypes thy1) (hd full_new_type_names'); - val typ_of_dtyp = typ_of_dtyp descr sorts'; - fun nth_dtyp i = typ_of_dtyp (DtRec i); + fun nth_dtyp i = typ_of_dtyp descr sorts' (DtRec i); + + val dt_atomTs = filter (fn Type (s, []) => s mem atoms | _ => false) + (get_nonrec_types descr sorts); (**** define permutation functions ****) @@ -156,7 +158,7 @@ let val T = nth_dtyp i in map (fn (cname, dts) => let - val Ts = map typ_of_dtyp dts; + val Ts = map (typ_of_dtyp descr sorts') dts; val names = DatatypeProp.make_tnames Ts; val args = map Free (names ~~ Ts); val c = Const (cname, Ts ---> T); @@ -404,9 +406,9 @@ let val (dts, dt') = strip_option dt; val (dts', dt'') = strip_dtyp dt'; - val Ts = map typ_of_dtyp dts; - val Us = map typ_of_dtyp dts'; - val T = typ_of_dtyp dt''; + val Ts = map (typ_of_dtyp descr sorts') dts; + val Us = map (typ_of_dtyp descr sorts') dts'; + val T = typ_of_dtyp descr sorts' dt''; val free = mk_Free "x" (Us ---> T) j; val free' = app_bnds free (length Us); fun mk_abs_fun (T, (i, t)) = @@ -594,20 +596,25 @@ let val xs = NameSpace.unpack s; in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end; - val descr'' = List.mapPartial + val (descr'', ndescr) = ListPair.unzip (List.mapPartial (fn (i, ("nominal.nOption", _, _)) => NONE - | (i, (s, dts, constrs)) => SOME (the (AList.lookup op = ty_idxs i), - (strip_nth_name 1 s, map reindex dts, - map (fn (cname, cargs) => - (strip_nth_name 2 cname, - foldl (fn (dt, dts) => - let val (dts', dt') = strip_option dt - in (dts @ dts' @ [reindex dt']) end) [] cargs)) constrs))) descr; + | (i, (s, dts, constrs)) => + 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)) + (foldl_map (fn (dts, dt) => + let val (dts', dt') = strip_option dt + in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end) + ([], cargs))) constrs) + in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)), + (index, constrs2)) + end) descr); val (descr1, descr2) = splitAt (length new_type_names, descr''); val descr' = [descr1, descr2]; - val typ_of_dtyp' = replace_types' o typ_of_dtyp; + val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts'; val rep_names = map (fn s => Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names; @@ -617,7 +624,7 @@ val recTs' = List.mapPartial (fn ((_, ("nominal.nOption", _, _)), T) => NONE | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts'); - val recTs = get_rec_types (List.concat descr') sorts'; + val recTs = get_rec_types descr'' sorts'; val newTs' = Library.take (length new_type_names, recTs'); val newTs = Library.take (length new_type_names, recTs); @@ -640,7 +647,7 @@ foldr mk_abs_fun (list_abs (map (pair "z" o typ_of_dtyp') dts', Const (List.nth (rep_names, k), typ_of_dtyp' dt'' --> - typ_of_dtyp dt'') $ app_bnds x (length dts'))) + typ_of_dtyp descr sorts' dt'') $ app_bnds x (length dts'))) xs :: r_args) else error "nested recursion not (yet) supported" | _ => (j + 1, x' :: l_args, x' :: r_args) @@ -916,9 +923,9 @@ end) atoms) constrs) end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps'))); - (**** Induction theorem ****) + (**** weak induction theorem ****) - val arities = get_arities (List.concat descr'); + val arities = get_arities descr''; fun mk_funs_inv thm = let @@ -955,7 +962,7 @@ end; val (indrule_lemma_prems, indrule_lemma_concls) = - Library.foldl mk_indrule_lemma (([], []), (List.concat descr' ~~ recTs ~~ recTs')); + Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs')); val indrule_lemma = standard (Goal.prove thy8 [] [] (Logic.mk_implies @@ -986,7 +993,7 @@ DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) (prems ~~ constr_defs))])); - val case_names_induct = mk_case_names_induct (List.concat descr'); + val case_names_induct = mk_case_names_induct descr''; (**** prove that new datatypes have finite support ****) @@ -1011,6 +1018,56 @@ length new_type_names)) end) atoms; + (**** strong induction theorem ****) + + val pnames = if length descr'' = 1 then ["P"] + else map (fn i => "P" ^ string_of_int i) (1 upto length descr''); + val ind_sort = map (fn T => Sign.intern_class thy8 ("fs_" ^ + Sign.base_name (fst (dest_Type T)))) dt_atomTs; + val fsT = TFree ("'n", ind_sort); + + fun make_pred i T = + Free (List.nth (pnames, i), T --> fsT --> HOLogic.boolT); + + fun make_ind_prem k T ((cname, cargs), idxs) = + let + val recs = List.filter is_rec_type cargs; + val Ts = map (typ_of_dtyp descr'' sorts') cargs; + val recTs' = map (typ_of_dtyp descr'' sorts') recs; + val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames); + val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); + val frees = tnames ~~ Ts; + val z = (variant tnames "z", fsT); + + fun mk_prem ((dt, s), T) = + let + val (Us, U) = strip_type T; + val l = length Us + in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop + (make_pred (body_index dt) U $ app_bnds (Free (s, T)) l $ Bound l)) + end; + + val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); + val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop + (Const ("nominal.fresh", T --> fsT --> HOLogic.boolT) $ + Free p $ Free z)) + (map (curry List.nth frees) (List.concat (map (fn (m, n) => + m upto m + n - 1) idxs))) + + in list_all_free (z :: frees, Logic.list_implies (prems' @ prems, + HOLogic.mk_Trueprop (make_pred k T $ + list_comb (Const (cname, Ts ---> T), map Free frees) $ Free z))) + end; + + val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) => + map (make_ind_prem i T) (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs)); + val tnames = DatatypeProp.make_tnames recTs; + val z = (variant tnames "z", fsT); + val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") + (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T) $ Free z) + (descr'' ~~ recTs ~~ tnames))); + val induct = Logic.list_implies (ind_prems, ind_concl); + val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global]; val (thy9, _) = thy8 |> @@ -1029,7 +1086,10 @@ (fst (dest_Type T), replicate (length sorts) [class], [class]) (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy - end) (atoms ~~ finite_supp_thms); + end) (atoms ~~ finite_supp_thms) |>> + Theory.add_path big_name |>>> + PureThy.add_axioms_i [(("induct_test", induct), [case_names_induct])] |>> + Theory.parent_path; in thy9