src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 33317 b4534348b8fd
equal deleted inserted replaced
32956:c39860141415 32957:675c0c7e6a37
   166 val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
   166 val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
   167 val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
   167 val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
   168 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
   168 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
   169 val abs_defin' = iso_locale RS iso_abs_defin';
   169 val abs_defin' = iso_locale RS iso_abs_defin';
   170 val rep_defin' = iso_locale RS iso_rep_defin';
   170 val rep_defin' = iso_locale RS iso_rep_defin';
   171 val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
   171 val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
   172 
   172 
   173 (* ----- generating beta reduction rules from definitions-------------------- *)
   173 (* ----- generating beta reduction rules from definitions-------------------- *)
   174 
   174 
   175 val _ = trace " Proving beta reduction rules...";
   175 val _ = trace " Proving beta reduction rules...";
   176 
   176 
   249 in
   249 in
   250   val _ = trace " Proving exhaust...";
   250   val _ = trace " Proving exhaust...";
   251   val exhaust = pg con_appls (mk_trp exh) (K tacs);
   251   val exhaust = pg con_appls (mk_trp exh) (K tacs);
   252   val _ = trace " Proving casedist...";
   252   val _ = trace " Proving casedist...";
   253   val casedist =
   253   val casedist =
   254     standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   254     Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   255 end;
   255 end;
   256 
   256 
   257 local 
   257 local 
   258   fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
   258   fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
   259   fun bound_fun i _ = Bound (length cons - i);
   259   fun bound_fun i _ = Bound (length cons - i);
   540     fun distincts []      = []
   540     fun distincts []      = []
   541       | distincts ((c,leqs)::cs) =
   541       | distincts ((c,leqs)::cs) =
   542         flat
   542         flat
   543           (ListPair.map (distinct c) ((map #1 cs),leqs)) @
   543           (ListPair.map (distinct c) ((map #1 cs),leqs)) @
   544         distincts cs;
   544         distincts cs;
   545   in map standard (distincts (cons ~~ distincts_le)) end;
   545   in map Drule.standard (distincts (cons ~~ distincts_le)) end;
   546 
   546 
   547 local 
   547 local 
   548   fun pgterm rel con args =
   548   fun pgterm rel con args =
   549     let
   549     let
   550       fun append s = upd_vname (fn v => v^s);
   550       fun append s = upd_vname (fn v => v^s);
   736         asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
   736         asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
   737         TRY (safe_tac HOL_cs) ::
   737         TRY (safe_tac HOL_cs) ::
   738         maps (eq_tacs ctxt) eqs;
   738         maps (eq_tacs ctxt) eqs;
   739     in pg copy_take_defs goal tacs end;
   739     in pg copy_take_defs goal tacs end;
   740 in
   740 in
   741   val take_rews = map standard
   741   val take_rews = map Drule.standard
   742     (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
   742     (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
   743 end; (* local *)
   743 end; (* local *)
   744 
   744 
   745 local
   745 local
   746   fun one_con p (con,args) =
   746   fun one_con p (con,args) =