--- a/src/HOL/Nominal/nominal_package.ML Fri Oct 13 18:15:18 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Fri Oct 13 18:18:58 2006 +0200
@@ -71,7 +71,7 @@
(term_frees t2) of
[Free (s, T)] => absfree (s, T, t2)
| _ => sys_error "indtac")
- | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
+ | SOME (_ $ t') => Abs ("x", fastype_of t', abstract_over (t', t2)))
val cert = cterm_of (Thm.sign_of_thm st);
val Ps = map (cert o head_of o snd o getP) ts;
val indrule' = cterm_instantiate (Ps ~~
@@ -145,6 +145,8 @@
val rev_simps = thms "rev.simps";
val app_simps = thms "op @.simps";
+val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
+
fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
let
(* this theory is used just for parsing *)
@@ -448,8 +450,8 @@
val _ = warning "representing sets";
- val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names
- (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
+ val rep_set_names = DatatypeProp.indexify_names
+ (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr);
val big_rep_name =
space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
(fn (i, ("Nominal.noption", _, _)) => NONE
@@ -488,34 +490,37 @@
in (j + 1, j' + length Ts,
case dt'' of
DtRec k => list_all (map (pair "x") Us,
- HOLogic.mk_Trueprop (HOLogic.mk_mem (free',
- Const (List.nth (rep_set_names, k),
- HOLogic.mk_setT T)))) :: prems
+ HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
+ T --> HOLogic.boolT) $ free')) :: prems
| _ => prems,
snd (foldr mk_abs_fun (j', free) Ts) :: ts)
end;
val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;
- val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
- (list_comb (Const (cname, map fastype_of ts ---> T), ts),
- Const (s, HOLogic.mk_setT T)))
+ val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
+ list_comb (Const (cname, map fastype_of ts ---> T), ts))
in Logic.list_implies (prems, concl)
end;
- val (intr_ts, ind_consts) =
- apfst List.concat (ListPair.unzip (List.mapPartial
+ val (intr_ts, (rep_set_names', recTs')) =
+ apfst List.concat (apsnd ListPair.unzip (ListPair.unzip (List.mapPartial
(fn ((_, ("Nominal.noption", _, _)), _) => NONE
| ((i, (_, _, constrs)), rep_set_name) =>
let val T = nth_dtyp i
in SOME (map (make_intr rep_set_name T) constrs,
- Const (rep_set_name, HOLogic.mk_setT T))
+ (rep_set_name, T))
end)
- (descr ~~ rep_set_names)));
+ (descr ~~ rep_set_names))));
+ val rep_set_names'' = map (Sign.full_name thy3) rep_set_names';
val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
setmp InductivePackage.quiet_mode false
- (InductivePackage.add_inductive_i false true big_rep_name false true false
- ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3;
+ (TheoryTarget.init NONE #>
+ InductivePackage.add_inductive_i false big_rep_name false true false
+ (map (fn (s, T) => (s, SOME (T --> HOLogic.boolT), NoSyn))
+ (rep_set_names' ~~ recTs'))
+ [] (map (fn x => (("", []), x)) intr_ts) [] #>
+ apfst (snd o LocalTheory.exit false)) thy3;
(**** Prove that representing set is closed under permutation ****)
@@ -528,16 +533,16 @@
fun mk_perm_closed name = map (fn th => standard (th RS mp))
(List.take (split_conj_thm (Goal.prove_global thy4 [] []
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
- (fn (S, x) =>
+ (fn ((s, T), x) =>
let
- val S = map_types (map_type_tfree
- (fn (s, cs) => TFree (s, cs union cp_classes))) S;
- val T = HOLogic.dest_setT (fastype_of S);
+ val T = map_type_tfree
+ (fn (s, cs) => TFree (s, cs union cp_classes)) T;
+ val S = Const (s, T --> HOLogic.boolT);
val permT = mk_permT (Type (name, []))
- in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
- HOLogic.mk_mem (Const ("Nominal.perm", permT --> T --> T) $
- Free ("pi", permT) $ Free (x, T), S))
- end) (ind_consts ~~ perm_indnames'))))
+ in HOLogic.mk_imp (S $ Free (x, T),
+ S $ (Const ("Nominal.perm", permT --> T --> T) $
+ Free ("pi", permT) $ Free (x, T)))
+ end) (rep_set_names'' ~~ recTs' ~~ perm_indnames'))))
(fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
[indtac rep_induct [] 1,
ALLGOALS (simp_tac (simpset_of thy4 addsimps
@@ -556,10 +561,12 @@
val (typedefs, thy6) =
thy5
- |> fold_map (fn ((((name, mx), tvs), c), name') => fn thy =>
+ |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
setmp TypedefPackage.quiet_mode true
- (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
- (rtac exI 1 THEN
+ (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx)
+ (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
+ Const (cname, U --> HOLogic.boolT)) NONE
+ (rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac rep_intrs 1))) thy |> (fn ((_, r), thy) =>
let
@@ -567,7 +574,6 @@
val pi = Free ("pi", permT);
val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
val T = Type (Sign.intern_type thy name, tvs');
- val Const (_, Type (_, [U])) = c
in apfst (pair r o hd)
(PureThy.add_defs_unchecked_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
(Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
@@ -577,12 +583,13 @@
Free ("x", T))))), [])] thy)
end))
(types_syntax ~~ tyvars ~~
- (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
+ List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~
+ new_type_names);
val perm_defs = map snd typedefs;
- val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
+ val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs;
val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
- val Rep_thms = map (#Rep o fst) typedefs;
+ val Rep_thms = map (collect_simp o #Rep o fst) typedefs;
val big_name = space_implode "_" new_type_names;
@@ -592,7 +599,7 @@
val _ = warning "prove that new types are in class pt_<name> ...";
fun pt_instance ((class, atom), perm_closed_thms) =
- fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
+ fold (fn ((((((Abs_inverse, Rep_inverse), Rep),
perm_def), name), tvs), perm_closed) => fn thy =>
AxClass.prove_arity
(Sign.intern_type thy name,
@@ -604,7 +611,8 @@
[Rep RS perm_closed RS Abs_inverse]) 1,
asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
(Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy)
- (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms);
+ (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
+ new_type_names ~~ tyvars ~~ perm_closed_thms);
(** prove that new types are in class cp_<name1>_<name2> **)
@@ -616,7 +624,7 @@
val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
val class = Sign.intern_class thy name;
val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
- in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
+ in fold (fn ((((((Abs_inverse, Rep),
perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
AxClass.prove_arity
(Sign.intern_type thy name,
@@ -630,8 +638,8 @@
cong_tac 1,
rtac refl 1,
rtac cp1' 1]) thy)
- (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~
- perm_closed_thms2) thy
+ (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
+ tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy
end;
val thy7 = fold (fn x => fn thy => thy |>
@@ -697,9 +705,6 @@
val abs_names = map (fn s =>
Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
- val recTs' = List.mapPartial
- (fn ((_, ("Nominal.noption", _, _)), T) => NONE
- | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
val recTs = get_rec_types descr'' sorts';
val newTs' = Library.take (length new_type_names, recTs');
val newTs = Library.take (length new_type_names, recTs);
@@ -758,30 +763,21 @@
List.take (pdescr, length new_type_names) ~~
new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
- val abs_inject_thms = map (fn tname =>
- PureThy.get_thm thy8 (Name ("Abs_" ^ tname ^ "_inject"))) new_type_names;
-
- val rep_inject_thms = map (fn tname =>
- PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inject"))) new_type_names;
-
- val rep_thms = map (fn tname =>
- PureThy.get_thm thy8 (Name ("Rep_" ^ tname))) new_type_names;
-
- val rep_inverse_thms = map (fn tname =>
- PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inverse"))) new_type_names;
+ val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs
+ val rep_inject_thms = map (#Rep_inject o fst) typedefs
(* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *)
fun prove_constr_rep_thm eqn =
let
val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
- val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms
+ val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
rtac refl 3,
resolve_tac rep_intrs 2,
- REPEAT (resolve_tac rep_thms 1)])
+ REPEAT (resolve_tac Rep_thms 1)])
end;
val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
@@ -790,7 +786,7 @@
fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
let
- val _ $ (_ $ (Rep $ x) $ _) = Logic.unvarify (prop_of th);
+ val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th);
val Type ("fun", [T, U]) = fastype_of Rep;
val permT = mk_permT (Type (atom, []));
val pi = Free ("pi", permT);
@@ -979,8 +975,8 @@
val Abs_t = Const (List.nth (abs_names, i), U --> T)
- in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,
- Const (List.nth (rep_set_names, i), HOLogic.mk_setT U)) $
+ in (prems @ [HOLogic.imp $
+ (Const (List.nth (rep_set_names'', i), U --> HOLogic.boolT) $ Rep_t) $
(mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
end;
@@ -1359,17 +1355,20 @@
val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
- val rec_set_Ts = map (fn (T1, T2) => rec_fn_Ts ---> HOLogic.mk_setT
- (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);
+ val rec_set_Ts = map (fn (T1, T2) =>
+ rec_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
val big_rec_name = big_name ^ "_rec_set";
- val rec_set_names = map (Sign.full_name (Theory.sign_of thy10))
- (if length descr'' = 1 then [big_rec_name] else
- (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
- (1 upto (length descr''))));
+ val rec_set_names' =
+ if length descr'' = 1 then [big_rec_name] else
+ map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
+ (1 upto (length descr''));
+ val rec_set_names = map (Sign.full_name (Theory.sign_of thy10)) rec_set_names';
val rec_fns = map (uncurry (mk_Free "f"))
(rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
+ val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
+ (rec_set_names' ~~ rec_set_Ts);
val rec_sets = map (fn c => list_comb (Const c, rec_fns))
(rec_set_names ~~ rec_set_Ts);
@@ -1399,8 +1398,7 @@
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 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'');
+ (List.nth (rec_sets', i) $ Free x $ Free y)) (recs ~~ frees'');
val prems2 =
map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop
(Const ("Nominal.fresh", T --> fastype_of f --> HOLogic.boolT) $
@@ -1422,9 +1420,8 @@
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)))],
+ HOLogic.mk_Trueprop (rec_set $
+ list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
if null result_freshs then rec_prems'
else rec_prems' @ [list_all_free (frees @ frees'',
@@ -1437,12 +1434,16 @@
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)
- (InductivePackage.add_inductive_i false true big_rec_name false false false
- rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy10;
+ (TheoryTarget.init NONE #>
+ InductivePackage.add_inductive_i false big_rec_name false false false
+ (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+ (map (apsnd SOME o dest_Free) rec_fns)
+ (map (fn x => (("", []), x)) rec_intr_ts) [] #>
+ apfst (snd o LocalTheory.exit false)) thy10;
(** equivariance **)
@@ -1462,8 +1463,7 @@
val x = Free ("x" ^ string_of_int i, T);
val y = Free ("y" ^ string_of_int i, U)
in
- (HOLogic.mk_mem (HOLogic.mk_prod (x, y), R),
- HOLogic.mk_mem (HOLogic.mk_prod (mk_perm [] (pi, x), mk_perm [] (pi, y)), R'))
+ (R $ x $ y, R' $ mk_perm [] (pi, x) $ mk_perm [] (pi, y))
end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
val ths = map (fn th => standard (th RS mp)) (split_conj_thm
(Goal.prove_global thy11 [] []
@@ -1501,7 +1501,7 @@
val x = Free ("x" ^ string_of_int i, T);
val y = Free ("y" ^ string_of_int i, U)
in
- HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (x, y), R),
+ HOLogic.mk_imp (R $ x $ y,
HOLogic.mk_mem (Const ("Nominal.supp", U --> aset) $ y, finites))
end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))
(fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
@@ -1543,12 +1543,9 @@
val y' = Free ("y'", U)
in
standard (Goal.prove (Context.init_proof thy11) [] (finite_prems @
- [HOLogic.mk_Trueprop (HOLogic.mk_mem
- (HOLogic.mk_prod (x, y), R)),
+ [HOLogic.mk_Trueprop (R $ x $ y),
HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
- HOLogic.mk_imp (HOLogic.mk_mem
- (HOLogic.mk_prod (x, y'), R),
- HOLogic.mk_eq (y', y)))),
+ HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),
HOLogic.mk_Trueprop (Const ("Nominal.fresh",
aT --> T --> HOLogic.boolT) $ a $ x)] @
freshs)
@@ -1605,9 +1602,9 @@
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) =>
+ val rec_unique_concls = map (fn ((x, 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)))
+ Abs ("y", U, R $ Free x $ Bound 0))
(rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
val induct_aux_rec = Drule.cterm_instantiate
@@ -1656,8 +1653,8 @@
(Goal.prove context
(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)))
+ (map (fn (((x, y), S), P) => HOLogic.mk_imp
+ (S $ Free x $ Free y, P $ (Free y)))
(rec_unique_frees'' ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds))))
(fn _ =>
rtac rec_induct 1 THEN
@@ -1678,11 +1675,12 @@
(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,
+ (HOL_ss addsimps List.concat distinct_thms)) 1] @
+ (if null idxs then [] else [hyp_subst_tac 1,
SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
let
- val (_, prem) = split_last prems';
+ val SOME prem = find_first (can (HOLogic.dest_eq o
+ HOLogic.dest_Trueprop o prop_of)) prems';
val _ $ (_ $ lhs $ rhs) = prop_of prem;
val _ $ (_ $ lhs' $ rhs') = term_of concl;
val rT = fastype_of lhs';
@@ -1696,7 +1694,7 @@
chop (length params div 2) (map term_of params);
val params' = params1 @ params2;
val rec_prems = filter (fn th => case prop_of th of
- _ $ (Const ("op :", _) $ _ $ _) => true | _ => false) prems';
+ _ $ (S $ _ $ _) => S mem rec_sets | _ => false) prems';
val fresh_prems = filter (fn th => case prop_of th of
_ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
| _ $ (Const ("Not", _) $ _) => true
@@ -1777,7 +1775,7 @@
val _ = warning "step 6: (ts, pi1^-1 o pi2 o vs) in rec_set";
val rec_prems' = map (fn th =>
let
- val _ $ (_ $ (_ $ x $ y) $ S) = prop_of th;
+ val _ $ (S $ x $ y) = prop_of th;
val k = find_index (equal S) rec_sets;
val pi = rpi1 @ pi2;
fun mk_pi z = foldr (mk_perm []) z pi;
@@ -1791,8 +1789,7 @@
cterm_of thy11 p)]) th;
in rtac th' 1 end;
val th' = Goal.prove context'' [] []
- (HOLogic.mk_Trueprop (HOLogic.mk_mem
- (HOLogic.mk_prod (mk_pi x, mk_pi y), S)))
+ (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
(fn _ => EVERY
(map eqvt_tac pi @
[simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @
@@ -1829,9 +1826,9 @@
val (rec_freshs1, rec_freshs2) = ListPair.unzip (List.concat
(map (fn (((rec_prem, rec_prem'), eqn), ih) =>
let
- val _ $ (_ $ (_ $ x $ (y as Free (_, T))) $ S) =
+ val _ $ (S $ x $ (y as Free (_, T))) =
prop_of rec_prem;
- val _ $ (_ $ (_ $ _ $ y') $ _) = prop_of rec_prem';
+ val _ $ (_ $ _ $ y') = prop_of rec_prem';
val k = find_index (equal S) rec_sets;
val atoms = List.concat (List.mapPartial
(fn ((bs, z), (bs', _)) =>
@@ -1941,7 +1938,7 @@
|> (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))))))
+ set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
(* prove characteristic equations for primrec combinators *)
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 13 18:15:18 2006 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 13 18:18:58 2006 +0200
@@ -108,24 +108,27 @@
val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
val big_rec_name' = big_name ^ "_rec_set";
- val rec_set_names = map (Sign.full_name (Theory.sign_of thy0))
- (if length descr' = 1 then [big_rec_name'] else
- (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
- (1 upto (length descr'))));
+ val rec_set_names' =
+ if length descr' = 1 then [big_rec_name'] else
+ map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
+ (1 upto (length descr'));
+ val rec_set_names = map (Sign.full_name (Theory.sign_of thy0)) rec_set_names';
val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
- val rec_set_Ts = map (fn (T1, T2) => reccomb_fn_Ts ---> HOLogic.mk_setT
- (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);
+ val rec_set_Ts = map (fn (T1, T2) =>
+ reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
val rec_fns = map (uncurry (mk_Free "f"))
(reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
+ val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
+ (rec_set_names' ~~ rec_set_Ts);
val rec_sets = map (fn c => list_comb (Const c, rec_fns))
(rec_set_names ~~ rec_set_Ts);
(* introduction rules for graph of primrec function *)
- fun make_rec_intr T set_name ((rec_intr_ts, l), (cname, cargs)) =
+ fun make_rec_intr T rec_set ((rec_intr_ts, l), (cname, cargs)) =
let
fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
let val free1 = mk_Free "x" U j
@@ -135,9 +138,8 @@
val free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k;
val i = length Us
in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
- (map (pair "x") Us, HOLogic.mk_mem (HOLogic.mk_prod
- (app_bnds free1 i, app_bnds free2 i),
- List.nth (rec_sets, m)))) :: prems,
+ (map (pair "x") Us, List.nth (rec_sets', m) $
+ app_bnds free1 i $ app_bnds free2 i)) :: prems,
free1::t1s, free2::t2s)
end
| _ => (j + 1, k, prems, free1::t1s, t2s))
@@ -146,19 +148,23 @@
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
- in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
- (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
- list_comb (List.nth (rec_fns, l), t1s @ t2s)), set_name)))], l + 1)
+ in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
+ (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
+ list_comb (List.nth (rec_fns, l), t1s @ t2s)))], l + 1)
end;
val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
- (([], 0), descr' ~~ recTs ~~ rec_sets);
+ (([], 0), descr' ~~ recTs ~~ rec_sets');
val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
- (InductivePackage.add_inductive_i false true big_rec_name' false false true
- rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy0;
+ (TheoryTarget.init NONE #>
+ InductivePackage.add_inductive_i false big_rec_name' false false true
+ (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+ (map (apsnd SOME o dest_Free) rec_fns)
+ (map (fn x => (("", []), x)) rec_intr_ts) [] #>
+ apfst (snd o LocalTheory.exit false)) thy0;
(* prove uniqueness and termination of primrec combinators *)
@@ -166,7 +172,7 @@
fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
let
- val distinct_tac = (etac Pair_inject 1) THEN
+ val distinct_tac =
(if i < length newTs then
full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1
else full_simp_tac dist_ss 1);
@@ -185,7 +191,7 @@
REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
etac elim 1,
REPEAT_DETERM_N j distinct_tac,
- etac Pair_inject 1, TRY (dresolve_tac inject 1),
+ TRY (dresolve_tac inject 1),
REPEAT (etac conjE 1), hyp_subst_tac 1,
REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
TRY (hyp_subst_tac 1),
@@ -203,9 +209,8 @@
let
val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
- absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod
- (mk_Free "x" T1 i, Free ("y", T2)), set_t)))
- (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
+ absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
+ (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
val cert = cterm_of thy1
val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
@@ -241,7 +246,7 @@
|> (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))))))
+ set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
||> parent_path flat_names;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 13 18:15:18 2006 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 13 18:18:58 2006 +0200
@@ -27,6 +27,8 @@
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
+val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
+
(** theory context references **)
@@ -65,10 +67,11 @@
val big_name = space_implode "_" new_type_names;
val thy1 = add_path flat_names big_name thy;
val big_rec_name = big_name ^ "_rep_set";
- val rep_set_names = map (Sign.full_name (Theory.sign_of thy1))
+ val rep_set_names' =
(if length descr' = 1 then [big_rec_name] else
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
+ val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) rep_set_names';
val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
val leafTs' = get_nonrec_types descr' sorts;
@@ -85,6 +88,8 @@
else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
val UnivT = HOLogic.mk_setT Univ_elT;
+ val UnivT' = Univ_elT --> HOLogic.boolT;
+ val Collect = Const ("Collect", UnivT' --> UnivT);
val In0 = Const (In0_name, Univ_elT --> Univ_elT);
val In1 = Const (In1_name, Univ_elT --> Univ_elT);
@@ -149,8 +154,8 @@
val free_t =
app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
in (j + 1, list_all (map (pair "x") Ts,
- HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
- Const (List.nth (rep_set_names, k), UnivT)))) :: prems,
+ HOLogic.mk_Trueprop
+ (Free (List.nth (rep_set_names', k), UnivT') $ free_t)) :: prems,
mk_lim free_t Ts :: ts)
end
| _ =>
@@ -159,32 +164,37 @@
end);
val (_, prems, ts) = foldr mk_prem (1, [], []) cargs;
- val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
- (mk_univ_inj ts n i, Const (s, UnivT)))
+ val concl = HOLogic.mk_Trueprop
+ (Free (s, UnivT') $ mk_univ_inj ts n i)
in Logic.list_implies (prems, concl)
end;
- val consts = map (fn s => Const (s, UnivT)) rep_set_names;
-
val intr_ts = List.concat (map (fn ((_, (_, _, constrs)), rep_set_name) =>
map (make_intr rep_set_name (length constrs))
- ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
+ ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'));
val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
- (InductivePackage.add_inductive_i false true big_rec_name false true false
- consts (map (fn x => (("", x), [])) intr_ts) []) thy1;
+ (TheoryTarget.init NONE #>
+ InductivePackage.add_inductive_i false big_rec_name false true false
+ (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
+ (map (fn x => (("", []), x)) intr_ts) [] #>
+ apfst (snd o LocalTheory.exit false)) thy1;
(********************************* typedef ********************************)
- val thy3 = add_path flat_names big_name (Library.foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
- setmp TypedefPackage.quiet_mode true
- (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
- (rtac exI 1 THEN
- QUIET_BREADTH_FIRST (has_fewer_prems 1)
- (resolve_tac rep_intrs 1))) thy |> snd)
- (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
- (Library.take (length newTs, consts)) ~~ new_type_names));
+ val (typedefs, thy3) = thy2 |>
+ parent_path flat_names |>
+ fold_map (fn ((((name, mx), tvs), c), name') =>
+ setmp TypedefPackage.quiet_mode true
+ (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx)
+ (Collect $ Const (c, UnivT')) NONE
+ (rtac exI 1 THEN rtac CollectI 1 THEN
+ QUIET_BREADTH_FIRST (has_fewer_prems 1)
+ (resolve_tac rep_intrs 1))))
+ (types_syntax ~~ tyvars ~~
+ (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
+ add_path flat_names big_name;
(*********************** definition of constructors ***********************)
@@ -257,47 +267,12 @@
val _ = message "Proving isomorphism properties ...";
- (* get axioms from theory *)
-
- val newT_iso_axms = map (fn s =>
- (get_thm thy4 (Name ("Abs_" ^ s ^ "_inverse")),
- get_thm thy4 (Name ("Rep_" ^ s ^ "_inverse")),
- get_thm thy4 (Name ("Rep_" ^ s)))) new_type_names;
-
- (*------------------------------------------------*)
- (* prove additional theorems: *)
- (* inj_on dt_Abs_i rep_set_i and inj dt_Rep_i *)
- (*------------------------------------------------*)
-
- fun prove_newT_iso_inj_thm (((s, (thm1, thm2, _)), T), rep_set_name) =
- let
- val sg = Theory.sign_of thy4;
- val RepT = T --> Univ_elT;
- val Rep_name = Sign.intern_const sg ("Rep_" ^ s);
- val AbsT = Univ_elT --> T;
- val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
+ val newT_iso_axms = map (fn (_, td) =>
+ (collect_simp (#Abs_inverse td), #Rep_inverse td,
+ collect_simp (#Rep td))) typedefs;
- val inj_Abs_thm =
- Goal.prove_global sg [] []
- (HOLogic.mk_Trueprop
- (Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
- Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))
- (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1]);
-
- val setT = HOLogic.mk_setT T
-
- val inj_Rep_thm =
- Goal.prove_global sg [] []
- (HOLogic.mk_Trueprop
- (Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
- Const (Rep_name, RepT) $ Const ("UNIV", setT)))
- (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]);
-
- in (inj_Abs_thm, inj_Rep_thm) end;
-
- val newT_iso_inj_thms = map prove_newT_iso_inj_thm
- (new_type_names ~~ newT_iso_axms ~~ newTs ~~
- Library.take (length newTs, rep_set_names));
+ val newT_iso_inj_thms = map (fn (_, td) =>
+ (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs;
(********* isomorphisms between existing types and "unfolded" types *******)
@@ -385,7 +360,7 @@
fun mk_funs_inv thm =
let
val {sign, prop, ...} = rep_thm thm;
- val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
+ val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
val used = add_term_tfree_names (a, []);
@@ -396,7 +371,7 @@
val f = Free ("f", Ts ---> U)
in Goal.prove_global sign [] [] (Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
- (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
+ (map (pair "x") Ts, S $ app_bnds f i)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
r $ (a $ app_bnds f i)), f))))
(fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])
@@ -418,14 +393,14 @@
in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
- HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT)))
+ Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i))
end;
val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
val rewrites = map mk_meta_eq iso_char_thms;
- val inj_thms' = map (fn r => r RS injD)
- (map snd newT_iso_inj_thms @ inj_thms);
+ val inj_thms' = map snd newT_iso_inj_thms @
+ map (fn r => r RS injD) inj_thms;
val inj_thm = Goal.prove_global thy5 [] []
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
@@ -465,14 +440,15 @@
val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
([], map #3 newT_iso_axms) (tl descr);
- val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded;
+ val iso_inj_thms = map snd newT_iso_inj_thms @
+ map (fn r => r RS injD) iso_inj_thms_unfolded;
- (* prove x : dt_rep_set_i --> x : range dt_Rep_i *)
+ (* prove dt_rep_set_i x --> x : range dt_Rep_i *)
fun mk_iso_t (((set_name, iso_name), i), T) =
let val isoT = T --> Univ_elT
in HOLogic.imp $
- HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $
+ (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
(if i < length newTs then Const ("True", HOLogic.boolT)
else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
@@ -517,12 +493,12 @@
fun prove_constr_rep_thm eqn =
let
- val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
+ val inj_thms = map fst newT_iso_inj_thms;
val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
- rtac refl 1,
+ rtac refl 3,
resolve_tac rep_intrs 2,
REPEAT (resolve_tac iso_elem_thms 1)])
end;
@@ -559,7 +535,7 @@
fun prove_constr_inj_thm rep_thms t =
let val inj_thms = Scons_inject :: (map make_elim
- ((map (fn r => r RS injD) iso_inj_thms) @
+ (iso_inj_thms @
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
Lim_inject, Suml_inject, Sumr_inject]))
in Goal.prove_global thy5 [] [] t (fn _ => EVERY
@@ -601,8 +577,8 @@
else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
Const (List.nth (all_rep_names, i), T --> Univ_elT)
- in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,
- Const (List.nth (rep_set_names, i), UnivT)) $
+ in (prems @ [HOLogic.imp $
+ (Const (List.nth (rep_set_names, i), UnivT') $ Rep_t) $
(mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
end;