# HG changeset patch # User wenzelm # Date 1322684041 -3600 # Node ID 9dcbf6a1829cc818bf3fc36b6aadfe255333e3d7 # Parent 3e006216319f0f562a8e0bdd61d3061f111076b5 misc tuning; diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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; diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype_aux.ML --- 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; diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype_case.ML --- 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 diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype_codegen.ML --- 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 diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype_data.ML --- 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; diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype_prop.ML --- 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; diff -r 3e006216319f -r 9dcbf6a1829c src/HOL/Tools/Datatype/datatype_realizer.ML --- 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 =