nominal2: IntEx2.thy@6a031829319a (annotated)

568 0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory IntEx2
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports QuotMain
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	uses
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	("Tools/numeral.ML")
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	("Tools/numeral_syntax.ML")
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	("Tools/int_arith.ML")
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	begin
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	fun
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	"intrel (x, y) (u, v) = (x + v = u + y)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	13
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	quotient int = "nat \<times> nat" / intrel
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	apply(unfold equivp_def)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	apply(auto simp add: mem_def expand_fun_eq)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	done
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	begin
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	quotient_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	zero_qnt::"int"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	"zero_qnt \<equiv> (0::nat, 0::nat)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	definition Zero_int_def[code del]:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	"0 = zero_qnt"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	quotient_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	one_qnt::"int"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	"one_qnt \<equiv> (1::nat, 0::nat)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	34
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	definition One_int_def[code del]:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	"1 = one_qnt"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	37
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	fun
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	"plus_raw (x, y) (u, v) = (x + u, y + v)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	42
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	quotient_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	"plus_qnt \<equiv> plus_raw"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	47
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	definition add_int_def[code del]:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	"z + w = plus_qnt z w"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	50
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	fun
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	"minus_raw (x, y) = (y, x)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	55
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	quotient_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	minus_qnt::"int \<Rightarrow> int"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	"minus_qnt \<equiv> minus_raw"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	60
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	definition minus_int_def [code del]:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	"- z = minus_qnt z"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	63
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	definition
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	65	diff_int_def [code del]: "z - w = z + (-w::int)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	66
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	fun
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	"mult_raw (x, y) (u, v) = (xu + yv, xv + yu)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	71
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	quotient_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	"mult_qnt \<equiv> mult_raw"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	76
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	definition
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	mult_int_def [code del]: "z * w = mult_qnt z w"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	79
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	fun
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	"le_raw (x, y) (u, v) = (x+v \<le> u+y)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	84
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	quotient_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	where
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	"le_qnt \<equiv> le_raw"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	89
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	90	definition
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	le_int_def [code del]:
570 6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	92	"z \<le> w = le_qnt z w"
568 0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	93
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	definition
570 6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	95	less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
568 0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	96
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	definition
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	98	zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	99
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	definition
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	101	zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	102
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	instance ..
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	104
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	end
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	106
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	thm add_assoc
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	108
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	lemma plus_raw_rsp[quotient_rsp]:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	by auto
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	112
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	113	lemma mult_raw_rsp[quotient_rsp]:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	114	shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	apply(auto)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	apply(simp add: mult algebra_simps)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	118
570 6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	119	lemma le_raw_rsp[quotient_rsp]:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	120	shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	121	by auto
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	122
568 0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	lemma plus_assoc_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	124	shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	125	by (cases i, cases j, cases k) (simp)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	126
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	lemma plus_sym_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	shows "plus_raw i j \<approx> plus_raw j i"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	by (cases i, cases j) (simp)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	130
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	lemma plus_zero_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	shows "plus_raw (0, 0) i \<approx> i"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	133	by (cases i) (simp)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	134
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	135	lemma plus_minus_zero_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	136	shows "plus_raw (minus_raw i) i \<approx> (0, 0)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	137	by (cases i) (simp)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	138
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	lemma mult_assoc_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	by (cases i, cases j, cases k)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	(simp add: mult algebra_simps)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	143
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	144	lemma mult_sym_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	shows "mult_raw i j \<approx> mult_raw j i"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	by (cases i, cases j) (simp)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	147
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	148	lemma mult_one_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	149	shows "mult_raw (1, 0) i \<approx> i"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	by (cases i) (simp)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	151
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	lemma mult_plus_comm_raw:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	154	by (cases i, cases j, cases k)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	(simp add: mult algebra_simps)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	156
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	lemma one_zero_distinct:
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	158	shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	159	by simp
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	160
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	161	text{The integers form a @{text comm_ring_1}}
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	162
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	163
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	164	ML {* val qty = @{typ "int"} *}
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	165	ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	166	ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	167
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	168	instance int :: comm_ring_1
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	169	proof
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	170	fix i j k :: int
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	171	show "(i + j) + k = i + (j + k)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	172	unfolding add_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	173	apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	174	done
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	175	show "i + j = j + i"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	176	unfolding add_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	177	apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	178	done
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	179	show "0 + i = (i::int)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	180	unfolding add_int_def Zero_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	181	apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	182	apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	183	apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	184	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	185	apply(tactic {* clean_tac @{context} 1*})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	186	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	187	show "- i + i = 0"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	188	unfolding add_int_def minus_int_def Zero_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	189	apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	190	apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	191	apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	192	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	193	apply(tactic {* clean_tac @{context} 1*})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	194	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	195	show "i - j = i + - j"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	196	by (simp add: diff_int_def)
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	197	show "(i * j) * k = i * (j * k)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	198	unfolding mult_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	199	apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	200	apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	201	apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	202	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	203	apply(tactic {* clean_tac @{context} 1*})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	204	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	205	show "i * j = j * i"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	206	unfolding mult_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	207	apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	208	apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	209	apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	210	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	211	apply(tactic {* clean_tac @{context} 1*})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	212	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	213	show "1 * i = i"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	214	unfolding mult_int_def One_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	215	apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	216	apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	218	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	219	apply(tactic {* clean_tac @{context} 1*})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	220	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	221	show "(i + j) * k = i * k + j * k"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	222	unfolding mult_int_def add_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	223	apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	224	apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	225	apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	226	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	227	apply(tactic {* clean_tac @{context} 1*})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	228	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	229	show "0 \<noteq> (1::int)"
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	230	unfolding Zero_int_def One_int_def
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	231	apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	232	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	233	defer
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	234	apply(tactic {* clean_tac @{context} 1*})
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	235	sorry
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	236	qed
0384e039b7f2 added new example for Ints; regularise does not work in all instances Christian Urban <urbanc@in.tum.de> parents: diff changeset	237
570 6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	238	term of_nat
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	239	thm of_nat_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	240
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	241	lemma int_def: "of_nat m = ABS_int (m, 0)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	242	apply(induct m)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	243	apply(simp add: Zero_int_def zero_qnt_def)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	244	apply(simp)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	245	apply(simp add: add_int_def One_int_def)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	246	apply(simp add: plus_qnt_def one_qnt_def)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	247	oops
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	248
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	249	lemma le_antisym_raw:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	250	shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	251	by (cases i, cases j) (simp)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	252
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	253	lemma le_refl_raw:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	254	shows "le_raw i i"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	255	by (cases i) (simp)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	256
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	257	lemma le_trans_raw:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	258	shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	259	by (cases i, cases j, cases k) (simp)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	260
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	261	lemma le_cases_raw:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	262	shows "le_raw i j \<or> le_raw j i"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	263	by (cases i, cases j)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	264	(simp add: linorder_linear)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	265
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	266	instance int :: linorder
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	267	proof
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	268	fix i j k :: int
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	269	show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	270	unfolding le_int_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	271	apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	272	done
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	273	show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	274	by (auto simp add: less_int_def dest: antisym)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	275	show "i \<le> i"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	276	unfolding le_int_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	277	apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	278	done
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	279	show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	280	unfolding le_int_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	281	apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	282	done
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	283	show "i \<le> j \<or> j \<le> i"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	284	unfolding le_int_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	285	apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	286	done
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	287	qed
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	288
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	289	instantiation int :: distrib_lattice
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	290	begin
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	291
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	292	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	293	"(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	294
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	295	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	296	"(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	297
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	298	instance
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	299	by intro_classes
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	300	(auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	301
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	302	end
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	303
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	304	lemma le_plus_raw:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	305	shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	306	by (cases i, cases j, cases k) (simp)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	307
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	308
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	309	instance int :: pordered_cancel_ab_semigroup_add
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	310	proof
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	311	fix i j k :: int
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	312	show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	313	unfolding le_int_def add_int_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	314	apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	315	done
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	316	qed
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	317
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	318	lemma test:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	319	"\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	320	\<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	321	apply(cases i, cases j, cases k)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	322	apply(auto simp add: mult algebra_simps)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	323	sorry
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	324
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	325
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	326	text{The integers form an ordered integral domain}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	327	instance int :: ordered_idom
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	328	proof
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	329	fix i j k :: int
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	330	show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	331	unfolding mult_int_def le_int_def less_int_def Zero_int_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	332	apply(tactic {* procedure_tac @{context} @{thm test} 1 *})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	333	defer
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	334	apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	335	defer
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	336	apply(tactic {* clean_tac @{context} 1*})
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	337	sorry
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	338	show "\<bar>i\<bar> = (if i < 0 then -i else i)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	339	by (simp only: zabs_def)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	340	show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	341	by (simp only: zsgn_def)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	342	qed
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	343
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	344	instance int :: lordered_ring
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	345	proof
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	346	fix k :: int
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	347	show "abs k = sup k (- k)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	348	by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	349	qed
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	350
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	351	lemmas int_distrib =
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	352	left_distrib [of "z1::int" "z2" "w", standard]
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	353	right_distrib [of "w::int" "z1" "z2", standard]
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	354	left_diff_distrib [of "z1::int" "z2" "w", standard]
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	355	right_diff_distrib [of "w::int" "z1" "z2", standard]
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	356
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	357
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	358	subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	359
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	360	(*
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	361	context ring_1
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	362	begin
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	363
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	364
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	365	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	366	of_int :: "int \<Rightarrow> 'a"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	367	where
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	368	"of_int
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	369	*)
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	370
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	371
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	372	subsection {* Binary representation *}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	373
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	374	text {*
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	375	This formalization defines binary arithmetic in terms of the integers
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	376	rather than using a datatype. This avoids multiple representations (leading
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	377	zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	378	int_of_binary}, for the numerical interpretation.
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	379
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	380	The representation expects that @{text "(m mod 2)"} is 0 or 1,
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	381	even if m is negative;
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	382	For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	383	@{text "-5 = (-3)*2 + 1"}.
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	384
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	385	This two's complement binary representation derives from the paper
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	386	"An Efficient Representation of Arithmetic for Term Rewriting" by
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	387	Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	388	Springer LNCS 488 (240-251), 1991.
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	389	*}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	390
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	391	subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	392
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	393	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	394	Pls :: int where
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	395	[code del]: "Pls = 0"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	396
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	397	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	398	Min :: int where
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	399	[code del]: "Min = - 1"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	400
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	401	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	402	Bit0 :: "int \<Rightarrow> int" where
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	403	[code del]: "Bit0 k = k + k"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	404
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	405	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	406	Bit1 :: "int \<Rightarrow> int" where
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	407	[code del]: "Bit1 k = 1 + k + k"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	408
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	409	class number = -- {* for numeric types: nat, int, real, \dots *}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	410	fixes number_of :: "int \<Rightarrow> 'a"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	411
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	412	use "~~/src/HOL/Tools/numeral.ML"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	413
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	414	syntax
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	415	"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	416
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	417	use "~~/src/HOL/Tools/numeral_syntax.ML"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	418	setup NumeralSyntax.setup
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	419
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	420	abbreviation
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	421	"Numeral0 \<equiv> number_of Pls"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	422
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	423	abbreviation
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	424	"Numeral1 \<equiv> number_of (Bit1 Pls)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	425
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	426	lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	427	-- {* Unfold all @{text let}s involving constants *}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	428	unfolding Let_def ..
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	429
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	430	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	431	succ :: "int \<Rightarrow> int" where
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	432	[code del]: "succ k = k + 1"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	433
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	434	definition
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	435	pred :: "int \<Rightarrow> int" where
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	436	[code del]: "pred k = k - 1"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	437
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	438	lemmas
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	439	max_number_of [simp] = max_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	440	[of "number_of u" "number_of v", standard, simp]
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	441	and
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	442	min_number_of [simp] = min_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	443	[of "number_of u" "number_of v", standard, simp]
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	444	-- {* unfolding @{text minx} and @{text max} on numerals *}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	445
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	446	lemmas numeral_simps =
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	447	succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	448
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	449	text {* Removal of leading zeroes *}
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	450
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	451	lemma Bit0_Pls [simp, code_post]:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	452	"Bit0 Pls = Pls"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	453	unfolding numeral_simps by simp
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	454
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	455	lemma Bit1_Min [simp, code_post]:
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	456	"Bit1 Min = Min"
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	457	unfolding numeral_simps by simp
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	458
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	459	lemmas normalize_bin_simps =
6a031829319a added more to IntEx2 Christian Urban <urbanc@in.tum.de> parents: 568 diff changeset	460	Bit0_Pls Bit1_Min

author	Christian Urban <urbanc@in.tum.de>
	Sun, 06 Dec 2009 01:43:46 +0100
changeset 570	6a031829319a
parent 568	0384e039b7f2
child 578	070161f1996a
child 579	eac2662a21ec
permissions	-rw-r--r--