src/HOL/Nominal/nominal_package.ML
changeset 20397 243293620225
parent 20376 53b31f7c1d87
child 20411 dd8a1cda2eaf
     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;