# HG changeset patch # User berghofe # Date 1155913403 -7200 # Node ID 24329362022583ab1846905c720a232902e62250 # Parent 4d0c337193487fb111895cda5705166245cf8419 - Fixed bug that caused uniqueness proof for recursion combinator to fail for mutually recursive datatypes - Implemented proofs of characteristic equations for recursion combinator. diff -r 4d0c33719348 -r 243293620225 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Thu Aug 17 20:31:36 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Fri Aug 18 17:03:23 2006 +0200 @@ -1336,8 +1336,7 @@ Theory.add_path big_name |> PureThy.add_thms [(("induct'", induct_aux), [])] ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])] ||>> - PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])] ||> - Theory.parent_path; + PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])]; (**** recursion combinator ****) @@ -1386,8 +1385,8 @@ rs) ys) @ mk_fresh3 rs yss; - fun make_rec_intr T p rec_set - ((rec_intr_ts, rec_prems, rec_prems', l), ((cname, cargs), idxs)) = + fun make_rec_intr T p rec_set ((rec_intr_ts, rec_prems, rec_prems', + rec_eq_prems, l), ((cname, cargs), idxs)) = let val Ts = map (typ_of_dtyp descr'' sorts') cargs; val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts; @@ -1425,13 +1424,14 @@ else rec_prems' @ [list_all_free (frees @ frees'', Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ [P], HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj result_freshs)))], + rec_eq_prems @ [List.concat prems2 @ prems3], l + 1) end; - val (rec_intr_ts, rec_prems, rec_prems', _) = + val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) = Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) => Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d')) - (([], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets); + (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets); val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) = setmp InductivePackage.quiet_mode (!quiet_mode) @@ -1596,6 +1596,7 @@ val fun_tupleT = fastype_of fun_tuple; val rec_unique_frees = DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs; + val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees; val rec_unique_frees' = DatatypeProp.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts; val rec_unique_concls = map (fn ((x as (_, T), U), R) => @@ -1635,8 +1636,8 @@ [ex] ctxt in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end; - val rec_unique = map standard (split_conj_thm (Goal.prove - (Context.init_proof thy11) [] + val rec_unique_thms = split_conj_thm (Goal.prove + (Context.init_proof thy11) (map fst rec_unique_frees) (List.concat finite_premss @ rec_prems @ rec_prems') (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)) (fn {prems, context} => @@ -1647,11 +1648,11 @@ val (P_ind_ths, ths2) = chop k ths1; val P_ths = map (fn th => th RS mp) (split_conj_thm (Goal.prove context - (map fst (rec_unique_frees @ rec_unique_frees')) [] + (map fst (rec_unique_frees'' @ rec_unique_frees')) [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (((x, y), S), P) => HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (Free x, Free y), S), P $ (Free y))) - (rec_unique_frees ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds)))) + (rec_unique_frees'' ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds)))) (fn _ => rtac rec_induct 1 THEN REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1)))); @@ -1661,20 +1662,19 @@ val fcbs = List.concat (map split_conj_thm ths2); in EVERY ([rtac induct_aux_rec 1] @ - List.concat (map (fn (_, finite_ths) => + maps (fn (_, finite_ths) => [cut_facts_tac finite_ths 1, - asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) finite_thss) @ - [ALLGOALS (EVERY' - [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]), - REPEAT_DETERM o eresolve_tac [conjE, ex1E], - rtac ex1I, - resolve_tac rec_intrs THEN_ALL_NEW atac, - rotate_tac ~1, - (DETERM o eresolve_tac rec_elims) THEN_ALL_NEW full_simp_tac - (HOL_ss addsimps (Pair_eq :: List.concat distinct_thms)), - TRY o (etac conjE THEN' hyp_subst_tac)])] @ - map (fn idxs => SUBPROOF - (fn {asms, concl, prems = prems', params, context = context', ...} => + asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) finite_thss @ + maps (fn ((_, idxss), elim) => maps (fn idxs => + [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1, + REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1), + rtac ex1I 1, + (resolve_tac rec_intrs THEN_ALL_NEW atac) 1, + rotate_tac ~1 1, + ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac + (HOL_ss addsimps (Pair_eq :: List.concat distinct_thms))) 1] @ + (if null idxs then [] else [etac conjE 1, hyp_subst_tac 1, + SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} => let val (_, prem) = split_last prems'; val _ $ (_ $ lhs $ rhs) = prop_of prem; @@ -1909,22 +1909,70 @@ val _ = warning "finished!" in resolve_tac final' 1 - end) context 1) (filter_out null (List.concat (map snd ndescr)))) - end))); + end) context 1])) idxss) (ndescr ~~ rec_elims)) + end)); + + val rec_total_thms = map (fn r => r RS theI') rec_unique_thms; + + (* define primrec combinators *) + + val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec"; + val reccomb_names = map (Sign.full_name thy11) + (if length descr'' = 1 then [big_reccomb_name] else + (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int) + (1 upto (length descr'')))); + val reccombs = map (fn ((name, T), T') => list_comb + (Const (name, rec_fn_Ts @ [T] ---> T'), rec_fns)) + (reccomb_names ~~ recTs ~~ rec_result_Ts); + + val (reccomb_defs, thy12) = + thy11 + |> Theory.add_consts_i (map (fn ((name, T), T') => + (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn)) + (reccomb_names ~~ recTs ~~ rec_result_Ts)) + |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => + ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, + Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', + HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))) + (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)); + + (* prove characteristic equations for primrec combinators *) + + val rec_thms = map (fn (prems, concl) => + let + val _ $ (_ $ (_ $ x) $ _) = concl; + val (_, cargs) = strip_comb x; + val ps = map (fn (x as Free (_, T), i) => + (Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs)); + val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl; + val prems' = List.concat finite_premss @ rec_prems @ rec_prems' @ + map (subst_atomic ps) prems; + fun solve rules prems = resolve_tac rules THEN_ALL_NEW + (resolve_tac prems THEN_ALL_NEW atac) + in + Goal.prove_global thy12 [] prems' concl' + (fn prems => EVERY + [rewrite_goals_tac reccomb_defs, + rtac the1_equality 1, + solve rec_unique_thms prems 1, + resolve_tac rec_intrs 1, + REPEAT (solve (prems @ rec_total_thms) prems 1)]) + end) (rec_eq_prems ~~ + DatatypeProp.make_primrecs new_type_names descr' sorts' thy12); (* FIXME: theorems are stored in database for testing only *) - val (_, thy12) = thy11 |> - Theory.add_path big_name |> + val (_, thy13) = thy12 |> PureThy.add_thmss [(("rec_equiv", List.concat rec_equiv_thms), []), (("rec_equiv'", List.concat rec_equiv_thms'), []), (("rec_fin_supp", List.concat rec_fin_supp_thms), []), (("rec_fresh", List.concat rec_fresh_thms), []), - (("rec_unique", rec_unique), [])] ||> + (("rec_unique", map standard rec_unique_thms), []), + (("recs", rec_thms), [])] ||> Theory.parent_path; in - thy12 + thy13 end; val add_nominal_datatype = gen_add_nominal_datatype read_typ true;