nominal2: IntEx.thy@d9151fa76f84 (annotated)

181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory IntEx
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports QuotMain
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	fun
281 46e6d06efe3f Experiments with lifting partially applied constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 276 diff changeset	6	intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	"intrel (x, y) (u, v) = (x + v = u + y)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	quotient my_int = "nat \<times> nat" / intrel
529 6348c2a57ec2 More name changes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 506 diff changeset	11	apply(unfold equivp_def)
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	apply(auto simp add: mem_def expand_fun_eq)
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	done
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	14
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	15	thm quotient_thm
91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	16
529 6348c2a57ec2 More name changes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 506 diff changeset	17	thm my_int_equivp
321 f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv Christian Urban <urbanc@in.tum.de> parents: 320 diff changeset	18
239 02b14a21761a Cleaning of the interface to lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 228 diff changeset	19	print_theorems
274 df225aa45770 simplified the quotient_def code Christian Urban <urbanc@in.tum.de> parents: 268 diff changeset	20	print_quotients
239 02b14a21761a Cleaning of the interface to lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 228 diff changeset	21
268 4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	22	quotient_def
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	23	ZERO::"my_int"
df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	24	where
df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	25	"ZERO \<equiv> (0::nat, 0::nat)"
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	27	ML {* print_qconstinfo @{context} *}
746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	28
268 4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	29	term ZERO
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	30	thm ZERO_def
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	31
290 a0be84b0c707 removed typing information from get_fun in quotient_def; potentially dangerous Christian Urban <urbanc@in.tum.de> parents: 286 diff changeset	32	ML {* prop_of @{thm ZERO_def} *}
a0be84b0c707 removed typing information from get_fun in quotient_def; potentially dangerous Christian Urban <urbanc@in.tum.de> parents: 286 diff changeset	33
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	34	ML {* separate *}
746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	35
268 4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	36	quotient_def
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	37	ONE::"my_int"
193 b888119a18ff merged Christian Urban <urbanc@in.tum.de> parents: 192 diff changeset	38	where
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	39	"ONE \<equiv> (1::nat, 0::nat)"
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	41	ML {* print_qconstinfo @{context} *}
746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	42
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	term ONE
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	thm ONE_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	45
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	"my_plus (x, y) (u, v) = (x + u, y + v)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	50
268 4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	51	quotient_def
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	52	PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	53	where
275 34ad627ac5d5 fixed definition of PLUS Christian Urban <urbanc@in.tum.de> parents: 274 diff changeset	54	"PLUS \<equiv> my_plus"
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	55
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	56	term my_plus
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	term PLUS
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	thm PLUS_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	59
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	"my_neg (x, y) = (y, x)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	64
268 4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	65	quotient_def
220 af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	66	NEG::"my_int \<Rightarrow> my_int"
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	67	where
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	68	"NEG \<equiv> my_neg"
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	69
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	term NEG
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	thm NEG_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	72
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	"MINUS z w = PLUS z (NEG w)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	77
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	"my_mult (x, y) (u, v) = (xu + yv, xv + yu)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	82
268 4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	83	quotient_def
220 af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	84	MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	85	where
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	86	"MULT \<equiv> my_mult"
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	87
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	term MULT
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	thm MULT_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	90
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	92	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	"my_le (x, y) (u, v) = (x+v \<le> u+y)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	96
268 4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	97	quotient_def
220 af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	98	LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	99	where
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	100	"LE \<equiv> my_le"
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	101
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	term LE
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	thm LE_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	104
321 f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv Christian Urban <urbanc@in.tum.de> parents: 320 diff changeset	105
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	106	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	108	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	"LESS z w = (LE z w \<and> z \<noteq> w)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	110
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	term LESS
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	112	thm LESS_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	113
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	114	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	ABS :: "my_int \<Rightarrow> my_int"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	"ABS i = (if (LESS i ZERO) then (NEG i) else i)"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	118
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	119	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	SIGN :: "my_int \<Rightarrow> my_int"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	121	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	"SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	123
310 fec6301a1989 added a container for quotient constants (does not work yet though) Christian Urban <urbanc@in.tum.de> parents: 306 diff changeset	124	ML {* print_qconstinfo @{context} *}
fec6301a1989 added a container for quotient constants (does not work yet though) Christian Urban <urbanc@in.tum.de> parents: 306 diff changeset	125
199 d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	126	lemma plus_sym_pre:
281 46e6d06efe3f Experiments with lifting partially applied constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 276 diff changeset	127	shows "my_plus a b \<approx> my_plus b a"
199 d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	128	apply(cases a)
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	129	apply(cases b)
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	130	apply(auto)
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	131	done
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	132
549 f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	133	lemma list_equiv_rsp[quotient_rsp]:
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	134	shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	135	by auto
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	136
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	137	lemma ho_plus_rsp[quotient_rsp]:
450 2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	138	shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	139	by (simp)
192 a296bf1a3b09 Simplifying code in int Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 191 diff changeset	140
a296bf1a3b09 Simplifying code in int Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 191 diff changeset	141	ML {* val qty = @{typ "my_int"} *}
239 02b14a21761a Cleaning of the interface to lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 228 diff changeset	142	ML {* val ty_name = "my_int" *}
458 44a70e69ef92 Code cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 455 diff changeset	143	ML {* val rsp_thms = @{thms ho_plus_rsp} *}
377 edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	144	ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	145	ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
197 c0f2db9a243b Further reordering in Int code. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 196 diff changeset	146
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	147	ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	148
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	149	ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	150	ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	151
552 d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	152	lemma test1: "my_plus a b = my_plus a b"
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	153	apply(rule refl)
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	154	done
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	155
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	156	lemma "PLUS a b = PLUS a b"
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	157	apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	158	apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	159	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	160	(* does not work yet *)
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	161	oops
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	162
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	163	lemma test2: "my_plus a = my_plus a"
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	164	apply(rule refl)
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	165	done
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	166
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	167	lemma "PLUS a = PLUS a"
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	168	apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	169	(* does not work yet *)
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	170	oops
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	171
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	172	lemma test3: "my_plus = my_plus"
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	173	apply(rule refl)
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	174	done
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	175
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	176	lemma "PLUS = PLUS"
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	177	apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	178	apply(rule ho_plus_rsp)
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	179	(* does not work yet *)
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	180	oops
d9151fa76f84 added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet Christian Urban <urbanc@in.tum.de> parents: 549 diff changeset	181
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	182
377 edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	183	lemma "PLUS a b = PLUS b a"
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	184	apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
432 9c33c0809733 Finished and tested the new regularize Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 423 diff changeset	185	apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
549 f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	186	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	187	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	188	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
445 f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	189	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	190	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	191	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	192	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	193	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	194	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	195	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	196	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	197	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	198	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	199	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	200	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	201	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	202	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	203	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	204	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	205	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	206	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	207	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	208	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	209	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	210	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	211	apply(tactic {* inj_repabs_tac_intex @{context} 1*})
549 f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	212	apply(tactic {* clean_tac @{context} 1 *})
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	213	done
342 eb15be678ac4 lift_thm with a goal. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 340 diff changeset	214
198 ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	215	lemma plus_assoc_pre:
281 46e6d06efe3f Experiments with lifting partially applied constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 276 diff changeset	216	shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
198 ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	217	apply (cases i)
ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	218	apply (cases j)
ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	219	apply (cases k)
224 f9a25fe22037 Cleaning the unnecessary theorems in 'IntEx'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 222 diff changeset	220	apply (simp)
198 ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	221	done
ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	222
377 edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	223	lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	224	apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
432 9c33c0809733 Finished and tested the new regularize Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 423 diff changeset	225	apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
445 f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	226	apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	227	apply(tactic {* clean_tac @{context} 1 *})
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	228	done
354 2eb6d527dfe4 addded a tactic, which sets up the three goals of the `algorithm' Christian Urban <urbanc@in.tum.de> parents: 347 diff changeset	229
379 57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	230	lemma ho_tst: "foldl my_plus x [] = x"
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	231	apply simp
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	232	done
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	233
485 4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	234	(* I believe it's true. *)
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	235	lemma foldl_rsp[quotient_rsp]:
537 57073b0b8fac Even more name changes and cleaning Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 536 diff changeset	236	"((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl"
536 44fa9df44e6f More code cleaning and name changes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 529 diff changeset	237	apply (simp only: fun_rel.simps)
485 4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	238	apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	239	apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	240	apply (rule impI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	241	apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	242	apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	243	apply (rule impI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	244	apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	245	apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	246	apply (rule impI)
489 2b7b349e470f deleted now obsolete argument rty everywhere Christian Urban <urbanc@in.tum.de> parents: 485 diff changeset	247	apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
414 4dad34ca50db Minor cleaning Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 409 diff changeset	248	sorry
4dad34ca50db Minor cleaning Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 409 diff changeset	249
379 57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	250	lemma "foldl PLUS x [] = x"
445 f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	251	apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	252	apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	253	apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
540 c0b13fb70d6d More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 537 diff changeset	254	apply(rule nil_rsp)
c0b13fb70d6d More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 537 diff changeset	255	apply(tactic {* quotient_tac @{context} 1*})
549 f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	256	apply(simp only: fun_map.simps id_simps)
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	257	apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	258	apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
529 6348c2a57ec2 More name changes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 506 diff changeset	259	apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	260	apply(tactic {* clean_tac @{context} 1 *})
549 f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	261	sorry
359 64c3c83e0ed4 New cleaning tactic Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 358 diff changeset	262
485 4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	263	lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	264	sorry
327 22c8bf90cadb tried to prove the repabs_inj lemma, but failed for the moment Christian Urban <urbanc@in.tum.de> parents: 326 diff changeset	265
485 4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	266	lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	267	apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	268	apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	269	apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
540 c0b13fb70d6d More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 537 diff changeset	270	apply(rule cons_rsp)
c0b13fb70d6d More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 537 diff changeset	271	apply(tactic {* quotient_tac @{context} 1 *})
549 f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	272	apply(simp only: fun_map.simps id_simps)
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	273	apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
f178958d3d81 not yet quite functional treatment of constants Christian Urban <urbanc@in.tum.de> parents: 540 diff changeset	274	apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
529 6348c2a57ec2 More name changes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 506 diff changeset	275	apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
6348c2a57ec2 More name changes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 506 diff changeset	276	apply(simp only: cons_prs[OF Quotient_my_int])
506 91c374abde06 removed quot argument...not all examples work anymore Christian Urban <urbanc@in.tum.de> parents: 505 diff changeset	277	apply(tactic {* clean_tac @{context} 1 *})
485 4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	278	done
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 466 diff changeset	279

author	Christian Urban <urbanc@in.tum.de>
	Sat, 05 Dec 2009 13:49:35 +0100 (2009-12-05)
changeset 552	d9151fa76f84
parent 549	f178958d3d81
child 553	09cd71fac4ec
permissions	-rw-r--r--