author berghofe Fri, 18 Aug 2006 17:03:23 +0200 changeset 20397 243293620225 parent 20396 4d0c33719348 child 20398 1db76dd407bb
- Fixed bug that caused uniqueness proof for recursion combinator to fail for mutually recursive datatypes - Implemented proofs of characteristic equations for recursion combinator.
```--- 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 @@
-      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 |>
+    val (_, thy13) = thy12 |>
[(("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;