equal
deleted
inserted
replaced
137 by (cut_inst_tac [("evs","evs")] lemma 1); |
137 by (cut_inst_tac [("evs","evs")] lemma 1); |
138 by (cut_inst_tac [("evs","evs'")] lemma 1); |
138 by (cut_inst_tac [("evs","evs'")] lemma 1); |
139 by (Clarify_tac 1); |
139 by (Clarify_tac 1); |
140 by (res_inst_tac [("x","N")] exI 1); |
140 by (res_inst_tac [("x","N")] exI 1); |
141 by (res_inst_tac [("x","Suc (N+Na)")] exI 1); |
141 by (res_inst_tac [("x","Suc (N+Na)")] exI 1); |
142 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add2, le_add1, |
142 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2, |
143 le_eq_less_Suc RS sym]) 1); |
143 less_Suc_eq_le]) 1); |
144 qed "Nonce_supply2"; |
144 qed "Nonce_supply2"; |
145 |
145 |
146 Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \ |
146 Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \ |
147 \ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''"; |
147 \ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''"; |
148 by (cut_inst_tac [("evs","evs")] lemma 1); |
148 by (cut_inst_tac [("evs","evs")] lemma 1); |
150 by (cut_inst_tac [("evs","evs''")] lemma 1); |
150 by (cut_inst_tac [("evs","evs''")] lemma 1); |
151 by (Clarify_tac 1); |
151 by (Clarify_tac 1); |
152 by (res_inst_tac [("x","N")] exI 1); |
152 by (res_inst_tac [("x","N")] exI 1); |
153 by (res_inst_tac [("x","Suc (N+Na)")] exI 1); |
153 by (res_inst_tac [("x","Suc (N+Na)")] exI 1); |
154 by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1); |
154 by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1); |
155 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add2, le_add1, |
155 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2, |
156 le_eq_less_Suc RS sym]) 1); |
156 less_Suc_eq_le]) 1); |
157 qed "Nonce_supply3"; |
157 qed "Nonce_supply3"; |
158 |
158 |
159 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; |
159 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; |
160 by (rtac (lemma RS exE) 1); |
160 by (rtac (lemma RS exE) 1); |
161 by (rtac selectI 1); |
161 by (rtac selectI 1); |