equal
deleted
inserted
replaced
|
1 (* Title: HOL/Library/SCT_Interpretation.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
1 theory SCT_Interpretation |
6 theory SCT_Interpretation |
2 imports Main SCT_Misc SCT_Definition |
7 imports Main SCT_Misc SCT_Definition |
3 begin |
8 begin |
4 |
|
5 |
9 |
6 definition |
10 definition |
7 "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))" |
11 "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))" |
8 |
12 |
9 lemma not_acc_smaller: |
13 lemma not_acc_smaller: |
407 ultimately have False |
411 ultimately have False |
408 by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp |
412 by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp |
409 thus "acc R x" .. |
413 thus "acc R x" .. |
410 qed |
414 qed |
411 |
415 |
412 |
|
413 end |
416 end |