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

33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	1	theory Predicate_Compile_Alternative_Defs
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	2	imports "../Predicate_Compile"
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
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	7	declare Collect_def[code_pred_inline]
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	8	declare mem_def[code_pred_inline]
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	9
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	10	declare eq_reflection[OF empty_def, code_pred_inline]
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	11	declare insert_code[code_pred_def]
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	12	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	13	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	14
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	15
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	16
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	17	section {* Alternative list definitions *}
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	18
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	19	subsection {* Alternative rules for set *}
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	20
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	21	lemma set_ConsI1 [code_pred_intro]:
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	22	"set (x # xs) x"
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	23	unfolding mem_def[symmetric, of _ x]
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	24	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	25
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	26	lemma set_ConsI2 [code_pred_intro]:
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	27	"set xs x ==> set (x' # xs) x"
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	28	unfolding mem_def[symmetric, of _ x]
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	29	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	30
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	31	code_pred [skip_proof] set
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	32	proof -
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	33	case set
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	34	from this show thesis
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	35	apply (case_tac xb)
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	36	apply auto
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	37	unfolding mem_def[symmetric, of _ xc]
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	38	apply auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	39	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	40	apply fastsimp
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	41	done
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	42	qed
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	43
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	44	subsection {* Alternative rules for list_all2 *}
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	45
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	46	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	47	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	48
33628 ed2111a5c3ed renaming code_pred_intros to code_pred_intro bulwahn parents: 33623 diff changeset	49	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	50	by auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	51
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	52	code_pred [skip_proof] list_all2
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	53	proof -
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	54	case list_all2
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	55	from this show thesis
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	56	apply -
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	57	apply (case_tac xa)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	58	apply (case_tac xb)
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	59	apply auto
34948 2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck bulwahn parents: 33628 diff changeset	60	apply (case_tac xb)
33150 75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	61	apply auto
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	62	done
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	63	qed
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	64
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	65
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	66
75eddea4abef further changes due to the previous merge in the predicate compiler bulwahn parents: diff changeset	67	end

author	wenzelm
	Sun, 07 Feb 2010 19:54:12 +0100
changeset 35022	c844b93dd147
parent 34948	2d5f2a9f7601
child 35324	c9f428269b38
permissions	-rw-r--r--