1.1 --- a/src/HOL/Nominal/nominal_package.ML Thu Aug 17 20:31:36 2006 +0200
1.2 +++ b/src/HOL/Nominal/nominal_package.ML Fri Aug 18 17:03:23 2006 +0200
1.3 @@ -1336,8 +1336,7 @@
1.4 Theory.add_path big_name |>
1.5 PureThy.add_thms [(("induct'", induct_aux), [])] ||>>
1.6 PureThy.add_thms [(("induct", induct), [case_names_induct])] ||>>
1.7 - PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])] ||>
1.8 - Theory.parent_path;
1.9 + PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])];
1.10
1.11 (**** recursion combinator ****)
1.12
1.13 @@ -1386,8 +1385,8 @@
1.14 rs) ys) @
1.15 mk_fresh3 rs yss;
1.16
1.17 - fun make_rec_intr T p rec_set
1.18 - ((rec_intr_ts, rec_prems, rec_prems', l), ((cname, cargs), idxs)) =
1.19 + fun make_rec_intr T p rec_set ((rec_intr_ts, rec_prems, rec_prems',
1.20 + rec_eq_prems, l), ((cname, cargs), idxs)) =
1.21 let
1.22 val Ts = map (typ_of_dtyp descr'' sorts') cargs;
1.23 val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
1.24 @@ -1425,13 +1424,14 @@
1.25 else rec_prems' @ [list_all_free (frees @ frees'',
1.26 Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ [P],
1.27 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj result_freshs)))],
1.28 + rec_eq_prems @ [List.concat prems2 @ prems3],
1.29 l + 1)
1.30 end;
1.31
1.32 - val (rec_intr_ts, rec_prems, rec_prems', _) =
1.33 + val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) =
1.34 Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) =>
1.35 Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d'))
1.36 - (([], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets);
1.37 + (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets);
1.38
1.39 val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) =
1.40 setmp InductivePackage.quiet_mode (!quiet_mode)
1.41 @@ -1596,6 +1596,7 @@
1.42 val fun_tupleT = fastype_of fun_tuple;
1.43 val rec_unique_frees =
1.44 DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs;
1.45 + val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
1.46 val rec_unique_frees' =
1.47 DatatypeProp.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
1.48 val rec_unique_concls = map (fn ((x as (_, T), U), R) =>
1.49 @@ -1635,8 +1636,8 @@
1.50 [ex] ctxt
1.51 in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
1.52
1.53 - val rec_unique = map standard (split_conj_thm (Goal.prove
1.54 - (Context.init_proof thy11) []
1.55 + val rec_unique_thms = split_conj_thm (Goal.prove
1.56 + (Context.init_proof thy11) (map fst rec_unique_frees)
1.57 (List.concat finite_premss @ rec_prems @ rec_prems')
1.58 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))
1.59 (fn {prems, context} =>
1.60 @@ -1647,11 +1648,11 @@
1.61 val (P_ind_ths, ths2) = chop k ths1;
1.62 val P_ths = map (fn th => th RS mp) (split_conj_thm
1.63 (Goal.prove context
1.64 - (map fst (rec_unique_frees @ rec_unique_frees')) []
1.65 + (map fst (rec_unique_frees'' @ rec_unique_frees')) []
1.66 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
1.67 (map (fn (((x, y), S), P) => HOLogic.mk_imp (HOLogic.mk_mem
1.68 (HOLogic.mk_prod (Free x, Free y), S), P $ (Free y)))
1.69 - (rec_unique_frees ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds))))
1.70 + (rec_unique_frees'' ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds))))
1.71 (fn _ =>
1.72 rtac rec_induct 1 THEN
1.73 REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
1.74 @@ -1661,20 +1662,19 @@
1.75 val fcbs = List.concat (map split_conj_thm ths2);
1.76 in EVERY
1.77 ([rtac induct_aux_rec 1] @
1.78 - List.concat (map (fn (_, finite_ths) =>
1.79 + maps (fn (_, finite_ths) =>
1.80 [cut_facts_tac finite_ths 1,
1.81 - asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) finite_thss) @
1.82 - [ALLGOALS (EVERY'
1.83 - [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]),
1.84 - REPEAT_DETERM o eresolve_tac [conjE, ex1E],
1.85 - rtac ex1I,
1.86 - resolve_tac rec_intrs THEN_ALL_NEW atac,
1.87 - rotate_tac ~1,
1.88 - (DETERM o eresolve_tac rec_elims) THEN_ALL_NEW full_simp_tac
1.89 - (HOL_ss addsimps (Pair_eq :: List.concat distinct_thms)),
1.90 - TRY o (etac conjE THEN' hyp_subst_tac)])] @
1.91 - map (fn idxs => SUBPROOF
1.92 - (fn {asms, concl, prems = prems', params, context = context', ...} =>
1.93 + asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) finite_thss @
1.94 + maps (fn ((_, idxss), elim) => maps (fn idxs =>
1.95 + [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
1.96 + REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
1.97 + rtac ex1I 1,
1.98 + (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
1.99 + rotate_tac ~1 1,
1.100 + ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
1.101 + (HOL_ss addsimps (Pair_eq :: List.concat distinct_thms))) 1] @
1.102 + (if null idxs then [] else [etac conjE 1, hyp_subst_tac 1,
1.103 + SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
1.104 let
1.105 val (_, prem) = split_last prems';
1.106 val _ $ (_ $ lhs $ rhs) = prop_of prem;
1.107 @@ -1909,22 +1909,70 @@
1.108 val _ = warning "finished!"
1.109 in
1.110 resolve_tac final' 1
1.111 - end) context 1) (filter_out null (List.concat (map snd ndescr))))
1.112 - end)));
1.113 + end) context 1])) idxss) (ndescr ~~ rec_elims))
1.114 + end));
1.115 +
1.116 + val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
1.117 +
1.118 + (* define primrec combinators *)
1.119 +
1.120 + val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
1.121 + val reccomb_names = map (Sign.full_name thy11)
1.122 + (if length descr'' = 1 then [big_reccomb_name] else
1.123 + (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
1.124 + (1 upto (length descr''))));
1.125 + val reccombs = map (fn ((name, T), T') => list_comb
1.126 + (Const (name, rec_fn_Ts @ [T] ---> T'), rec_fns))
1.127 + (reccomb_names ~~ recTs ~~ rec_result_Ts);
1.128 +
1.129 + val (reccomb_defs, thy12) =
1.130 + thy11
1.131 + |> Theory.add_consts_i (map (fn ((name, T), T') =>
1.132 + (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
1.133 + (reccomb_names ~~ recTs ~~ rec_result_Ts))
1.134 + |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
1.135 + ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
1.136 + Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
1.137 + HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
1.138 + (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
1.139 +
1.140 + (* prove characteristic equations for primrec combinators *)
1.141 +
1.142 + val rec_thms = map (fn (prems, concl) =>
1.143 + let
1.144 + val _ $ (_ $ (_ $ x) $ _) = concl;
1.145 + val (_, cargs) = strip_comb x;
1.146 + val ps = map (fn (x as Free (_, T), i) =>
1.147 + (Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs));
1.148 + val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl;
1.149 + val prems' = List.concat finite_premss @ rec_prems @ rec_prems' @
1.150 + map (subst_atomic ps) prems;
1.151 + fun solve rules prems = resolve_tac rules THEN_ALL_NEW
1.152 + (resolve_tac prems THEN_ALL_NEW atac)
1.153 + in
1.154 + Goal.prove_global thy12 [] prems' concl'
1.155 + (fn prems => EVERY
1.156 + [rewrite_goals_tac reccomb_defs,
1.157 + rtac the1_equality 1,
1.158 + solve rec_unique_thms prems 1,
1.159 + resolve_tac rec_intrs 1,
1.160 + REPEAT (solve (prems @ rec_total_thms) prems 1)])
1.161 + end) (rec_eq_prems ~~
1.162 + DatatypeProp.make_primrecs new_type_names descr' sorts' thy12);
1.163
1.164 (* FIXME: theorems are stored in database for testing only *)
1.165 - val (_, thy12) = thy11 |>
1.166 - Theory.add_path big_name |>
1.167 + val (_, thy13) = thy12 |>
1.168 PureThy.add_thmss
1.169 [(("rec_equiv", List.concat rec_equiv_thms), []),
1.170 (("rec_equiv'", List.concat rec_equiv_thms'), []),
1.171 (("rec_fin_supp", List.concat rec_fin_supp_thms), []),
1.172 (("rec_fresh", List.concat rec_fresh_thms), []),
1.173 - (("rec_unique", rec_unique), [])] ||>
1.174 + (("rec_unique", map standard rec_unique_thms), []),
1.175 + (("recs", rec_thms), [])] ||>
1.176 Theory.parent_path;
1.177
1.178 in
1.179 - thy12
1.180 + thy13
1.181 end;
1.182
1.183 val add_nominal_datatype = gen_add_nominal_datatype read_typ true;