nominal2: IntEx.thy@2dc708ddb93a (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
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	apply(unfold EQUIV_def)
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
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	15	thm my_int_equiv
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	16
239 02b14a21761a Cleaning of the interface to lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 228 diff changeset	17	print_theorems
274 df225aa45770 simplified the quotient_def code Christian Urban <urbanc@in.tum.de> parents: 268 diff changeset	18	print_quotients
239 02b14a21761a Cleaning of the interface to lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 228 diff changeset	19
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	20	quotient_def
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	21	ZERO::"my_int"
df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	22	where
df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	23	"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	24
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	25	ML {* print_qconstinfo @{context} *}
746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	26
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	27	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	28	thm ZERO_def
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
290 a0be84b0c707 removed typing information from get_fun in quotient_def; potentially dangerous Christian Urban <urbanc@in.tum.de> parents: 286 diff changeset	30	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	31
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	32	ML {* separate *}
746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	33
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	34	quotient_def
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	35	ONE::"my_int"
193 b888119a18ff merged Christian Urban <urbanc@in.tum.de> parents: 192 diff changeset	36	where
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	37	"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	38
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	39	ML {* print_qconstinfo @{context} *}
746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	40
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	term ONE
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	thm ONE_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	43
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	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	46	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	"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	48
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	49	quotient_def
218 df05cd030d2f added infrastructure for defining lifted constants Christian Urban <urbanc@in.tum.de> parents: 210 diff changeset	50	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	51	where
275 34ad627ac5d5 fixed definition of PLUS Christian Urban <urbanc@in.tum.de> parents: 274 diff changeset	52	"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	53
318 746b17e1d6d8 fixed the storage of qconst definitions Christian Urban <urbanc@in.tum.de> parents: 312 diff changeset	54	term my_plus
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	term PLUS
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	thm PLUS_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	57
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	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	60	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	"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	62
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	63	quotient_def
220 af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	64	NEG::"my_int \<Rightarrow> my_int"
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	65	where
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	66	"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	67
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	term NEG
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	thm NEG_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	70
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	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	73	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	"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	75
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	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	78	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	"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	80
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	81	quotient_def
220 af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	82	MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	83	where
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	84	"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	85
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	term MULT
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	thm MULT_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	88
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	(* 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	90	fun
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	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	92	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	"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	94
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	95	quotient_def
220 af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	96	LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	97	where
af951c8fb80a updated all definitions Christian Urban <urbanc@in.tum.de> parents: 218 diff changeset	98	"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	99
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	term LE
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	101	thm LE_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	102
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	103
181 3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	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	106	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	"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	108
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	term LESS
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	thm LESS_def
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	111
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	112	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	113	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	114	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	"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	116
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	definition
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	118	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	119	where
3e53081ad53a added another example file about integers (see HOL/Int.thy) Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	"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	121
310 fec6301a1989 added a container for quotient constants (does not work yet though) Christian Urban <urbanc@in.tum.de> parents: 306 diff changeset	122	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	123
199 d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	124	lemma plus_sym_pre:
281 46e6d06efe3f Experiments with lifting partially applied constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 276 diff changeset	125	shows "my_plus a b \<approx> my_plus b a"
199 d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	126	apply(cases a)
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	127	apply(cases b)
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	128	apply(auto)
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	129	done
d6bf4234c7f6 merged Christian Urban <urbanc@in.tum.de> parents: 198 diff changeset	130
450 2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	131	lemma ho_plus_rsp[quot_rsp]:
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	132	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	133	by (simp)
192 a296bf1a3b09 Simplifying code in int Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 191 diff changeset	134
a296bf1a3b09 Simplifying code in int Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 191 diff changeset	135	ML {* val qty = @{typ "my_int"} *}
239 02b14a21761a Cleaning of the interface to lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 228 diff changeset	136	ML {* val ty_name = "my_int" *}
192 a296bf1a3b09 Simplifying code in int Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 191 diff changeset	137	ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
260 59578f428bbe Fixes after optimization and preparing for a general FORALL_PRS Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 239 diff changeset	138	ML {* val defs = @{thms PLUS_def} *}
377 edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	139	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	140	ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	141	ML {* val consts = lookup_quot_consts defs *}
197 c0f2db9a243b Further reordering in Int code. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 196 diff changeset	142
450 2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	143	ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	144
450 2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	145	ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	146	ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [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	147
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	148
377 edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	149	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	150	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	151	apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
423 2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	152	prefer 2
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	153	ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	154	ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	155	apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
445 f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	156	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	157	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	158	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	159	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	160	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	161	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	162	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	163	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	164	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	165	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	166	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	167	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	168	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	169	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	170	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	171	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	172	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	173	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	174	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	175	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	176	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	177	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	178	apply(tactic {* inj_repabs_tac_intex @{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	179	done
342 eb15be678ac4 lift_thm with a goal. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 340 diff changeset	180
198 ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	181	lemma plus_assoc_pre:
281 46e6d06efe3f Experiments with lifting partially applied constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 276 diff changeset	182	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	183	apply (cases i)
ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	184	apply (cases j)
ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	185	apply (cases k)
224 f9a25fe22037 Cleaning the unnecessary theorems in 'IntEx'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 222 diff changeset	186	apply (simp)
198 ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	187	done
ff4425e000db Completely cleaned Int. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 197 diff changeset	188
377 edd71fd83a2d cleaning in MyInt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 374 diff changeset	189	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	190	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	191	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	192	apply(tactic {* all_inj_repabs_tac_intex @{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	193	ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	194	ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	195	apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	196	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	197
379 57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	198	lemma ho_tst: "foldl my_plus x [] = x"
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	199	apply simp
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	200	done
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	201
450 2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	202	(* FIXME/TODO: is this a respectfulness theorem? Does not look like one. *)
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	203	lemma map_prs:
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	204	"map REP_my_int (map ABS_my_int x) = x"
414 4dad34ca50db Minor cleaning Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 409 diff changeset	205	sorry
4dad34ca50db Minor cleaning Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 409 diff changeset	206
450 2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	207	lemma foldl_prs[quot_rsp]:
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] Christian Urban <urbanc@in.tum.de> parents: 446 diff changeset	208	"((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
416 3f3927f793d4 Removing arguments of tactics: absrep, rel_refl, reps_same are computed. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 414 diff changeset	209	sorry
3f3927f793d4 Removing arguments of tactics: absrep, rel_refl, reps_same are computed. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 414 diff changeset	210
379 57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	211	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	212	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	213	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	214	apply(tactic {* all_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	215	apply(simp add: map_prs)
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	216	ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac Christian Urban <urbanc@in.tum.de> parents: 433 diff changeset	217	ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *}
379 57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	218	sorry
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	219
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	220	(*
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	221	FIXME: All below is your construction code; mostly commented out as it
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	222	does not work.
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	223	*)
57bde65f6eb2 Removed unused things from QuotMain. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 377 diff changeset	224
362 7a3d86050e72 added a prepare_tac Christian Urban <urbanc@in.tum.de> parents: 360 diff changeset	225	lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
406 f32237ef18a6 deleted obsolete qenv code Christian Urban <urbanc@in.tum.de> parents: 405 diff changeset	226	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	227	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	228	apply(tactic {* all_inj_repabs_tac_intex @{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	229	ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	230	ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	231	apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC Christian Urban <urbanc@in.tum.de> parents: 419 diff changeset	232	done
359 64c3c83e0ed4 New cleaning tactic Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 358 diff changeset	233
327 22c8bf90cadb tried to prove the repabs_inj lemma, but failed for the moment Christian Urban <urbanc@in.tum.de> parents: 326 diff changeset	234

author	Christian Urban <urbanc@in.tum.de>
	Sun, 29 Nov 2009 03:59:18 +0100
changeset 450	2dc708ddb93a
parent 446	84ee3973f083
child 451	586e3dc4afdb
permissions	-rw-r--r--