isabelle: src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML@487427a02bee (annotated)

49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	1	(* Title: HOL/Codatatype/Tools/bnf_sugar_tactics.ML
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	3	Copyright 2012
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	4
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	5	Tactics for sugar on top of a BNF.
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	6	*)
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	7
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	8	signature BNF_SUGAR_TACTICS =
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	9	sig
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	10	val mk_nchotomy_tac: int -> thm -> tactic
49028 487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	11	val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	12	val mk_other_half_disc_disjoint_tac: thm -> tactic
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	13	end;
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	14
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	15	structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	16	struct
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	17
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	18	open BNF_FP_Util
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	19
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	20	fun mk_nchotomy_tac n exhaust =
f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	21	(rtac allI THEN' rtac exhaust THEN'
49022 005ce926a932 define selectors and discriminators blanchet parents: 49020 diff changeset	22	EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	23
49028 487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	24	fun mk_half_disc_disjoint_tac m disc_def disc'_thm =
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	25	(dtac (disc_def RS iffD1) THEN'
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	26	REPEAT_DETERM_N m o etac exE THEN'
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	27	hyp_subst_tac THEN'
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	28	rtac disc'_thm) 1;
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	29
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	30	fun mk_other_half_disc_disjoint_tac half_thm =
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	31	(etac @{thm contrapos_pn} THEN' etac half_thm) 1;
487427a02bee generate "disc_distinct" theorems blanchet parents: 49022 diff changeset	32
49020 f379cf5d71bd more work on BNF sugar -- up to derivation of nchotomy blanchet parents: diff changeset	33	end;

author	blanchet
	Thu, 30 Aug 2012 13:42:05 +0200
changeset 49028	487427a02bee
parent 49022	005ce926a932
child 49029	f0ecfa9575a9
permissions	-rw-r--r--