--- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy Mon Sep 22 10:55:51 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy Mon Sep 22 15:01:27 2014 +0200
@@ -26,6 +26,16 @@
codatatype ('b, 'c :: ord, 'd, 'e) some_passive =
SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
+codatatype 'a multi_live_direct1 = MultiLiveDirect1 'a
+codatatype 'a multi_live_direct2 = MultiLiveDirect2 'a 'a
+codatatype 'a multi_live_direct3 = MultiLiveDirect3 'a 'a 'a
+codatatype 'a multi_live_direct4 = MultiLiveDirect4 'a 'a 'a 'a
+codatatype 'a multi_live_direct5 = MultiLiveDirect5 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct6 = MultiLiveDirect6 'a 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct7 = MultiLiveDirect7 'a 'a 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
+codatatype 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
+
codatatype lambda =
Var string |
App lambda lambda |
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy Mon Sep 22 10:55:51 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy Mon Sep 22 15:01:27 2014 +0200
@@ -24,6 +24,16 @@
datatype (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
+datatype (discs_sels) 'a multi_live_direct1 = MultiLiveDirect1 'a
+datatype (discs_sels) 'a multi_live_direct2 = MultiLiveDirect2 'a 'a
+datatype (discs_sels) 'a multi_live_direct3 = MultiLiveDirect3 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct4 = MultiLiveDirect4 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct5 = MultiLiveDirect5 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct6 = MultiLiveDirect6 'a 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct7 = MultiLiveDirect7 'a 'a 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a
+datatype (discs_sels) 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a
+
datatype (discs_sels) hfset = HFset "hfset fset"
datatype (discs_sels) lambda =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Sep 22 10:55:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Sep 22 15:01:27 2014 +0200
@@ -365,7 +365,12 @@
fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
Abs_pre_inverses =
let
- val assms_ctor_defs = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms;
+ val assms_tac =
+ let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in
+ fold (curry (op ORELSE')) (map (fn thm =>
+ funpow (length (prems_of thm)) (fn tac => tac THEN' atac) (rtac thm)) assms')
+ (etac FalseE)
+ end;
val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
|> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
in
@@ -377,12 +382,8 @@
unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
@{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
Un_empty_right empty_iff singleton_iff}) THEN
- REPEAT_DETERM (HEADGOAL
- (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
- REPEAT_DETERM o eresolve_tac @{thms UN_E UnE singletonE} THEN'
- fold (curry (op ORELSE')) (map (fn thm =>
- funpow (length (prems_of thm)) (fn tac => tac THEN' atac) (rtac thm)) assms_ctor_defs)
- (etac FalseE)))
+ REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE' eresolve_tac @{thms UN_E UnE singletonE} ORELSE'
+ assms_tac))
end;
end;