41 by (blast_tac (claset() addIs [double_induction_lemma]) 1); |
41 by (blast_tac (claset() addIs [double_induction_lemma]) 1); |
42 qed "IT_implies_termi"; |
42 qed "IT_implies_termi"; |
43 |
43 |
44 (*** Every terminating term is in IT ***) |
44 (*** Every terminating term is in IT ***) |
45 |
45 |
46 val IT_cases = map (IT.mk_cases |
46 Addsimps [Var_apps_neq_Abs_apps RS not_sym]; |
47 ([Var_apps_eq_Var_apps_conv, Abs_eq_apps_conv, apps_eq_Abs_conv, |
47 |
48 Abs_apps_eq_Abs_apps_conv, |
48 Goal "Var n $$ ss ~= Abs r $ s $$ ts"; |
49 Var_apps_neq_Abs_apps, Var_apps_neq_Abs_apps RS not_sym, |
49 by (simp_tac (simpset() addsimps [foldl_Cons RS sym] |
50 hd(tl(get_thms List.thy "foldl.simps")) RS sym ] |
50 delsimps [foldl_Cons]) 1); |
51 @ dB.simps @ list.simps)) |
51 qed "Var_apps_neq_Abs_app_apps"; |
52 ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"]; |
52 Addsimps [Var_apps_neq_Abs_app_apps, |
|
53 Var_apps_neq_Abs_app_apps RS not_sym]; |
|
54 |
|
55 |
|
56 Goal "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' & s=s' & ss=ss')"; |
|
57 by (simp_tac (simpset() addsimps [foldl_Cons RS sym] |
|
58 delsimps [foldl_Cons]) 1); |
|
59 qed "Abs_apps_eq_Abs_app_apps"; |
|
60 Addsimps [Abs_apps_eq_Abs_app_apps]; |
|
61 |
|
62 val IT_cases = |
|
63 map IT.mk_cases |
|
64 ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"]; |
53 AddSEs IT_cases; |
65 AddSEs IT_cases; |
54 |
66 |
55 (* Turned out to be redundant: |
|
56 Goal "t : termi beta ==> \ |
|
57 \ !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)"; |
|
58 by (etac acc_induct 1); |
|
59 by (force_tac (claset() |
|
60 addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1); |
|
61 val lemma = result(); |
|
62 |
|
63 Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)"; |
|
64 by (dtac lemma 1); |
|
65 by (Blast_tac 1); |
|
66 qed "apps_in_termi_betaD"; |
|
67 |
|
68 Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta"; |
|
69 by (etac acc_induct 1); |
|
70 by (force_tac (claset() addIs [accI],simpset()) 1); |
|
71 val lemma = result(); |
|
72 |
|
73 Goal "Abs r : termi beta ==> r : termi beta"; |
|
74 by (dtac lemma 1); |
|
75 by (Blast_tac 1); |
|
76 qed "Abs_in_termi_betaD"; |
|
77 |
|
78 Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta"; |
|
79 by (etac acc_induct 1); |
|
80 by (force_tac (claset() addIs [accI],simpset()) 1); |
|
81 val lemma = result(); |
|
82 |
|
83 Goal "r$s : termi beta ==> r : termi beta & s : termi beta"; |
|
84 by (dtac lemma 1); |
|
85 by (Blast_tac 1); |
|
86 qed "App_in_termi_betaD"; |
|
87 *) |
|
88 |
67 |
89 Goal "r : termi beta ==> r : IT"; |
68 Goal "r : termi beta ==> r : IT"; |
90 by (etac acc_induct 1); |
69 by (etac acc_induct 1); |
91 by (rename_tac "r" 1); |
70 by (rename_tac "r" 1); |
92 by (etac thin_rl 1); |
71 by (etac thin_rl 1); |