isabelle: src/HOL/ex/Predicate_Compile_Alternative_Defs.thy@8bfe94730530 (annotated)

33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	1	theory Predicate_Compile_Alternative_Defs
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: 33150 diff changeset	2	imports Main
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	3	begin
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	4
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	5	section {* Set operations *}
33623 4ec42d38224f changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned bulwahn parents: 33326 diff changeset	6
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	7	declare eq_reflection[OF empty_def, code_pred_inline]
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	8	declare eq_reflection[OF Un_def, code_pred_inline]
33623 4ec42d38224f changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned bulwahn parents: 33326 diff changeset	9	declare eq_reflection[OF UNION_def, code_pred_inline]
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	10
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	11	section {* Alternative list definitions *}
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	12
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	13	subsection {* Alternative rules for set *}
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	14
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	15	lemma set_ConsI1 [code_pred_intro]:
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	16	"set (x # xs) x"
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	17	unfolding mem_def[symmetric, of _ x]
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	18	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	19
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	20	lemma set_ConsI2 [code_pred_intro]:
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	21	"set xs x ==> set (x' # xs) x"
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	22	unfolding mem_def[symmetric, of _ x]
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	23	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	24
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	25	code_pred set
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	26	proof -
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	27	case set
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	28	from this show thesis
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	29	apply (case_tac a1)
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	30	apply auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	31	unfolding mem_def[symmetric, of _ a2]
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	32	apply auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	33	unfolding mem_def
33326 7d0288d90535 improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler bulwahn parents: 33250 diff changeset	34	apply fastsimp
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	35	done
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	36	qed
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	37
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	38	subsection {* Alternative rules for list_all2 *}
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	39
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	40	lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	41	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	42
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	43	lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	44	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	45
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	46	code_pred list_all2
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	47	proof -
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	48	case list_all2
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	49	from this show thesis
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	50	apply -
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	51	apply (case_tac a1)
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	52	apply (case_tac a2)
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	53	apply auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	54	apply (case_tac a2)
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	55	apply auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	56	done
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	57	qed
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	58
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	59
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	60
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	61	end

author	blanchet
	Tue, 17 Nov 2009 18:24:43 +0100
changeset 33739	8bfe94730530
parent 33628	ed2111a5c3ed
child 34948	2d5f2a9f7601
permissions	-rw-r--r--