equal
deleted
inserted
replaced
17 inductive IT |
17 inductive IT |
18 intros |
18 intros |
19 Var: "rs : lists IT ==> Var n $$ rs : IT" |
19 Var: "rs : lists IT ==> Var n $$ rs : IT" |
20 Lambda: "r : IT ==> Abs r : IT" |
20 Lambda: "r : IT ==> Abs r : IT" |
21 Beta: "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT" |
21 Beta: "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT" |
22 monos lists_mono (* FIXME move to HOL!? *) |
|
23 |
22 |
24 |
23 |
25 text {* Every term in IT terminates. *} |
24 text {* Every term in IT terminates. *} |
26 |
25 |
27 lemma double_induction_lemma [rulify]: |
26 lemma double_induction_lemma [rulify]: |
32 apply (rule allI) |
31 apply (rule allI) |
33 apply (rule impI) |
32 apply (rule impI) |
34 apply (erule acc_induct) |
33 apply (erule acc_induct) |
35 apply clarify |
34 apply clarify |
36 apply (rule accI) |
35 apply (rule accI) |
37 apply (tactic {* safe_tac (claset () addSEs [thm "apps_betasE"]) *}) -- FIXME |
36 apply (safe elim!: apps_betasE) |
38 apply assumption |
37 apply assumption |
39 apply (blast intro: subst_preserves_beta apps_preserves_beta) |
38 apply (blast intro: subst_preserves_beta apps_preserves_beta) |
40 apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI |
39 apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI |
41 dest: acc_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) |
40 dest: acc_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) |
42 apply (blast dest: apps_preserves_betas) |
41 apply (blast dest: apps_preserves_betas) |