--- a/src/HOL/Tools/Datatype/datatype.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Nov 30 21:14:01 2011 +0100
@@ -65,7 +65,8 @@
val thy1 = Sign.add_path big_name thy;
val big_rec_name = big_name ^ "_rep_set";
val rep_set_names' =
- (if length descr' = 1 then [big_rec_name] else
+ (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_bname thy1) rep_set_names';
@@ -73,15 +74,19 @@
val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr);
val leafTs' = Datatype_Aux.get_nonrec_types descr' sorts;
val branchTs = Datatype_Aux.get_branching_types descr' sorts;
- val branchT = if null branchTs then HOLogic.unitT
+ val branchT =
+ if null branchTs then HOLogic.unitT
else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
val unneeded_vars =
- subtract (op =) (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
- val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
+ subtract (op =)
+ (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+ val leafTs =
+ leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val (newTs, oldTs) = chop (length (hd descr)) recTs;
- val sumT = if null leafTs then HOLogic.unitT
+ val sumT =
+ if null leafTs then HOLogic.unitT
else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs;
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
val UnivT = HOLogic.mk_setT Univ_elT;
@@ -98,17 +103,17 @@
fun mk_inj T' x =
let
fun mk_inj' T n i =
- if n = 1 then x else
- let val n2 = n div 2;
- val Type (_, [T1, T2]) = T
- in
- if i <= n2 then
- Const (@{const_name Inl}, T1 --> T) $ (mk_inj' T1 n2 i)
- else
- Const (@{const_name Inr}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
- end
- in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
- end;
+ if n = 1 then x
+ else
+ let
+ val n2 = n div 2;
+ val Type (_, [T1, T2]) = T;
+ in
+ if i <= n2
+ then Const (@{const_name Inl}, T1 --> T) $ (mk_inj' T1 n2 i)
+ else Const (@{const_name Inr}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
+ end;
+ in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs) end;
(* make injections for constructors *)
@@ -124,17 +129,17 @@
fun mk_fun_inj T' x =
let
fun mk_inj T n i =
- if n = 1 then x else
- let
- val n2 = n div 2;
- val Type (_, [T1, T2]) = T;
- fun mkT U = (U --> Univ_elT) --> T --> Univ_elT
- in
- if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
- else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
- end
- in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
- end;
+ if n = 1 then x
+ else
+ let
+ val n2 = n div 2;
+ val Type (_, [T1, T2]) = T;
+ fun mkT U = (U --> Univ_elT) --> T --> Univ_elT;
+ in
+ if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
+ else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
+ end;
+ in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs) end;
fun mk_lim t Ts = fold_rev (fn T => fn t => Lim $ mk_fun_inj T (Abs ("x", T, t))) Ts t;
@@ -153,21 +158,19 @@
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) dts;
val free_t =
Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
- in (j + 1, list_all (map (pair "x") Ts,
+ in
+ (j + 1, list_all (map (pair "x") Ts,
HOLogic.mk_Trueprop
(Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
mk_lim free_t Ts :: ts)
end
| _ =>
let val T = Datatype_Aux.typ_of_dtyp descr' sorts dt
- in (j + 1, prems, (Leaf $ mk_inj T (Datatype_Aux.mk_Free "x" T j))::ts)
- end);
+ in (j + 1, prems, (Leaf $ mk_inj T (Datatype_Aux.mk_Free "x" T j)) :: ts) end);
val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
- val concl = HOLogic.mk_Trueprop
- (Free (s, UnivT') $ mk_univ_inj ts n i)
- in Logic.list_implies (prems, concl)
- end;
+ val concl = HOLogic.mk_Trueprop (Free (s, UnivT') $ mk_univ_inj ts n i);
+ in Logic.list_implies (prems, concl) end;
val intr_ts = maps (fn ((_, (_, _, constrs)), rep_set_name) =>
map (make_intr rep_set_name (length constrs))
@@ -221,10 +224,12 @@
let
val T = Datatype_Aux.typ_of_dtyp descr' sorts dt;
val free_t = Datatype_Aux.mk_Free "x" T j;
- in (case (Datatype_Aux.strip_dtyp dt, strip_type T) of
- ((_, Datatype_Aux.DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
- (Const (nth all_rep_names m, U --> Univ_elT) $
- Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args)
+ in
+ (case (Datatype_Aux.strip_dtyp dt, strip_type T) of
+ ((_, Datatype_Aux.DtRec m), (Us, U)) =>
+ (j + 1, free_t :: l_args, mk_lim
+ (Const (nth all_rep_names m, U --> Univ_elT) $
+ Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args)
| _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
end;
@@ -251,16 +256,17 @@
(thy, defs, eqns, rep_congs, dist_lemmas) =
let
val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
- val rep_const = cterm_of thy
- (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
+ val rep_const =
+ cterm_of thy (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
val cong' =
Drule.export_without_context
(cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
val dist =
Drule.export_without_context
(cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
- val (thy', defs', eqns', _) = fold ((make_constr_def tname T) (length constrs))
- (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
+ val (thy', defs', eqns', _) =
+ fold ((make_constr_def tname T) (length constrs))
+ (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
in
(Sign.parent_path thy', defs', eqns @ [eqns'],
rep_congs @ [cong'], dist_lemmas @ [dist])
@@ -308,8 +314,10 @@
let
val T' = Datatype_Aux.typ_of_dtyp descr' sorts dt;
val (Us, U) = strip_type T'
- in (case Datatype_Aux.strip_dtyp dt of
- (_, Datatype_Aux.DtRec j) => if member (op =) ks' j then
+ in
+ (case Datatype_Aux.strip_dtyp dt of
+ (_, Datatype_Aux.DtRec j) =>
+ if member (op =) ks' j then
(i2 + 1, i2' + 1, ts @ [mk_lim (Datatype_Aux.app_bnds
(Datatype_Aux.mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
Ts @ [Us ---> Univ_elT])
@@ -341,29 +349,31 @@
fun process_dt (k, (tname, _, constrs)) (fs, eqns, isos) =
let
- val (fs', eqns', _) =
- fold (make_iso_def k ks (length constrs)) constrs (fs, eqns, 1);
- val iso = (nth recTs k, nth all_rep_names k)
+ val (fs', eqns', _) = fold (make_iso_def k ks (length constrs)) constrs (fs, eqns, 1);
+ val iso = (nth recTs k, nth all_rep_names k);
in (fs', eqns', isos @ [iso]) end;
-
+
val (fs, eqns, isos) = fold process_dt ds ([], [], []);
val fTs = map fastype_of fs;
- val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"),
- Logic.mk_equals (Const (iso_name, T --> Univ_elT),
- list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
+ val defs =
+ map (fn (rec_name, (T, iso_name)) =>
+ (Binding.name (Long_Name.base_name iso_name ^ "_def"),
+ Logic.mk_equals (Const (iso_name, T --> Univ_elT),
+ list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
val (def_thms, thy') =
apsnd Theory.checkpoint ((Global_Theory.add_defs false o map Thm.no_attributes) defs thy);
(* prove characteristic equations *)
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
- val char_thms' = map (fn eqn => Skip_Proof.prove_global thy' [] [] eqn
- (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
+ val char_thms' =
+ map (fn eqn => Skip_Proof.prove_global thy' [] [] eqn
+ (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
in (thy', char_thms' @ char_thms) end;
- val (thy5, iso_char_thms) = apfst Theory.checkpoint (fold_rev make_iso_defs
- (tl descr) (Sign.add_path big_name thy4, []));
+ val (thy5, iso_char_thms) =
+ apfst Theory.checkpoint (fold_rev make_iso_defs (tl descr) (Sign.add_path big_name thy4, []));
(* prove isomorphism properties *)
@@ -376,35 +386,37 @@
fun mk_thm i =
let
- val Ts = map (TFree o rpair HOLogic.typeS)
- (Name.variant_list used (replicate i "'t"));
- val f = Free ("f", Ts ---> U)
- in Skip_Proof.prove_global thy [] [] (Logic.mk_implies
- (HOLogic.mk_Trueprop (HOLogic.list_all
- (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
- HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
- r $ (a $ Datatype_Aux.app_bnds f i)), f))))
- (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
- REPEAT (etac allE 1), rtac thm 1, atac 1])
+ val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
+ val f = Free ("f", Ts ---> U);
+ in
+ Skip_Proof.prove_global thy [] []
+ (Logic.mk_implies
+ (HOLogic.mk_Trueprop (HOLogic.list_all
+ (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
+ r $ (a $ Datatype_Aux.app_bnds f i)), f))))
+ (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
+ REPEAT (etac allE 1), rtac thm 1, atac 1])
end
in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *)
- val fun_congs = map (fn T => make_elim (Drule.instantiate'
- [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
+ val fun_congs =
+ map (fn T => make_elim (Drule.instantiate' [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
fun prove_iso_thms ds (inj_thms, elem_thms) =
let
val (_, (tname, _, _)) = hd ds;
- val induct = (#induct o the o Symtab.lookup dt_info) tname;
+ val induct = #induct (the (Symtab.lookup dt_info tname));
fun mk_ind_concl (i, _) =
let
val T = nth recTs i;
val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
- val rep_set_name = nth rep_set_names i
- in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
+ val rep_set_name = nth rep_set_names i;
+ in
+ (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
HOLogic.mk_eq (Rep_t $ Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $
HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)),
Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i))
@@ -413,59 +425,60 @@
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 snd newT_iso_inj_thms @
- map (fn r => r RS @{thm injD}) inj_thms;
+ val inj_thms' = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) inj_thms;
- val inj_thm = Skip_Proof.prove_global thy5 [] []
- (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1)) (fn _ => EVERY
- [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
- REPEAT (EVERY
- [rtac allI 1, rtac impI 1,
- Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
- REPEAT (EVERY
- [hyp_subst_tac 1,
- rewrite_goals_tac rewrites,
- REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
- (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
- ORELSE (EVERY
- [REPEAT (eresolve_tac (Scons_inject ::
- map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
- REPEAT (cong_tac 1), rtac refl 1,
- REPEAT (atac 1 ORELSE (EVERY
- [REPEAT (rtac ext 1),
- REPEAT (eresolve_tac (mp :: allE ::
- map make_elim (Suml_inject :: Sumr_inject ::
- Lim_inject :: inj_thms') @ fun_congs) 1),
- atac 1]))])])])]);
+ val inj_thm =
+ Skip_Proof.prove_global thy5 [] []
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
+ (fn _ => EVERY
+ [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ REPEAT (EVERY
+ [rtac allI 1, rtac impI 1,
+ Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
+ REPEAT (EVERY
+ [hyp_subst_tac 1,
+ rewrite_goals_tac rewrites,
+ REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
+ (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
+ ORELSE (EVERY
+ [REPEAT (eresolve_tac (Scons_inject ::
+ map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
+ REPEAT (cong_tac 1), rtac refl 1,
+ REPEAT (atac 1 ORELSE (EVERY
+ [REPEAT (rtac ext 1),
+ REPEAT (eresolve_tac (mp :: allE ::
+ map make_elim (Suml_inject :: Sumr_inject ::
+ Lim_inject :: inj_thms') @ fun_congs) 1),
+ atac 1]))])])])]);
val inj_thms'' = map (fn r => r RS datatype_injI) (Datatype_Aux.split_conj_thm inj_thm);
- val elem_thm =
- Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
+ val elem_thm =
+ Skip_Proof.prove_global thy5 [] []
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
(fn _ =>
- EVERY [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
- rewrite_goals_tac rewrites,
- REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
- ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
+ EVERY [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ rewrite_goals_tac rewrites,
+ REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
+ ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
- in (inj_thms'' @ inj_thms, elem_thms @ (Datatype_Aux.split_conj_thm elem_thm))
- end;
+ in (inj_thms'' @ inj_thms, elem_thms @ (Datatype_Aux.split_conj_thm elem_thm)) end;
val (iso_inj_thms_unfolded, iso_elem_thms) =
fold_rev prove_iso_thms (tl descr) ([], map #3 newT_iso_axms);
- val iso_inj_thms = map snd newT_iso_inj_thms @
- map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
+ val iso_inj_thms =
+ map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
(* 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 $
- (Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
- (if i < length newTs then HOLogic.true_const
- else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
- Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
- Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
+ let val isoT = T --> Univ_elT in
+ HOLogic.imp $
+ (Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
+ (if i < length newTs then HOLogic.true_const
+ else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
+ Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
+ Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
end;
val iso_t = HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (map mk_iso_t
@@ -473,23 +486,24 @@
(* all the theorems are proved by one single simultaneous induction *)
- val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq}))
- iso_inj_thms_unfolded;
+ val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq})) iso_inj_thms_unfolded;
- val iso_thms = if length descr = 1 then [] else
- drop (length newTs) (Datatype_Aux.split_conj_thm
- (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
- [(Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
- REPEAT (rtac TrueI 1),
- rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
- Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
- rewrite_goals_tac (map Thm.symmetric range_eqs),
- REPEAT (EVERY
- [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
- maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
- TRY (hyp_subst_tac 1),
- rtac (sym RS range_eqI) 1,
- resolve_tac iso_char_thms 1])])));
+ val iso_thms =
+ if length descr = 1 then []
+ else
+ drop (length newTs) (Datatype_Aux.split_conj_thm
+ (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
+ [(Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ REPEAT (rtac TrueI 1),
+ rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
+ Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
+ rewrite_goals_tac (map Thm.symmetric range_eqs),
+ REPEAT (EVERY
+ [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
+ maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
+ TRY (hyp_subst_tac 1),
+ rtac (sym RS range_eqI) 1,
+ resolve_tac iso_char_thms 1])])));
val Abs_inverse_thms' =
map #1 newT_iso_axms @
@@ -503,17 +517,19 @@
val _ = Datatype_Aux.message config "Proving freeness of constructors ...";
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *)
-
+
fun prove_constr_rep_thm eqn =
let
val inj_thms = map fst newT_iso_inj_thms;
- val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
- in Skip_Proof.prove_global thy5 [] [] eqn (fn _ => EVERY
- [resolve_tac inj_thms 1,
- rewrite_goals_tac rewrites,
- rtac refl 3,
- resolve_tac rep_intrs 2,
- REPEAT (resolve_tac iso_elem_thms 1)])
+ val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms);
+ in
+ Skip_Proof.prove_global thy5 [] [] eqn
+ (fn _ => EVERY
+ [resolve_tac inj_thms 1,
+ rewrite_goals_tac rewrites,
+ rtac refl 3,
+ resolve_tac rep_intrs 2,
+ REPEAT (resolve_tac iso_elem_thms 1)])
end;
(*--------------------------------------------------------------*)
@@ -523,9 +539,10 @@
val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns;
- val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
- dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
- (constr_rep_thms ~~ dist_lemmas);
+ val dist_rewrites =
+ map (fn (rep_thms, dist_lemma) =>
+ dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
+ (constr_rep_thms ~~ dist_lemmas);
fun prove_distinct_thms dist_rewrites' (k, ts) =
let
@@ -537,29 +554,34 @@
in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove ts end;
in prove ts end;
- val distinct_thms = map2 (prove_distinct_thms)
- dist_rewrites (Datatype_Prop.make_distincts descr sorts);
+ val distinct_thms =
+ map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr sorts);
(* prove injectivity of constructors *)
fun prove_constr_inj_thm rep_thms t =
- let val inj_thms = Scons_inject :: (map make_elim
- (iso_inj_thms @
- [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
- Lim_inject, Suml_inject, Sumr_inject]))
- in Skip_Proof.prove_global thy5 [] [] t (fn _ => EVERY
- [rtac iffI 1,
- REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
- dresolve_tac rep_congs 1, dtac box_equals 1,
- REPEAT (resolve_tac rep_thms 1),
- REPEAT (eresolve_tac inj_thms 1),
- REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
- REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
- atac 1]))])
+ let
+ val inj_thms = Scons_inject ::
+ map make_elim
+ (iso_inj_thms @
+ [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
+ Lim_inject, Suml_inject, Sumr_inject])
+ in
+ Skip_Proof.prove_global thy5 [] [] t
+ (fn _ => EVERY
+ [rtac iffI 1,
+ REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
+ dresolve_tac rep_congs 1, dtac box_equals 1,
+ REPEAT (resolve_tac rep_thms 1),
+ REPEAT (eresolve_tac inj_thms 1),
+ REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
+ REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
+ atac 1]))])
end;
- val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
- ((Datatype_Prop.make_injs descr sorts) ~~ constr_rep_thms);
+ val constr_inject =
+ map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
+ ((Datatype_Prop.make_injs descr sorts) ~~ constr_rep_thms);
val ((constr_inject', distinct_thms'), thy6) =
thy5
@@ -571,22 +593,22 @@
val _ = Datatype_Aux.message config "Proving induction rule for datatypes ...";
- val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
- (map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded);
+ val Rep_inverse_thms =
+ map (fn (_, iso, _) => iso RS subst) newT_iso_axms @
+ map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded;
val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded;
fun mk_indrule_lemma ((i, _), T) (prems, concls) =
let
- val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $
- Datatype_Aux.mk_Free "x" T i;
+ val Rep_t =
+ Const (nth all_rep_names i, T --> Univ_elT) $ Datatype_Aux.mk_Free "x" T i;
- val Abs_t = if i < length newTs then
- Const (Sign.intern_const thy6
- ("Abs_" ^ (nth new_type_names i)), Univ_elT --> T)
+ val Abs_t =
+ if i < length newTs then
+ Const (Sign.intern_const thy6 ("Abs_" ^ nth new_type_names i), Univ_elT --> T)
else Const (@{const_name the_inv_into},
[HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
- HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
-
+ HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT);
in
(prems @
[HOLogic.imp $
@@ -601,31 +623,38 @@
val cert = cterm_of thy6;
- val indrule_lemma = Skip_Proof.prove_global thy6 [] []
- (Logic.mk_implies
- (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
- HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY
+ val indrule_lemma =
+ Skip_Proof.prove_global thy6 [] []
+ (Logic.mk_implies
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
+ HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls)))
+ (fn _ =>
+ EVERY
[REPEAT (etac conjE 1),
REPEAT (EVERY
[TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
etac mp 1, resolve_tac iso_elem_thms 1])]);
val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
- val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
- map (Free o apfst fst o dest_Var) Ps;
+ val frees =
+ if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
+ else map (Free o apfst fst o dest_Var) Ps;
val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
val dt_induct_prop = Datatype_Prop.make_ind descr sorts;
- val dt_induct = Skip_Proof.prove_global thy6 []
- (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
- (fn {prems, ...} => EVERY
- [rtac indrule_lemma' 1,
- (Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
- EVERY (map (fn (prem, r) => (EVERY
- [REPEAT (eresolve_tac Abs_inverse_thms 1),
- simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
- DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
- (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
+ val dt_induct =
+ Skip_Proof.prove_global thy6 []
+ (Logic.strip_imp_prems dt_induct_prop)
+ (Logic.strip_imp_concl dt_induct_prop)
+ (fn {prems, ...} =>
+ EVERY
+ [rtac indrule_lemma' 1,
+ (Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ EVERY (map (fn (prem, r) => (EVERY
+ [REPEAT (eresolve_tac Abs_inverse_thms 1),
+ simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
+ DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
+ (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
val ([dt_induct'], thy7) =
thy6
@@ -647,21 +676,20 @@
val _ = Theory.requires thy "Datatype" "datatype definitions";
(* this theory is used just for parsing *)
- val tmp_thy = thy |>
- Theory.copy |>
- Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
- (tname, length tvs, mx)) dts);
+ val tmp_thy = thy
+ |> Theory.copy
+ |> Sign.add_types_global (map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dts);
- val (tyvars, _, _, _)::_ = dts;
+ val (tyvars, _, _, _) ::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
- let val full_tname = Sign.full_name tmp_thy tname
- in
+ let val full_tname = Sign.full_name tmp_thy tname in
(case duplicates (op =) tvs of
[] =>
if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
else error ("Mutually recursive datatypes must have same type parameters")
- | dups => error ("Duplicate parameter(s) for datatype " ^ Binding.print tname ^
- " : " ^ commas dups))
+ | dups =>
+ error ("Duplicate parameter(s) for datatype " ^ Binding.print tname ^
+ " : " ^ commas dups))
end) dts);
val dt_names = map fst new_dts;
@@ -683,24 +711,23 @@
in
(constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
- end handle ERROR msg => cat_error msg
- ("The error above occurred in constructor " ^ Binding.print cname ^
- " of datatype " ^ Binding.print tname);
+ end handle ERROR msg =>
+ cat_error msg ("The error above occurred in constructor " ^ Binding.print cname ^
+ " of datatype " ^ Binding.print tname);
- val (constrs', constr_syntax', sorts') =
- fold prep_constr constrs ([], [], sorts)
+ val (constrs', constr_syntax', sorts') = fold prep_constr constrs ([], [], sorts);
in
- case duplicates (op =) (map fst constrs') of
+ (case duplicates (op =) (map fst constrs') of
[] =>
(dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
| dups =>
- error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname)
+ error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname))
end;
- val (dts', constr_syntax, sorts', i) =
- fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
- val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
+ val (dts', constr_syntax, sorts', i) = fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
+ val sorts =
+ sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
val dt_info = Datatype_Data.get_all thy;
val (descr, _) = Datatype_Aux.unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
val _ =
@@ -715,9 +742,10 @@
thy
|> representation_proofs config dt_info new_type_names descr sorts
types_syntax constr_syntax (Datatype_Data.mk_case_names_induct (flat descr))
- |-> (fn (inject, distinct, induct) => Datatype_Data.derive_datatype_props
- config dt_names (SOME new_type_names) descr sorts
- induct inject distinct)
+ |-> (fn (inject, distinct, induct) =>
+ Datatype_Data.derive_datatype_props
+ config dt_names (SOME new_type_names) descr sorts
+ induct inject distinct)
end;
val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Nov 30 21:14:01 2011 +0100
@@ -53,29 +53,33 @@
let
val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
Abs ("z", T', Const (@{const_name True}, T''))) induct_Ps;
- val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
- Var (("P", 0), HOLogic.boolT))
- val insts = take i dummyPs @ (P::(drop (i + 1) dummyPs));
+ val P =
+ Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
+ Var (("P", 0), HOLogic.boolT));
+ val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
val cert = cterm_of thy;
- val insts' = (map cert induct_Ps) ~~ (map cert insts);
- val induct' = refl RS ((nth
- (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
-
+ val insts' = map cert induct_Ps ~~ map cert insts;
+ val induct' =
+ refl RS
+ (nth (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i RSN (2, rev_mp));
in
- Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
- (fn {prems, ...} => EVERY
- [rtac induct' 1,
- REPEAT (rtac TrueI 1),
- REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
- REPEAT (rtac TrueI 1)])
+ Skip_Proof.prove_global thy []
+ (Logic.strip_imp_prems t)
+ (Logic.strip_imp_concl t)
+ (fn {prems, ...} =>
+ EVERY
+ [rtac induct' 1,
+ REPEAT (rtac TrueI 1),
+ REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
+ REPEAT (rtac TrueI 1)])
end;
- val casedist_thms = map_index prove_casedist_thm
- (newTs ~~ Datatype_Prop.make_casedists descr sorts)
+ val casedist_thms =
+ map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr sorts);
in
thy
|> Datatype_Aux.store_thms_atts "exhaust" new_type_names
- (map single case_names_exhausts) casedist_thms
+ (map single case_names_exhausts) casedist_thms
end;
@@ -98,53 +102,58 @@
val big_rec_name' = big_name ^ "_rec_set";
val rec_set_names' =
- if length descr' = 1 then [big_rec_name'] else
+ 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_bname thy0) rec_set_names';
val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr sorts used;
- val rec_set_Ts = map (fn (T1, T2) =>
- reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (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 (Datatype_Aux.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);
+ val rec_fns =
+ map (uncurry (Datatype_Aux.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 rec_set (cname, cargs) (rec_intr_ts, l) =
let
fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
- let val free1 = Datatype_Aux.mk_Free "x" U j
- in (case (Datatype_Aux.strip_dtyp dt, strip_type U) of
- ((_, Datatype_Aux.DtRec m), (Us, _)) =>
- let
- val free2 = Datatype_Aux.mk_Free "y" (Us ---> 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, nth rec_sets' m $
- Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
- free1::t1s, free2::t2s)
- end
- | _ => (j + 1, k, prems, free1::t1s, t2s))
+ let val free1 = Datatype_Aux.mk_Free "x" U j in
+ (case (Datatype_Aux.strip_dtyp dt, strip_type U) of
+ ((_, Datatype_Aux.DtRec m), (Us, _)) =>
+ let
+ val free2 = Datatype_Aux.mk_Free "y" (Us ---> 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, nth rec_sets' m $
+ Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
+ free1 :: t1s, free2 :: t2s)
+ end
+ | _ => (j + 1, k, prems, free1::t1s, t2s))
end;
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
- val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
+ val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], []);
- in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
- (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
- list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
+ in
+ (rec_intr_ts @
+ [Logic.list_implies (prems, HOLogic.mk_Trueprop
+ (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
+ list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
end;
- val (rec_intr_ts, _) = fold (fn ((d, T), set_name) =>
- fold (make_rec_intr T set_name) (#3 (snd d)))
- (descr' ~~ recTs ~~ rec_sets') ([], 0);
+ val (rec_intr_ts, _) =
+ fold (fn ((d, T), set_name) =>
+ fold (make_rec_intr T set_name) (#3 (snd d))) (descr' ~~ recTs ~~ rec_sets') ([], 0);
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
thy0
@@ -165,19 +174,20 @@
fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
let
val distinct_tac =
- (if i < length newTs then
- full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
- else full_simp_tac (HOL_ss addsimps (flat other_dist_rewrites)) 1);
+ if i < length newTs then
+ full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
+ else full_simp_tac (HOL_ss addsimps (flat other_dist_rewrites)) 1;
- val inject = map (fn r => r RS iffD1)
- (if i < length newTs then nth constr_inject i
- else injects_of tname);
+ val inject =
+ map (fn r => r RS iffD1)
+ (if i < length newTs then nth constr_inject i else injects_of tname);
- fun mk_unique_constr_tac n (cname, cargs) (tac, intr::intrs, j) =
+ fun mk_unique_constr_tac n (cname, cargs) (tac, intr :: intrs, j) =
let
- val k = length (filter Datatype_Aux.is_rec_type cargs)
-
- in (EVERY [DETERM tac,
+ val k = length (filter Datatype_Aux.is_rec_type cargs);
+ in
+ (EVERY
+ [DETERM tac,
REPEAT (etac ex1E 1), rtac ex1I 1,
DEPTH_SOLVE_1 (ares_tac [intr] 1),
REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
@@ -192,26 +202,26 @@
intrs, j + 1)
end;
- val (tac', intrs', _) = fold (mk_unique_constr_tac (length constrs))
- constrs (tac, intrs, 0);
-
+ val (tac', intrs', _) =
+ fold (mk_unique_constr_tac (length constrs)) constrs (tac, intrs, 0);
in (tac', intrs') end;
val rec_unique_thms =
let
- val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
- Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
- absfree ("y", T2) (set_t $ Datatype_Aux.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);
- val induct' = cterm_instantiate ((map cert induct_Ps) ~~
- (map cert insts)) induct;
- val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
- (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
- THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
-
+ val rec_unique_ts =
+ map (fn (((set_t, T1), T2), i) =>
+ Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
+ absfree ("y", T2) (set_t $ Datatype_Aux.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);
+ val induct' = cterm_instantiate (map cert induct_Ps ~~ map cert insts) induct;
+ val (tac, _) =
+ fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
+ (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
+ rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
in
Datatype_Aux.split_conj_thm (Skip_Proof.prove_global thy1 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts)) (K tac))
@@ -221,27 +231,28 @@
(* define primrec combinators *)
- val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
- val reccomb_names = map (Sign.full_bname thy1)
- (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, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
+ val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
+ val reccomb_names =
+ map (Sign.full_bname thy1)
+ (if length descr' = 1 then [big_reccomb_name]
+ else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto (length descr')));
+ val reccombs =
+ map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
(reccomb_names ~~ recTs ~~ rec_result_Ts);
val (reccomb_defs, thy2) =
thy1
|> Sign.add_consts_i (map (fn ((name, T), T') =>
- (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
- (reccomb_names ~~ recTs ~~ rec_result_Ts))
+ (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
+ (reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (Global_Theory.add_defs false o map Thm.no_attributes)
- (map (fn ((((name, comb), set), T), T') =>
- (Binding.name (Long_Name.base_name name ^ "_def"),
- Logic.mk_equals (comb, absfree ("x", T)
- (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
- (set $ Free ("x", T) $ Free ("y", T'))))))
- (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
+ (map
+ (fn ((((name, comb), set), T), T') =>
+ (Binding.name (Long_Name.base_name name ^ "_def"),
+ Logic.mk_equals (comb, absfree ("x", T)
+ (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
+ (set $ Free ("x", T) $ Free ("y", T'))))))
+ (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
||> Sign.parent_path
||> Theory.checkpoint;
@@ -250,14 +261,16 @@
val _ = Datatype_Aux.message config "Proving characteristic theorems for primrec combinators ...";
- val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
- (fn _ => EVERY
- [rewrite_goals_tac reccomb_defs,
- rtac @{thm the1_equality} 1,
- resolve_tac rec_unique_thms 1,
- resolve_tac rec_intrs 1,
- REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
- (Datatype_Prop.make_primrecs new_type_names descr sorts thy2);
+ val rec_thms =
+ map (fn t =>
+ Skip_Proof.prove_global thy2 [] [] t
+ (fn _ => EVERY
+ [rewrite_goals_tac reccomb_defs,
+ rtac @{thm the1_equality} 1,
+ resolve_tac rec_unique_thms 1,
+ resolve_tac rec_intrs 1,
+ REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
+ (Datatype_Prop.make_primrecs new_type_names descr sorts thy2);
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
@@ -285,52 +298,55 @@
fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
- val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
- let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
- val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
- in Const (@{const_name undefined}, Ts @ Ts' ---> T')
- end) constrs) descr';
+ val case_dummy_fns =
+ map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
+ let
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
+ in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
(* define case combinators via primrec combinators *)
- val (case_defs, thy2) = fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
- let
- val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
- let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
- val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
- val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
- val frees = take (length cargs) frees';
- val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j
- in
- (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
- end) (constrs ~~ (1 upto length constrs)));
-
- val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
- val fns = flat (take i case_dummy_fns) @
- fns2 @ flat (drop (i + 1) case_dummy_fns);
- val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
- val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
- val def = (Binding.name (Long_Name.base_name name ^ "_def"),
- Logic.mk_equals (list_comb (Const (name, caseT), fns1),
- list_comb (reccomb, (flat (take i case_dummy_fns)) @
- fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
- val ([def_thm], thy') =
- thy
- |> Sign.declare_const_global decl |> snd
- |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
-
- in (defs @ [def_thm], thy')
- end) (hd descr ~~ newTs ~~ case_names ~~
- take (length newTs) reccomb_names) ([], thy1)
+ val (case_defs, thy2) =
+ fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
+ let
+ val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
+ let
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+ val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
+ val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
+ val frees = take (length cargs) frees';
+ val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j;
+ in
+ (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
+ end) (constrs ~~ (1 upto length constrs)));
+
+ val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
+ val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
+ val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
+ val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
+ val def =
+ (Binding.name (Long_Name.base_name name ^ "_def"),
+ Logic.mk_equals (list_comb (Const (name, caseT), fns1),
+ list_comb (reccomb, (flat (take i case_dummy_fns)) @
+ fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
+ val ([def_thm], thy') =
+ thy
+ |> Sign.declare_const_global decl |> snd
+ |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
+
+ in (defs @ [def_thm], thy') end)
+ (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1)
||> Theory.checkpoint;
- val case_thms = map (map (fn t => Skip_Proof.prove_global thy2 [] [] t
- (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
- (Datatype_Prop.make_cases new_type_names descr sorts thy2)
+ val case_thms =
+ (map o map) (fn t =>
+ Skip_Proof.prove_global thy2 [] [] t
+ (fn _ =>
+ EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
+ (Datatype_Prop.make_cases new_type_names descr sorts thy2);
in
thy2
|> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
@@ -351,23 +367,23 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
- fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
- exhaustion), case_thms'), T) =
+ fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
let
val cert = cterm_of thy;
val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
- val exhaustion' = cterm_instantiate
- [(cert lhs, cert (Free ("x", T)))] exhaustion;
- val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
- (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
+ val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
+ val tac =
+ EVERY [rtac exhaustion' 1,
+ ALLGOALS (asm_simp_tac (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))];
in
- (Skip_Proof.prove_global thy [] [] t1 tacf,
- Skip_Proof.prove_global thy [] [] t2 tacf)
+ (Skip_Proof.prove_global thy [] [] t1 (K tac),
+ Skip_Proof.prove_global thy [] [] t2 (K tac))
end;
- val split_thm_pairs = map prove_split_thms
- ((Datatype_Prop.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
- dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
+ val split_thm_pairs =
+ map prove_split_thms
+ ((Datatype_Prop.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
+ dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
@@ -381,11 +397,11 @@
fun prove_weak_case_congs new_type_names descr sorts thy =
let
fun prove_weak_case_cong t =
- Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
- (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
+ Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+ (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1]);
- val weak_case_congs = map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs
- new_type_names descr sorts thy)
+ val weak_case_congs =
+ map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr sorts thy);
in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
@@ -399,18 +415,18 @@
fun prove_nchotomy (t, exhaustion) =
let
(* For goal i, select the correct disjunct to attack, then prove it *)
- fun tac i 0 = EVERY [TRY (rtac disjI1 i),
- hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
- | tac i n = rtac disjI2 i THEN tac i (n - 1)
- in
- Skip_Proof.prove_global thy [] [] t (fn _ =>
- EVERY [rtac allI 1,
- Datatype_Aux.exh_tac (K exhaustion) 1,
- ALLGOALS (fn i => tac i (i-1))])
+ fun tac i 0 = EVERY [TRY (rtac disjI1 i), hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
+ | tac i n = rtac disjI2 i THEN tac i (n - 1);
+ in
+ Skip_Proof.prove_global thy [] [] t
+ (fn _ =>
+ EVERY [rtac allI 1,
+ Datatype_Aux.exh_tac (K exhaustion) 1,
+ ALLGOALS (fn i => tac i (i - 1))])
end;
val nchotomys =
- map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms)
+ map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms);
in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
@@ -418,25 +434,27 @@
let
fun prove_case_cong ((t, nchotomy), case_rewrites) =
let
- val (Const ("==>", _) $ tm $ _) = t;
- val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma)) = tm;
+ val Const ("==>", _) $ tm $ _ = t;
+ val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
val cert = cterm_of thy;
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_vars (concl_of nchotomy') [];
- val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy'
+ val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
in
Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
- (fn {prems, ...} =>
- let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
- in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
+ (fn {prems, ...} =>
+ let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) in
+ EVERY [
+ simp_tac (HOL_ss addsimps [hd prems]) 1,
cut_facts_tac [nchotomy''] 1,
REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
end)
end;
- val case_congs = map prove_case_cong (Datatype_Prop.make_case_congs
- new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
+ val case_congs =
+ map prove_case_cong (Datatype_Prop.make_case_congs
+ new_type_names descr sorts thy ~~ nchotomys ~~ case_thms);
in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 21:14:01 2011 +0100
@@ -39,7 +39,7 @@
include DATATYPE_COMMON
val message : config -> string -> unit
-
+
val store_thmss_atts : string -> string list -> attribute list list -> thm list list
-> theory -> thm list list * theory
val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
@@ -76,7 +76,7 @@
-> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
-> ((string * typ list) * (string * 'a list) list) list
val check_nonempty : descr list -> unit
- val unfold_datatypes :
+ val unfold_datatypes :
theory -> descr -> (string * sort) list -> info Symtab.table ->
descr -> int -> descr list * int
val find_shortest_path : descr -> int -> (string * int) option
@@ -147,12 +147,13 @@
(case flt (Misc_Legacy.term_frees t2) of
[Free (s, T)] => SOME (absfree (s, T) t2)
| _ => NONE)
- | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
- val insts = map_filter (fn (t, u) =>
- case abstr (getP u) of
- NONE => NONE
- | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u')) (ts ~~ ts');
- val indrule' = cterm_instantiate insts indrule
+ | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))));
+ val insts =
+ map_filter (fn (t, u) =>
+ (case abstr (getP u) of
+ NONE => NONE
+ | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
+ val indrule' = cterm_instantiate insts indrule;
in rtac indrule' i end);
@@ -169,7 +170,7 @@
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' =
cterm_instantiate [(cterm_of thy (head_of lhs),
- cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
+ cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion;
in compose_tac (false, exhaustion', nprems_of exhaustion) i end);
@@ -205,12 +206,10 @@
split : thm,
split_asm: thm};
-fun mk_Free s T i = Free (s ^ (string_of_int i), T);
+fun mk_Free s T i = Free (s ^ string_of_int i, T);
-fun subst_DtTFree _ substs (T as (DtTFree name)) =
- AList.lookup (op =) substs name |> the_default T
- | subst_DtTFree i substs (DtType (name, ts)) =
- DtType (name, map (subst_DtTFree i substs) ts)
+fun subst_DtTFree _ substs (T as DtTFree name) = the_default T (AList.lookup (op =) substs name)
+ | subst_DtTFree i substs (DtType (name, ts)) = DtType (name, map (subst_DtTFree i substs) ts)
| subst_DtTFree i _ (DtRec j) = DtRec (i + j);
exception Datatype;
@@ -235,9 +234,10 @@
| mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
fun name_of_typ (Type (s, Ts)) =
- let val s' = Long_Name.base_name s
- in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @
- [if Lexicon.is_identifier s' then s' else "x"])
+ let val s' = Long_Name.base_name s in
+ space_implode "_"
+ (filter_out (equal "") (map name_of_typ Ts) @
+ [if Lexicon.is_identifier s' then s' else "x"])
end
| name_of_typ _ = "";
@@ -245,17 +245,17 @@
| dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
| dtyp_of_typ new_dts (Type (tname, Ts)) =
(case AList.lookup (op =) new_dts tname of
- NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
- | SOME vs => if map (try (fst o dest_TFree)) Ts = map SOME vs then
- DtRec (find_index (curry op = tname o fst) new_dts)
- else error ("Illegal occurrence of recursive type " ^ tname));
+ NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
+ | SOME vs =>
+ if map (try (fst o dest_TFree)) Ts = map SOME vs then
+ DtRec (find_index (curry op = tname o fst) new_dts)
+ else error ("Illegal occurrence of recursive type " ^ tname));
fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, (the o AList.lookup (op =) sorts) a)
| typ_of_dtyp descr sorts (DtRec i) =
- let val (s, ds, _) = (the o AList.lookup (op =) descr) i
+ let val (s, ds, _) = the (AList.lookup (op =) descr i)
in Type (s, map (typ_of_dtyp descr sorts) ds) end
- | typ_of_dtyp descr sorts (DtType (s, ds)) =
- Type (s, map (typ_of_dtyp descr sorts) ds);
+ | typ_of_dtyp descr sorts (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr sorts) ds);
(* find all non-recursive types in datatype description *)
@@ -271,28 +271,34 @@
(* get all branching types *)
fun get_branching_types descr sorts =
- map (typ_of_dtyp descr sorts) (fold (fn (_, (_, _, constrs)) =>
- fold (fn (_, cargs) => fold (strip_dtyp #> fst #> fold (insert op =)) cargs)
- constrs) descr []);
+ map (typ_of_dtyp descr sorts)
+ (fold
+ (fn (_, (_, _, constrs)) =>
+ fold (fn (_, cargs) => fold (strip_dtyp #> fst #> fold (insert op =)) cargs) constrs)
+ descr []);
-fun get_arities descr = fold (fn (_, (_, _, constrs)) =>
- fold (fn (_, cargs) => fold (insert op =) (map (length o fst o strip_dtyp)
- (filter is_rec_type cargs))) constrs) descr [];
+fun get_arities descr =
+ fold
+ (fn (_, (_, _, constrs)) =>
+ fold (fn (_, cargs) =>
+ fold (insert op =) (map (length o fst o strip_dtyp) (filter is_rec_type cargs))) constrs)
+ descr [];
(* interpret construction of datatype *)
-fun interpret_construction descr vs { atyp, dtyp } =
+fun interpret_construction descr vs {atyp, dtyp} =
let
val typ_of_dtyp = typ_of_dtyp descr vs;
- fun interpT dT = case strip_dtyp dT
- of (dTs, DtRec l) =>
+ fun interpT dT =
+ (case strip_dtyp dT of
+ (dTs, DtRec l) =>
let
- val (tyco, dTs', _) = (the o AList.lookup (op =) descr) l;
+ val (tyco, dTs', _) = the (AList.lookup (op =) descr l);
val Ts = map typ_of_dtyp dTs;
val Ts' = map typ_of_dtyp dTs';
val is_proper = forall (can dest_TFree) Ts';
in dtyp Ts (l, is_proper) (tyco, Ts') end
- | _ => atyp (typ_of_dtyp dT);
+ | _ => atyp (typ_of_dtyp dT));
fun interpC (c, dTs) = (c, map interpT dTs);
fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of_dtyp dTs), map interpC cs);
in map interpD descr end;
@@ -304,52 +310,58 @@
val descr' = flat descr;
fun is_nonempty_dt is i =
let
- val (_, _, constrs) = (the o AList.lookup (op =) descr') i;
- fun arg_nonempty (_, DtRec i) = if member (op =) is i then false
- else is_nonempty_dt (i::is) i
+ val (_, _, constrs) = the (AList.lookup (op =) descr' i);
+ fun arg_nonempty (_, DtRec i) =
+ if member (op =) is i then false
+ else is_nonempty_dt (i :: is) i
| arg_nonempty _ = true;
- in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
- end
- in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
- (fn (_, (s, _, _)) => raise Datatype_Empty s)
+ in exists (forall (arg_nonempty o strip_dtyp) o snd) constrs end
+ in
+ assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
+ (fn (_, (s, _, _)) => raise Datatype_Empty s)
end;
(* unfold a list of mutually recursive datatype specifications *)
(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
(* need to be unfolded *)
-fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i =
+fun unfold_datatypes thy orig_descr sorts (dt_info : info Symtab.table) descr i =
let
- fun typ_error T msg = error ("Non-admissible type expression\n" ^
- Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
+ fun typ_error T msg =
+ error ("Non-admissible type expression\n" ^
+ Syntax.string_of_typ_global thy (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
fun get_dt_descr T i tname dts =
(case Symtab.lookup dt_info tname of
- NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
- \ nested recursion")
- | (SOME {index, descr, ...}) =>
- let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
- val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths =>
- typ_error T ("Type constructor " ^ tname ^ " used with wrong\
- \ number of arguments")
- in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
- (tn, map (subst_DtTFree i subst) args,
- map (apsnd (map (subst_DtTFree i subst))) cs))) descr)
- end);
+ NONE =>
+ typ_error T (tname ^ " is not a datatype - can't use it in nested recursion")
+ | SOME {index, descr, ...} =>
+ let
+ val (_, vars, _) = the (AList.lookup (op =) descr index);
+ val subst = (map dest_DtTFree vars ~~ dts)
+ handle ListPair.UnequalLengths =>
+ typ_error T ("Type constructor " ^ tname ^ " used with wrong number of arguments");
+ in
+ (i + index,
+ map (fn (j, (tn, args, cs)) =>
+ (i + j, (tn, map (subst_DtTFree i subst) args,
+ map (apsnd (map (subst_DtTFree i subst))) cs))) descr)
+ end);
(* unfold a single constructor argument *)
fun unfold_arg T (i, Ts, descrs) =
if is_rec_type T then
- let val (Us, U) = strip_dtyp T
- in if exists is_rec_type Us then
+ let val (Us, U) = strip_dtyp T in
+ if exists is_rec_type Us then
typ_error T "Non-strictly positive recursive occurrence of type"
- else (case U of
- DtType (tname, dts) =>
+ else
+ (case U of
+ DtType (tname, dts) =>
let
val (index, descr) = get_dt_descr T i tname dts;
- val (descr', i') = unfold_datatypes sign orig_descr sorts
- dt_info descr (i + length descr)
+ val (descr', i') =
+ unfold_datatypes thy orig_descr sorts dt_info descr (i + length descr);
in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
| _ => (i, Ts @ [T], descrs))
end
@@ -375,17 +387,19 @@
fun find_nonempty descr is i =
let
- fun arg_nonempty (_, DtRec i) = if member (op =) is i
+ fun arg_nonempty (_, DtRec i) =
+ if member (op =) is i
then NONE
- else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
+ else Option.map (Integer.add 1 o snd) (find_nonempty descr (i :: is) i)
| arg_nonempty _ = SOME 0;
fun max_inf (SOME i) (SOME j) = SOME (Integer.max i j)
| max_inf _ _ = NONE;
fun max xs = fold max_inf xs (SOME 0);
val (_, _, constrs) = the (AList.lookup (op =) descr i);
- val xs = sort (int_ord o pairself snd)
- (map_filter (fn (s, dts) => Option.map (pair s)
- (max (map (arg_nonempty o strip_dtyp) dts))) constrs)
+ val xs =
+ sort (int_ord o pairself snd)
+ (map_filter (fn (s, dts) => Option.map (pair s)
+ (max (map (arg_nonempty o strip_dtyp) dts))) constrs)
in if null xs then NONE else SOME (hd xs) end;
fun find_shortest_path descr i = find_nonempty descr [i] i;
--- a/src/HOL/Tools/Datatype/datatype_case.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Wed Nov 30 21:14:01 2011 +0100
@@ -74,18 +74,18 @@
let
val (_, Ty) = dest_Const c
val Ts = binder_types Ty;
- val names = Name.variant_list used
- (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
+ val names =
+ Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
val ty = body_type Ty;
- val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
- raise CASE_ERROR ("type mismatch", ~1)
- val c' = ty_inst ty_theta c
- val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
+ val ty_theta = ty_match ty colty
+ handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
+ val c' = ty_inst ty_theta c;
+ val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts);
in (c', gvars) end;
(*Goes through a list of rows and picks out the ones beginning with a
- pattern with constructor = name.*)
+ pattern with constructor = name.*)
fun mk_group (name, T) rows =
let val k = length (binder_types T) in
fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
@@ -94,13 +94,11 @@
(Const (name', _), args) =>
if name = name' then
if length args = k then
- let val (args', cnstrts') = split_list (map strip_constraints args)
- in
+ let val (args', cnstrts') = split_list (map strip_constraints args) in
((((prfx, args' @ ps), rhs) :: in_group, not_in_group),
(default_names names args', map2 append cnstrts cnstrts'))
end
- else raise CASE_ERROR
- ("Wrong number of arguments for constructor " ^ name, i)
+ else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ name, i)
else ((in_group, row :: not_in_group), (names, cnstrts))
| _ => raise CASE_ERROR ("Not a constructor pattern", i)))
rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
@@ -114,12 +112,10 @@
(rows as (((prfx, _ :: ps), _) :: _)) =
let
fun part [] [] = []
- | part [] ((_, (_, i)) :: _) =
- raise CASE_ERROR ("Not a constructor pattern", i)
+ | part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
| part (c :: cs) rows =
let
- val ((in_group, not_in_group), (names, cnstrts)) =
- mk_group (dest_Const c) rows;
+ val ((in_group, not_in_group), (names, cnstrts)) = mk_group (dest_Const c) rows;
val used' = fold add_row_used in_group used;
val (c', gvars) = fresh_constr ty_match ty_inst colty used' c;
val in_group' =
@@ -127,9 +123,10 @@
then
let
val Ts = map type_of ps;
- val xs = Name.variant_list
- (fold Term.add_free_names gvars used')
- (replicate (length ps) "x")
+ val xs =
+ Name.variant_list
+ (fold Term.add_free_names gvars used')
+ (replicate (length ps) "x");
in
[((prfx, gvars @ map Free (xs ~~ Ts)),
(Const (@{const_syntax undefined}, res_ty), ~1))]
@@ -144,33 +141,28 @@
end
in part constructors rows end;
-fun v_to_prfx (prfx, Free v::pats) = (v::prfx,pats)
+fun v_to_prfx (prfx, Free v :: pats) = (v :: prfx, pats)
| v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
(* Translation of pattern terms into nested case expressions. *)
-
+
fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
let
val name = singleton (Name.variant_list used) "a";
- fun expand constructors used ty ((_, []), _) =
- raise CASE_ERROR ("mk_case: expand_var_row", ~1)
+ fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1)
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
if is_Free p then
let
val used' = add_row_used row used;
fun expnd c =
- let val capp =
- list_comb (fresh_constr ty_match ty_inst ty used' c)
- in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag))
- end
+ let val capp = list_comb (fresh_constr ty_match ty_inst ty used' c)
+ in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end
in map expnd constructors end
else [row]
fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
- | mk [] (((_, []), (tm, tag)) :: _) = (* Done *)
- ([tag], tm)
- | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) =
- mk path [row]
+ | mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
+ | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
| mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
(case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
@@ -183,28 +175,28 @@
(case ty_info tab (cname, cT) of
NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
| SOME {case_name, constructors} =>
- let
- val pty = body_type cT;
- val used' = fold Term.add_free_names us used;
- val nrows = maps (expand constructors used' pty) rows;
- val subproblems = partition ty_match ty_inst type_of used'
- constructors pty range_ty nrows;
- val (pat_rect, dtrees) = split_list (map (fn {new_formals, group, ...} =>
- mk (new_formals @ us) group) subproblems)
- val case_functions = map2
- (fn {new_formals, names, constraints, ...} =>
- fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
- Abs (if s = "" then name else s, T,
- abstract_over (x, t)) |>
- fold mk_fun_constrain cnstrts)
- (new_formals ~~ names ~~ constraints))
- subproblems dtrees;
- val types = map type_of (case_functions @ [u]);
- val case_const = Const (case_name, types ---> range_ty)
- val tree = list_comb (case_const, case_functions @ [u])
- in (flat pat_rect, tree) end)
- | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
- Syntax.string_of_term ctxt t, i))
+ let
+ val pty = body_type cT;
+ val used' = fold Term.add_free_names us used;
+ val nrows = maps (expand constructors used' pty) rows;
+ val subproblems =
+ partition ty_match ty_inst type_of used'
+ constructors pty range_ty nrows;
+ val (pat_rect, dtrees) =
+ split_list (map (fn {new_formals, group, ...} =>
+ mk (new_formals @ us) group) subproblems);
+ val case_functions =
+ map2 (fn {new_formals, names, constraints, ...} =>
+ fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
+ Abs (if s = "" then name else s, T, abstract_over (x, t))
+ |> fold mk_fun_constrain cnstrts) (new_formals ~~ names ~~ constraints))
+ subproblems dtrees;
+ val types = map type_of (case_functions @ [u]);
+ val case_const = Const (case_name, types ---> range_ty);
+ val tree = list_comb (case_const, case_functions @ [u]);
+ in (flat pat_rect, tree) end)
+ | SOME (t, i) =>
+ raise CASE_ERROR ("Not a datatype constructor: " ^ Syntax.string_of_term ctxt t, i))
end
| mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1)
in mk end;
@@ -213,11 +205,12 @@
(*Repeated variable occurrences in a pattern are not allowed.*)
fun no_repeat_vars ctxt pat = fold_aterms
- (fn x as Free (s, _) => (fn xs =>
- if member op aconv xs x then
- case_error (quote s ^ " occurs repeatedly in the pattern " ^
- quote (Syntax.string_of_term ctxt pat))
- else x :: xs)
+ (fn x as Free (s, _) =>
+ (fn xs =>
+ if member op aconv xs x then
+ case_error (quote s ^ " occurs repeatedly in the pattern " ^
+ quote (Syntax.string_of_term ctxt pat))
+ else x :: xs)
| _ => I) pat [];
fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
@@ -225,34 +218,35 @@
fun string_of_clause (pat, rhs) =
Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
val _ = map (no_repeat_vars ctxt o fst) clauses;
- val rows = map_index (fn (i, (pat, rhs)) =>
- (([], [pat]), (rhs, i))) clauses;
+ val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
val rangeT =
- (case distinct op = (map (type_of o snd) clauses) of
+ (case distinct (op =) (map (type_of o snd) clauses) of
[] => case_error "no clauses given"
| [T] => T
| _ => case_error "all cases must have the same result type");
val used' = fold add_row_used rows used;
- val (tags, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
- used' rangeT [x] rows
- handle CASE_ERROR (msg, i) => case_error (msg ^
- (if i < 0 then ""
- else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
+ val (tags, case_tm) =
+ mk_case tab ctxt ty_match ty_inst type_of used' rangeT [x] rows
+ handle CASE_ERROR (msg, i) =>
+ case_error
+ (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
val _ =
(case subtract (op =) tags (map (snd o snd) rows) of
[] => ()
| is =>
- (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
+ (case config of Error => case_error | Warning => warning | Quiet => fn _ => ())
("The following clauses are redundant (covered by preceding clauses):\n" ^
- cat_lines (map (string_of_clause o nth clauses) is)));
+ cat_lines (map (string_of_clause o nth clauses) is)));
in
case_tm
end;
-fun make_case tab ctxt = gen_make_case
- (match_type (Proof_Context.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
-val make_case_untyped = gen_make_case (K (K Vartab.empty))
- (K (Term.map_types (K dummyT))) (K dummyT);
+fun make_case tab ctxt =
+ gen_make_case (match_type (Proof_Context.theory_of ctxt))
+ Envir.subst_term_types fastype_of tab ctxt;
+
+val make_case_untyped =
+ gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT);
(* parse translation *)
@@ -271,21 +265,17 @@
| prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
let val x = singleton (Name.variant_list used) "x"
in (Free (x, T), x :: used) end
- | prep_pat (Const (s, T)) used =
- (Const (intern_const_syntax s, T), used)
+ | prep_pat (Const (s, T)) used = (Const (intern_const_syntax s, T), used)
| prep_pat (v as Free (s, T)) used =
let val s' = Proof_Context.intern_const ctxt s in
- if Sign.declared_const thy s' then
- (Const (s', T), used)
+ if Sign.declared_const thy s' then (Const (s', T), used)
else (v, used)
end
| prep_pat (t $ u) used =
let
val (t', used') = prep_pat t used;
val (u', used'') = prep_pat u used';
- in
- (t' $ u', used'')
- end
+ in (t' $ u', used'') end
| prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
let val (l', cnstrts) = strip_constraints l
@@ -294,10 +284,11 @@
fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
| dest_case2 t = [t];
val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
- val case_tm = make_case_untyped (tab_of thy) ctxt
- (if err then Error else Warning) []
- (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
- (flat cnstrts) t) cases;
+ val case_tm =
+ make_case_untyped (tab_of thy) ctxt
+ (if err then Error else Warning) []
+ (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
+ (flat cnstrts) t) cases;
in case_tm end
| case_tr _ _ _ ts = case_error "case_tr";
@@ -318,17 +309,17 @@
val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
val (xs, ys) = chop i zs;
val u = list_abs (ys, strip_abs_body t);
- val xs' = map Free (Name.variant_list (Misc_Legacy.add_term_names (u, used))
- (map fst xs) ~~ map snd xs)
+ val xs' =
+ map Free
+ (Name.variant_list (Misc_Legacy.add_term_names (u, used)) (map #1 xs) ~~ map #2 xs);
in (xs', subst_bounds (rev xs', u)) end;
fun is_dependent i t =
let val k = length (strip_abs_vars t) - i
in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
fun count_cases (_, _, true) = I
- | count_cases (c, (_, body), false) =
- AList.map_default op aconv (body, []) (cons c);
+ | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c);
val is_undefined = name_of #> equal (SOME @{const_name undefined});
- fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
+ fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body);
in
(case ty_info tab cname of
SOME {constructors, case_name} =>
@@ -337,13 +328,13 @@
val cases = map (fn (Const (s, U), t) =>
let
val k = length (binder_types U);
- val p as (xs, _) = strip_abs k t
+ val p as (xs, _) = strip_abs k t;
in
- (Const (s, map type_of xs ---> type_of x),
- p, is_dependent k t)
+ (Const (s, map type_of xs ---> type_of x), p, is_dependent k t)
end) (constructors ~~ fs);
- val cases' = sort (int_ord o swap o pairself (length o snd))
- (fold_rev count_cases cases []);
+ val cases' =
+ sort (int_ord o swap o pairself (length o snd))
+ (fold_rev count_cases cases []);
val R = type_of t;
val dummy =
if d then Term.dummy_pattern R
@@ -353,17 +344,18 @@
map mk_case
(case find_first (is_undefined o fst) cases' of
SOME (_, cs) =>
- if length cs = length constructors then [hd cases]
- else filter_out (fn (_, (_, body), _) => is_undefined body) cases
- | NONE => case cases' of
- [] => cases
- | (default, cs) :: _ =>
- if length cs = 1 then cases
- else if length cs = length constructors then
- [hd cases, (dummy, ([], default), false)]
- else
- filter_out (fn (c, _, _) => member op aconv cs c) cases @
- [(dummy, ([], default), false)]))
+ if length cs = length constructors then [hd cases]
+ else filter_out (fn (_, (_, body), _) => is_undefined body) cases
+ | NONE =>
+ (case cases' of
+ [] => cases
+ | (default, cs) :: _ =>
+ if length cs = 1 then cases
+ else if length cs = length constructors then
+ [hd cases, (dummy, ([], default), false)]
+ else
+ filter_out (fn (c, _, _) => member op aconv cs c) cases @
+ [(dummy, ([], default), false)])))
end handle CASE_ERROR _ => NONE
else NONE
| _ => NONE)
@@ -390,8 +382,7 @@
fun gen_strip_case dest t =
(case dest [] t of
- SOME (x, clauses) =>
- SOME (x, maps (strip_case'' dest) clauses)
+ SOME (x, clauses) => SOME (x, maps (strip_case'' dest) clauses)
| NONE => NONE);
val strip_case = gen_strip_case oo dest_case;
@@ -411,8 +402,7 @@
| Const (s, _) => Syntax.const (Lexicon.mark_const s)
| t => t) pat $
map_aterms
- (fn x as Free (s, T) =>
- if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
+ (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
| t => t) rhs
end;
in
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Nov 30 21:14:01 2011 +0100
@@ -20,7 +20,8 @@
let
val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
- in if is_some (try (Code.constrset_of_consts thy) cs')
+ in
+ if is_some (try (Code.constrset_of_consts thy) cs')
then SOME cs
else NONE
end;
@@ -30,16 +31,14 @@
fun mk_case_cert thy tyco =
let
- val raw_thms =
- (#case_rewrites o Datatype_Data.the_info thy) tyco;
+ val raw_thms = #case_rewrites (Datatype_Data.the_info thy tyco);
val thms as hd_thm :: _ = raw_thms
|> Conjunction.intr_balanced
|> Thm.unvarify_global
|> Conjunction.elim_balanced (length raw_thms)
|> map Simpdata.mk_meta_eq
- |> map Drule.zero_var_indexes
- val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
- | _ => I) (Thm.prop_of hd_thm) [];
+ |> map Drule.zero_var_indexes;
+ val params = fold_aterms (fn (Free (v, _)) => insert (op =) v | _ => I) (Thm.prop_of hd_thm) [];
val rhs = hd_thm
|> Thm.prop_of
|> Logic.dest_equals
@@ -48,11 +47,11 @@
|> apsnd (fst o split_last)
|> list_comb;
val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
- val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
+ val asm = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
in
thms
|> Conjunction.intr_balanced
- |> Raw_Simplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
+ |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)]
|> Thm.implies_intr asm
|> Thm.generalize ([], params) 0
|> AxClass.unoverload thy
@@ -65,26 +64,30 @@
fun mk_eq_eqns thy tyco =
let
val (vs, cos) = Datatype_Data.the_spec thy tyco;
- val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
+ val {descr, index, inject = inject_thms, distinct = distinct_thms, ...} =
Datatype_Data.the_info thy tyco;
val ty = Type (tyco, map TFree vs);
- fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT)
- $ t1 $ t2;
+ fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT) $ t1 $ t2;
fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
- val triv_injects = map_filter
- (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
- | _ => NONE) cos;
+ val triv_injects =
+ map_filter
+ (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
+ | _ => NONE) cos;
fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
[trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
- val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
+ val distincts =
+ maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
- val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps
- (map Simpdata.mk_eq (@{thm equal} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
- fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+ val simpset =
+ Simplifier.global_context thy
+ (HOL_basic_ss addsimps
+ (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)));
+ fun prove prop =
+ Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
|> Simpdata.mk_eq;
in (map prove (triv_injects @ injects @ distincts), prove refl) end;
@@ -93,26 +96,28 @@
fun add_def tyco lthy =
let
val ty = Type (tyco, map TFree vs);
- fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
- $ Free ("x", ty) $ Free ("y", ty);
- val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
+ fun mk_side const_name =
+ Const (const_name, ty --> ty --> HOLogic.boolT) $ Free ("x", ty) $ Free ("y", ty);
+ val def =
+ HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
val def' = Syntax.check_term lthy def;
- val ((_, (_, thm)), lthy') = Specification.definition
- (NONE, (Attrib.empty_binding, def')) lthy;
+ val ((_, (_, thm)), lthy') =
+ Specification.definition (NONE, (Attrib.empty_binding, def')) lthy;
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy);
val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
- fun tac thms = Class.intro_classes_tac []
- THEN ALLGOALS (Proof_Context.fact_tac thms);
- fun prefix tyco = Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name;
+ fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
+ fun prefix tyco =
+ Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name;
fun add_eq_thms tyco =
Theory.checkpoint
#> `(fn thy => mk_eq_eqns thy tyco)
- #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
+ #-> (fn (thms, thm) =>
+ Global_Theory.note_thmss Thm.lemmaK
[((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
- #> snd
+ #> snd;
in
thy
|> Class.instantiation (tycos, vs, [HOLogic.class_equal])
@@ -128,17 +133,18 @@
fun add_all_code config tycos thy =
let
- val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) tycos;
+ val (vs :: _, coss) = split_list (map (Datatype_Data.the_spec thy) tycos);
val any_css = map2 (mk_constr_consts thy vs) tycos coss;
- val css = if exists is_none any_css then []
- else map_filter I any_css;
+ val css = if exists is_none any_css then [] else map_filter I any_css;
val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
val certs = map (mk_case_cert thy) tycos;
- val tycos_eq = filter_out
- (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
+ val tycos_eq =
+ filter_out
+ (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
in
if null css then thy
- else thy
+ else
+ thy
|> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
|> fold Code.add_datatype css
|> fold_rev Code.add_default_eqn case_rewrites
--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 30 21:14:01 2011 +0100
@@ -72,24 +72,24 @@
let
val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
in
- case body_type T of
+ (case body_type T of
Type (tyco, _) => AList.lookup (op =) tab tyco
- | _ => NONE
+ | _ => NONE)
end;
fun info_of_constr_permissive thy (c, T) =
let
- val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
- val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
- val default =
- if null tab then NONE
- else SOME (snd (List.last tab))
- (*conservative wrt. overloaded constructors*);
- in case hint
- of NONE => default
- | SOME tyco => case AList.lookup (op =) tab tyco
- of NONE => default (*permissive*)
- | SOME info => SOME info
+ val tab = Symtab.lookup_list (#constrs (DatatypesData.get thy)) c;
+ val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE);
+ val default = if null tab then NONE else SOME (snd (List.last tab));
+ (*conservative wrt. overloaded constructors*)
+ in
+ (case hint of
+ NONE => default
+ | SOME tyco =>
+ (case AList.lookup (op =) tab tyco of
+ NONE => default (*permissive*)
+ | SOME info => SOME info))
end;
val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
@@ -112,10 +112,9 @@
let
val { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
- val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
- o Datatype_Aux.dest_DtTFree) dtys;
- val cos = map
- (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos;
+ val sorts =
+ map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v)) o Datatype_Aux.dest_DtTFree) dtys;
+ val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos;
in (sorts, cos) end;
fun the_descr thy (raw_tycos as raw_tyco :: _) =
@@ -124,27 +123,30 @@
val descr = #descr info;
val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
- val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
- o Datatype_Aux.dest_DtTFree) dtys;
+ val vs =
+ map ((fn v => (v, the (AList.lookup (op =) (#sorts info) v))) o Datatype_Aux.dest_DtTFree)
+ dtys;
fun is_DtTFree (Datatype_Aux.DtTFree _) = true
- | is_DtTFree _ = false
+ | is_DtTFree _ = false;
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
val protoTs as (dataTs, _) =
chop k descr
|> (pairself o map)
(fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
-
+
val tycos = map fst dataTs;
val _ =
if eq_set (op =) (tycos, raw_tycos) then ()
- else error ("Type constructors " ^ commas_quote raw_tycos ^
- " do not belong exhaustively to one mutual recursive datatype");
+ else
+ error ("Type constructors " ^ commas_quote raw_tycos ^
+ " do not belong exhaustively to one mutual recursive datatype");
val (Ts, Us) = (pairself o map) Type protoTs;
val names = map Long_Name.base_name (the_default tycos (#alt_names info));
- val (auxnames, _) = Name.make_context names
+ val (auxnames, _) =
+ Name.make_context names
|> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us;
val prefix = space_implode "_" names;
@@ -158,16 +160,16 @@
in map_filter (Option.map #distinct o get_info thy) tycos end;
fun get_constrs thy dtco =
- case try (the_spec thy) dtco
- of SOME (sorts, cos) =>
- let
- fun subst (v, sort) = TVar ((v, 0), sort);
- fun subst_ty (TFree v) = subst v
- | subst_ty ty = ty;
- val dty = Type (dtco, map subst sorts);
- fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
- in SOME (map mk_co cos) end
- | NONE => NONE;
+ (case try (the_spec thy) dtco of
+ SOME (sorts, cos) =>
+ let
+ fun subst (v, sort) = TVar ((v, 0), sort);
+ fun subst_ty (TFree v) = subst v
+ | subst_ty ty = ty;
+ val dty = Type (dtco, map subst sorts);
+ fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
+ in SOME (map mk_co cos) end
+ | NONE => NONE);
@@ -188,9 +190,9 @@
handle TYPE (msg, _, _) => error msg;
val sorts' = Term.add_tfreesT T sorts;
val _ =
- case duplicates (op =) (map fst sorts') of
+ (case duplicates (op =) (map fst sorts') of
[] => ()
- | dups => error ("Inconsistent sort constraints for " ^ commas dups)
+ | dups => error ("Inconsistent sort constraints for " ^ commas dups));
in (T, sorts') end;
@@ -226,17 +228,17 @@
(* translation rules for case *)
-fun make_case ctxt = Datatype_Case.make_case
- (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt;
+fun make_case ctxt =
+ Datatype_Case.make_case (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt;
-fun strip_case ctxt = Datatype_Case.strip_case
- (info_of_case (Proof_Context.theory_of ctxt));
+fun strip_case ctxt =
+ Datatype_Case.strip_case (info_of_case (Proof_Context.theory_of ctxt));
fun add_case_tr' case_names thy =
Sign.add_advanced_trfuns ([], [],
map (fn case_name =>
- let val case_name' = Lexicon.mark_const case_name
- in (case_name', Datatype_Case.case_tr' info_of_case case_name')
+ let val case_name' = Lexicon.mark_const case_name in
+ (case_name', Datatype_Case.case_tr' info_of_case case_name')
end) case_names, []) thy;
val trfun_setup =
@@ -276,7 +278,10 @@
(** abstract theory extensions relative to a datatype characterisation **)
structure Datatype_Interpretation = Interpretation
- (type T = Datatype_Aux.config * string list val eq: T * T -> bool = eq_snd op =);
+(
+ type T = Datatype_Aux.config * string list;
+ val eq: T * T -> bool = eq_snd (op =);
+);
fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
@@ -313,22 +318,28 @@
Datatype_Aux.message config
("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
- val (exhaust, thy3) = Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
- descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
- val (nchotomys, thy4) = Datatype_Abs_Proofs.prove_nchotomys config new_type_names
- descr sorts exhaust thy3;
- val ((rec_names, rec_rewrites), thy5) = Datatype_Abs_Proofs.prove_primrec_thms
- config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
- inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr sorts))
- induct thy4;
- val ((case_rewrites, case_names), thy6) = Datatype_Abs_Proofs.prove_case_thms
- config new_type_names descr sorts rec_names rec_rewrites thy5;
- val (case_congs, thy7) = Datatype_Abs_Proofs.prove_case_congs new_type_names
- descr sorts nchotomys case_rewrites thy6;
- val (weak_case_congs, thy8) = Datatype_Abs_Proofs.prove_weak_case_congs new_type_names
- descr sorts thy7;
- val (splits, thy9) = Datatype_Abs_Proofs.prove_split_thms
- config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
+ val (exhaust, thy3) =
+ Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
+ descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
+ val (nchotomys, thy4) =
+ Datatype_Abs_Proofs.prove_nchotomys config new_type_names
+ descr sorts exhaust thy3;
+ val ((rec_names, rec_rewrites), thy5) =
+ Datatype_Abs_Proofs.prove_primrec_thms
+ config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
+ inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr sorts))
+ induct thy4;
+ val ((case_rewrites, case_names), thy6) =
+ Datatype_Abs_Proofs.prove_case_thms
+ config new_type_names descr sorts rec_names rec_rewrites thy5;
+ val (case_congs, thy7) =
+ Datatype_Abs_Proofs.prove_case_congs new_type_names
+ descr sorts nchotomys case_rewrites thy6;
+ val (weak_case_congs, thy8) =
+ Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr sorts thy7;
+ val (splits, thy9) =
+ Datatype_Abs_Proofs.prove_split_thms
+ config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
val dt_infos = map_index
@@ -406,7 +417,8 @@
val _ = if length frees <> length vs then no_constr cT else ();
in (tyco, (vs, cT)) end;
- val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
+ val raw_cs =
+ AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
val _ =
(case map_filter (fn (tyco, _) =>
if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs of
@@ -417,22 +429,25 @@
(case distinct (op =) (map length raw_vss) of
[n] => 0 upto n - 1
| _ => error "Different types in given constructors");
- fun inter_sort m = map (fn xs => nth xs m) raw_vss
- |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
+ fun inter_sort m =
+ map (fn xs => nth xs m) raw_vss
+ |> foldr1 (Sorts.inter_sort (Sign.classes_of thy));
val sorts = map inter_sort ms;
val vs = Name.invent_names Name.context Name.aT sorts;
- fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
- (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
+ fun norm_constr (raw_vs, (c, T)) =
+ (c, map_atyps
+ (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
val cs = map (apsnd (map norm_constr)) raw_cs;
val dtyps_of_typ =
map (Datatype_Aux.dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
val dt_names = map fst cs;
- fun mk_spec (i, (tyco, constr)) = (i, (tyco,
- map (Datatype_Aux.DtTFree o fst) vs,
- (map o apsnd) dtyps_of_typ constr))
+ fun mk_spec (i, (tyco, constr)) =
+ (i, (tyco,
+ map (Datatype_Aux.DtTFree o fst) vs,
+ (map o apsnd) dtyps_of_typ constr));
val descr = map_index mk_spec cs;
val injs = Datatype_Prop.make_injs [descr] vs;
val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs);
@@ -445,7 +460,7 @@
unflat rules (map Drule.zero_var_indexes_list raw_thms);
(*FIXME somehow dubious*)
in
- Proof_Context.background_theory_result
+ Proof_Context.background_theory_result (* FIXME !? *)
(prove_rep_datatype config dt_names alt_names descr vs
raw_inject half_distinct raw_induct)
#-> after_qed
@@ -477,7 +492,7 @@
(Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") --
Scan.repeat1 Parse.term
>> (fn (alt_names, ts) =>
- Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
+ Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
open Datatype_Aux;
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Nov 30 21:14:01 2011 +0100
@@ -39,7 +39,10 @@
let
fun index (x :: xs) tab =
(case AList.lookup (op =) tab x of
- NONE => if member (op =) xs x then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
+ NONE =>
+ if member (op =) xs x
+ then (x ^ "1") :: index xs ((x, 2) :: tab)
+ else x :: index xs tab
| SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
| index [] _ = [];
in index names [] end;
@@ -59,7 +62,8 @@
let
val descr' = flat descr;
fun make_inj T (cname, cargs) =
- if null cargs then I else
+ if null cargs then I
+ else
let
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val constr_t = Const (cname, Ts ---> T);
@@ -85,25 +89,23 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
- fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
+ fun prep_constr (cname, cargs) =
+ (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
fun make_distincts' _ [] = []
- | make_distincts' T ((cname, cargs)::constrs) =
+ | make_distincts' T ((cname, cargs) :: constrs) =
let
val frees = map Free ((make_tnames cargs) ~~ cargs);
val t = list_comb (Const (cname, cargs ---> T), frees);
fun make_distincts'' (cname', cargs') =
let
- val frees' = map Free ((map ((op ^) o (rpair "'"))
- (make_tnames cargs')) ~~ cargs');
- val t' = list_comb (Const (cname', cargs' ---> T), frees')
+ val frees' = map Free (map (suffix "'") (make_tnames cargs') ~~ cargs');
+ val t' = list_comb (Const (cname', cargs' ---> T), frees');
in
HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t'))
- end
-
+ end;
in map make_distincts'' constrs @ make_distincts' T constrs end;
-
in
map2 (fn ((_, (_, _, constrs))) => fn T =>
(length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs
@@ -142,18 +144,20 @@
val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
-
- in list_all_free (frees, Logic.list_implies (prems,
- HOLogic.mk_Trueprop (make_pred k T $
- list_comb (Const (cname, Ts ---> T), map Free frees))))
+ in
+ list_all_free (frees,
+ Logic.list_implies (prems,
+ HOLogic.mk_Trueprop (make_pred k T $
+ list_comb (Const (cname, Ts ---> T), map Free frees))))
end;
- val prems = maps (fn ((i, (_, _, constrs)), T) =>
- map (make_ind_prem i T) constrs) (descr' ~~ recTs);
+ val prems =
+ maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = make_tnames recTs;
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
- (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
- (descr' ~~ recTs ~~ tnames)))
+ val concl =
+ HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
+ (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
+ (descr' ~~ recTs ~~ tnames)));
in Logic.list_implies (prems, concl) end;
@@ -167,16 +171,17 @@
let
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
- val free_ts = map Free frees
- in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
- (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
- HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
+ val free_ts = map Free frees;
+ in
+ list_all_free (frees,
+ Logic.mk_implies (HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
+ HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
end;
fun make_casedist ((_, (_, _, constrs))) T =
let val prems = map (make_casedist_prem T) constrs
- in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
- end
+ in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))) end;
in
map2 make_casedist (hd descr)
@@ -189,8 +194,10 @@
let
val descr' = flat descr;
- val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~
- replicate (length descr') HOLogic.typeS);
+ val rec_result_Ts =
+ map TFree
+ (Name.variant_list used (replicate (length descr') "'t") ~~
+ replicate (length descr') HOLogic.typeS);
val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -214,19 +221,20 @@
val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
- val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
- (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
+ val rec_fns =
+ map (uncurry (Datatype_Aux.mk_Free "f"))
+ (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
- val reccomb_names = map (Sign.intern_const thy)
- (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, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
+ val reccomb_names =
+ map (Sign.intern_const thy)
+ (if length descr' = 1 then [big_reccomb_name]
+ else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto (length descr'))));
+ val reccombs =
+ map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
(reccomb_names ~~ recTs ~~ rec_result_Ts);
- fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =
+ fun make_primrec T comb_t (cname, cargs) (ts, f :: fs) =
let
val recs = filter Datatype_Aux.is_rec_type cargs;
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
@@ -242,13 +250,13 @@
nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
end;
- val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
+ val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees');
- in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
- (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
- list_comb (f, frees @ reccombs')))], fs)
+ in
+ (ts @ [HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
+ list_comb (f, frees @ reccombs')))], fs)
end;
-
in
fold (fn ((dt, T), comb_t) => fold (make_primrec T comb_t) (#3 (snd dt)))
(descr' ~~ recTs ~~ reccombs) ([], rec_fns)
@@ -270,8 +278,7 @@
let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs
in Ts ---> T' end) constrs) (hd descr);
- val case_names = map (fn s =>
- Sign.intern_const thy (s ^ "_case")) new_type_names
+ val case_names = map (fn s => Sign.intern_const thy (s ^ "_case")) new_type_names;
in
map (fn ((name, Ts), T) => list_comb
(Const (name, Ts @ [T] ---> T'),
@@ -290,15 +297,16 @@
fun make_case T comb_t ((cname, cargs), f) =
let
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
- val frees = map Free ((make_tnames Ts) ~~ Ts)
- in HOLogic.mk_Trueprop (HOLogic.mk_eq
- (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
- list_comb (f, frees)))
- end
-
- in map (fn (((_, (_, _, constrs)), T), comb_t) =>
- map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
- ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
+ val frees = map Free ((make_tnames Ts) ~~ Ts);
+ in
+ HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
+ list_comb (f, frees)))
+ end;
+ in
+ map (fn (((_, (_, _, constrs)), T), comb_t) =>
+ map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
+ ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
end;
@@ -316,30 +324,31 @@
fun make_split (((_, (_, _, constrs)), T), comb_t) =
let
val (_, fs) = strip_comb comb_t;
- val used = ["P", "x"] @ (map (fst o dest_Free) fs);
+ val used = ["P", "x"] @ map (fst o dest_Free) fs;
fun process_constr ((cname, cargs), f) (t1s, t2s) =
let
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
- val eqn = HOLogic.mk_eq (Free ("x", T),
- list_comb (Const (cname, Ts ---> T), frees));
- val P' = P $ list_comb (f, frees)
- in (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees
- (HOLogic.imp $ eqn $ P') :: t1s,
- fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees
- (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)
+ val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees));
+ val P' = P $ list_comb (f, frees);
+ in
+ (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees
+ (HOLogic.imp $ eqn $ P') :: t1s,
+ fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees
+ (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)
end;
val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
- val lhs = P $ (comb_t $ Free ("x", T))
+ val lhs = P $ (comb_t $ Free ("x", T));
in
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Datatype_Aux.mk_conj t1s)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Datatype_Aux.mk_disj t2s)))
end
- in map make_split ((hd descr) ~~ newTs ~~
- (make_case_combs new_type_names descr sorts thy "f"))
+ in
+ map make_split
+ ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
end;
(************************* additional rules for TFL ***************************)
@@ -349,26 +358,26 @@
val case_combs = make_case_combs new_type_names descr sorts thy "f";
fun mk_case_cong comb =
- let
+ let
val Type ("fun", [T, _]) = fastype_of comb;
val M = Free ("M", T);
val M' = Free ("M'", T);
in
Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')),
HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M')))
- end
+ end;
in
map mk_case_cong case_combs
end;
-
+
(*---------------------------------------------------------------------------
* Structure of case congruence theorem looks like this:
*
- * (M = M')
- * ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk))
- * ==> ...
- * ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = gn x1..xj))
+ * (M = M')
+ * ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk))
+ * ==> ...
+ * ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = gn x1..xj))
* ==>
* (ty_case f1..fn M = ty_case g1..gn M')
*---------------------------------------------------------------------------*)
@@ -398,14 +407,12 @@
(HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
- end
-
+ end;
in
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) ::
map mk_clause (fs ~~ gs ~~ constrs),
HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb' $ M')))
- end
-
+ end;
in
map mk_case_cong (case_combs ~~ case_combs' ~~ hd descr)
end;
@@ -431,10 +438,11 @@
fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
(HOLogic.mk_eq (Free ("v", T),
list_comb (Const (cname, Ts ---> T), map Free frees)))
- end
-
- in map (fn ((_, (_, _, constrs)), T) =>
- HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
+ end;
+ in
+ map (fn ((_, (_, _, constrs)), T) =>
+ HOLogic.mk_Trueprop
+ (HOLogic.mk_all ("v", T, Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
(hd descr ~~ newTs)
end;
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Nov 30 19:18:17 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Nov 30 21:14:01 2011 +0100
@@ -28,12 +28,13 @@
fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
let
val recTs = Datatype_Aux.get_rec_types descr sorts;
- val pnames = if length descr = 1 then ["P"]
+ val pnames =
+ if length descr = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
val rec_result_Ts = map (fn ((i, _), P) =>
- if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
- (descr ~~ pnames);
+ if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
+ (descr ~~ pnames);
fun make_pred i T U r x =
if member (op =) is i then
@@ -56,10 +57,12 @@
val rT = nth (rec_result_Ts) i;
val vs' = filter_out is_unit vs;
val f = Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
- val f' = Envir.eta_contract (fold_rev (absfree o dest_Free) vs
- (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
- in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
- (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
+ val f' =
+ Envir.eta_contract (fold_rev (absfree o dest_Free) vs
+ (if member (op =) is i then list_comb (f, vs') else HOLogic.unit));
+ in
+ (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
+ (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
end
| mk_prems vs (((dt, s), T) :: ds) =
let
@@ -68,19 +71,20 @@
val i = length Us;
val rT = nth (rec_result_Ts) k;
val r = Free ("r" ^ s, Us ---> rT);
- val (p, f) = mk_prems (vs @ [r]) ds
- in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
- (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
- (make_pred k rT U (Datatype_Aux.app_bnds r i)
- (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
- end
-
+ val (p, f) = mk_prems (vs @ [r]) ds;
+ in
+ (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
+ (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
+ (make_pred k rT U (Datatype_Aux.app_bnds r i)
+ (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
+ end;
in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
constrs) (descr ~~ recTs) 1)));
fun mk_proj j [] t = t
- | mk_proj j (i :: is) t = if null is then t else
- if (j: int) = i then HOLogic.mk_fst t
+ | mk_proj j (i :: is) t =
+ if null is then t
+ else if (j: int) = i then HOLogic.mk_fst t
else mk_proj j is (HOLogic.mk_snd t);
val tnames = Datatype_Prop.make_tnames recTs;
@@ -88,28 +92,32 @@
val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
(descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
- val r = if null is then Extraction.nullt else
- foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
- if member (op =) is i then SOME
- (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
- else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
- (map (fn ((((i, _), T), U), tname) =>
- make_pred i U T (mk_proj i is r) (Free (tname, T)))
- (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
+ val r =
+ if null is then Extraction.nullt
+ else
+ foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
+ if member (op =) is i then SOME
+ (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
+ else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
+ val concl =
+ HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
+ (map (fn ((((i, _), T), U), tname) =>
+ make_pred i U T (mk_proj i is r) (Free (tname, T)))
+ (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
val cert = cterm_of thy;
val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
- val thm = Goal.prove_internal (map cert prems) (cert concl)
- (fn prems =>
- EVERY [
- rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
- rtac (cterm_instantiate inst induct) 1,
- ALLGOALS Object_Logic.atomize_prems_tac,
- rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
- REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
- REPEAT (etac allE i) THEN atac i)) 1)])
+ val thm =
+ Goal.prove_internal (map cert prems) (cert concl)
+ (fn prems =>
+ EVERY [
+ rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
+ rtac (cterm_instantiate inst induct) 1,
+ ALLGOALS Object_Logic.atomize_prems_tac,
+ rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
+ REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
+ REPEAT (etac allE i) THEN atac i)) 1)])
|> Drule.export_without_context;
val ind_name = Thm.derivation_name induct;
@@ -122,29 +130,29 @@
val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
- val ivs1 = map Var (filter_out (fn (_, T) =>
- @{type_name bool} = tname_of (body_type T)) ivs);
+ val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
val prf =
Extraction.abs_corr_shyps thy' induct vs ivs2
(fold_rev (fn (f, p) => fn prf =>
- (case head_of (strip_abs_body f) of
- Free (s, T) =>
- let val T' = Logic.varifyT_global T
- in Abst (s, SOME T', Proofterm.prf_abstract_over
- (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
- end
- | _ => AbsP ("H", SOME p, prf)))
- (rec_fns ~~ prems_of thm)
- (Proofterm.proof_combP
- (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+ (case head_of (strip_abs_body f) of
+ Free (s, T) =>
+ let val T' = Logic.varifyT_global T in
+ Abst (s, SOME T', Proofterm.prf_abstract_over
+ (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
+ end
+ | _ => AbsP ("H", SOME p, prf)))
+ (rec_fns ~~ prems_of thm)
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
- else Logic.varify_global (fold_rev lambda
- (map Logic.unvarify_global ivs1 @ filter_out is_unit
- (map (head_of o strip_abs_body) rec_fns)) r);
+ else
+ Logic.varify_global (fold_rev lambda
+ (map Logic.unvarify_global ivs1 @ filter_out is_unit
+ (map (head_of o strip_abs_body) rec_fns)) r);
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
@@ -162,10 +170,11 @@
val frees = Name.variant_list ["P", "y"] (Datatype_Prop.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
- in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
- (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
- HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
- list_comb (r, free_ts)))))
+ in
+ (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
+ HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
+ list_comb (r, free_ts)))))
end;
val SOME (_, _, constrs) = AList.lookup (op =) descr index;
@@ -176,14 +185,15 @@
val y = Var (("y", 0), Logic.varifyT_global T);
val y' = Free ("y", T);
- val thm = Goal.prove_internal (map cert prems)
- (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
- (fn prems =>
- EVERY [
- rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
- ALLGOALS (EVERY'
- [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
- resolve_tac prems, asm_simp_tac HOL_basic_ss])])
+ val thm =
+ Goal.prove_internal (map cert prems)
+ (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
+ (fn prems =>
+ EVERY [
+ rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
+ ALLGOALS (EVERY'
+ [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
+ resolve_tac prems, asm_simp_tac HOL_basic_ss])])
|> Drule.export_without_context;
val exh_name = Thm.derivation_name exhaust;
@@ -193,22 +203,25 @@
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
- val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
- (fold_rev (fn (p, r) => fn prf =>
- Proofterm.forall_intr_proof' (Logic.varify_global r)
- (AbsP ("H", SOME (Logic.varify_global p), prf)))
- (prems ~~ rs)
- (Proofterm.proof_combP
- (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
- val prf' = Extraction.abs_corr_shyps thy' exhaust []
- (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
- val r' = Logic.varify_global (Abs ("y", T,
- list_abs (map dest_Free rs, list_comb (r,
- map Bound ((length rs - 1 downto 0) @ [length rs])))));
-
- in Extraction.add_realizers_i
- [(exh_name, (["P"], r', prf)),
- (exh_name, ([], Extraction.nullt, prf'))] thy'
+ val prf =
+ Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
+ (fold_rev (fn (p, r) => fn prf =>
+ Proofterm.forall_intr_proof' (Logic.varify_global r)
+ (AbsP ("H", SOME (Logic.varify_global p), prf)))
+ (prems ~~ rs)
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+ val prf' =
+ Extraction.abs_corr_shyps thy' exhaust []
+ (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
+ val r' =
+ Logic.varify_global (Abs ("y", T,
+ list_abs (map dest_Free rs, list_comb (r,
+ map Bound ((length rs - 1 downto 0) @ [length rs])))));
+ in
+ Extraction.add_realizers_i
+ [(exh_name, (["P"], r', prf)),
+ (exh_name, ([], Extraction.nullt, prf'))] thy'
end;
fun add_dt_realizers config names thy =