# HG changeset patch # User berghofe # Date 1153235422 -7200 # Node ID 922b4e7b8efdb7269620e1de32f6a7ef35b5889c # Parent 2517cd4b1f37bd5711c17fd2329b6ba9fc42d7c0 Started implementing uniqueness proof for recursion combinator (still unfinished). diff -r 2517cd4b1f37 -r 922b4e7b8efd src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Tue Jul 18 16:15:47 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Tue Jul 18 17:10:22 2006 +0200 @@ -1373,35 +1373,54 @@ (* introduction rules for graph of recursion function *) - fun make_rec_intr T rec_set ((rec_intr_ts, l), ((cname, cargs), idxs)) = + val rec_preds = map (fn (a, T) => + Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts); + + fun make_rec_intr T p rec_set + ((rec_intr_ts, rec_prems, rec_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; val frees' = partition_cargs idxs frees; val recs = List.mapPartial - (fn ((_, DtRec i), (_, x)) => SOME (i, x) | _ => NONE) + (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE) (partition_cargs idxs cargs ~~ frees'); val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~ map (fn (i, _) => List.nth (rec_result_Ts, i)) recs; - val prems = map (fn ((i, x), y) => HOLogic.mk_Trueprop + val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop (HOLogic.mk_mem (HOLogic.mk_prod (Free x, Free y), List.nth (rec_sets, i)))) (recs ~~ frees''); - val prems' = - List.concat (map (fn p as (_, T) => map (fn f => HOLogic.mk_Trueprop + val prems2 = + map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop (Const ("Nominal.fresh", T --> fastype_of f --> HOLogic.boolT) $ - Free p $ f)) rec_fns) (List.concat (map fst frees'))) @ + Free p $ f)) (List.concat (map fst frees'))) rec_fns; + val prems3 = mk_fresh1 [] (List.concat (map fst frees')) @ - mk_fresh2 [] frees' - in (rec_intr_ts @ [Logic.list_implies (prems' @ prems, - HOLogic.mk_Trueprop (HOLogic.mk_mem - (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), map Free frees), - list_comb (List.nth (rec_fns, l), map Free (frees @ frees''))), - rec_set)))], l + 1) + mk_fresh2 [] frees'; + val prems4 = map (fn ((i, _), y) => + HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees''); + val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees'')); + val rec_freshs = map (fn p as (_, T) => + Const ("Nominal.fresh", T --> fastype_of result --> HOLogic.boolT) $ + Free p $ result) (List.concat (map (fst o snd) recs)); + val P = HOLogic.mk_Trueprop (p $ result) + in + (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1, + HOLogic.mk_Trueprop (HOLogic.mk_mem + (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), map Free frees), + result), rec_set)))], + rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))], + if null rec_freshs then rec_prems' + else rec_prems' @ [list_all_free (frees @ frees'', + Logic.list_implies (List.nth (prems2, l) @ prems3 @ [P], + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_freshs)))], + l + 1) end; - val (rec_intr_ts, _) = Library.foldl (fn (x, (((d, d'), T), rec_set)) => - Library.foldl (make_rec_intr T rec_set) (x, #3 (snd d) ~~ snd d')) - (([], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_sets); + val (rec_intr_ts, rec_prems, rec_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); val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) = setmp InductivePackage.quiet_mode (!quiet_mode) @@ -1472,11 +1491,51 @@ (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1)))) end) dt_atomTs; + (** uniqueness **) + + val fresh_prems = List.concat (map (fn aT => + map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem + (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f, + Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) + (rec_fns ~~ rec_fn_Ts)) dt_atomTs); + + val fun_tuple = foldr1 HOLogic.mk_prod rec_fns; + val fun_tupleT = fastype_of fun_tuple; + val rec_unique_frees = + DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs; + val rec_unique_concls = map (fn ((x as (_, T), U), R) => + Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $ + Abs ("y", U, HOLogic.mk_mem (HOLogic.pair_const T U $ Free x $ Bound 0, R))) + (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets); + val induct_aux_rec = Drule.cterm_instantiate + (map (pairself (cterm_of thy11)) + (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT, + Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple))) + fresh_fs @ + map (fn (((P, T), (x, U)), Q) => + (Var ((P, 0), HOLogic.unitT --> Logic.varifyT T --> HOLogic.boolT), + Abs ("z", HOLogic.unitT, absfree (x, U, Q)))) + (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @ + map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T))) + rec_unique_frees)) induct_aux; + + val rec_unique = map standard (split_conj_thm (Goal.prove_global thy11 [] + (fresh_prems @ rec_prems @ rec_prems') + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)) + (fn ths => EVERY + [rtac induct_aux_rec 1, + print_tac "after application of induction theorem", + setmp quick_and_dirty true (SkipProof.cheat_tac thy11) (** FIXME !! **)]))); + (* FIXME: theorems are stored in database for testing only *) - val (_, 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), [])] thy11; + val (_, thy12) = thy11 |> + Theory.add_path big_name |> + 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_unique", rec_unique), [])] ||> + Theory.parent_path; in thy12