equal
deleted
inserted
replaced
67 lemma Sigma_Suc1: |
67 lemma Sigma_Suc1: |
68 "m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)"; |
68 "m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)"; |
69 by (simp add: below_def less_Suc_eq) blast; |
69 by (simp add: below_def less_Suc_eq) blast; |
70 |
70 |
71 lemma Sigma_Suc2: |
71 lemma Sigma_Suc2: |
72 "m = n + 2 ==> A <*> below m = (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"; |
72 "m = n + 2 ==> A <*> below m = |
|
73 (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"; |
73 by (auto simp add: below_def) arith; |
74 by (auto simp add: below_def) arith; |
74 |
75 |
75 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2; |
76 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2; |
76 |
77 |
77 |
78 |
110 |
111 |
111 |
112 |
112 subsection {* Dominoes *}; |
113 subsection {* Dominoes *}; |
113 |
114 |
114 consts |
115 consts |
115 domino :: "(nat * nat) set set"; |
116 domino :: "(nat * nat) set set"; |
116 |
117 |
117 inductive domino |
118 inductive domino |
118 intros |
119 intros |
119 horiz: "{(i, j), (i, j + 1)} : domino" |
120 horiz: "{(i, j), (i, j + 1)} : domino" |
120 vertl: "{(i, j), (i + 1, j)} : domino"; |
121 vertl: "{(i, j), (i + 1, j)} : domino"; |