6 |
6 |
7 (*** Every term in IT terminates ***) |
7 (*** Every term in IT terminates ***) |
8 |
8 |
9 Goal "s : termi beta ==> !t. t : termi beta --> \ |
9 Goal "s : termi beta ==> !t. t : termi beta --> \ |
10 \ (!r ss. t = r[s/0]$$ss --> Abs r $ s $$ ss : termi beta)"; |
10 \ (!r ss. t = r[s/0]$$ss --> Abs r $ s $$ ss : termi beta)"; |
11 be acc_induct 1; |
11 by (etac acc_induct 1); |
12 be thin_rl 1; |
12 by (etac thin_rl 1); |
13 br allI 1; |
13 by (rtac allI 1); |
14 br impI 1; |
14 by (rtac impI 1); |
15 be acc_induct 1; |
15 by (etac acc_induct 1); |
16 by(Clarify_tac 1); |
16 by (Clarify_tac 1); |
17 br accI 1; |
17 by (rtac accI 1); |
18 by(safe_tac (claset() addSEs [apps_betasE])); |
18 by (safe_tac (claset() addSEs [apps_betasE])); |
19 ba 1; |
19 by (assume_tac 1); |
20 by(blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1); |
20 by (blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1); |
21 by(blast_tac (claset() |
21 by (blast_tac (claset() |
22 addIs [apps_preserves_beta2,subst_preserves_beta2,rtrancl_converseI] |
22 addIs [apps_preserves_beta2,subst_preserves_beta2,rtrancl_converseI] |
23 addDs [acc_downwards]) 1); |
23 addDs [acc_downwards]) 1); |
24 (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) |
24 (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) |
25 by(blast_tac (claset() addDs [apps_preserves_betas]) 1); |
25 by (blast_tac (claset() addDs [apps_preserves_betas]) 1); |
26 qed_spec_mp "double_induction_lemma"; |
26 qed_spec_mp "double_induction_lemma"; |
27 |
27 |
28 Goal "t : IT ==> t : termi(beta)"; |
28 Goal "t : IT ==> t : termi(beta)"; |
29 be IT.induct 1; |
29 be IT.induct 1; |
30 bd rev_subsetD 1; |
30 by (dtac rev_subsetD 1); |
31 br lists_mono 1; |
31 by (rtac lists_mono 1); |
32 br Int_lower2 1; |
32 by (rtac Int_lower2 1); |
33 by(Asm_full_simp_tac 1); |
33 by (Asm_full_simp_tac 1); |
34 bd lists_accD 1; |
34 by (dtac lists_accD 1); |
35 be acc_induct 1; |
35 by (etac acc_induct 1); |
36 br accI 1; |
36 by (rtac accI 1); |
37 by(blast_tac (claset() addSDs [head_Var_reduction]) 1); |
37 by (blast_tac (claset() addSDs [head_Var_reduction]) 1); |
38 be acc_induct 1; |
38 by (etac acc_induct 1); |
39 br accI 1; |
39 by (rtac accI 1); |
40 by(Blast_tac 1); |
40 by (Blast_tac 1); |
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 val IT_cases = map (IT.mk_cases |
53 AddSEs IT_cases; |
53 AddSEs IT_cases; |
54 |
54 |
55 (* Turned out to be redundant: |
55 (* Turned out to be redundant: |
56 Goal "t : termi beta ==> \ |
56 Goal "t : termi beta ==> \ |
57 \ !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)"; |
57 \ !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)"; |
58 be acc_induct 1; |
58 by (etac acc_induct 1); |
59 by(force_tac (claset() |
59 by (force_tac (claset() |
60 addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1); |
60 addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1); |
61 val lemma = result(); |
61 val lemma = result(); |
62 |
62 |
63 Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)"; |
63 Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)"; |
64 bd lemma 1; |
64 by (dtac lemma 1); |
65 by(Blast_tac 1); |
65 by (Blast_tac 1); |
66 qed "apps_in_termi_betaD"; |
66 qed "apps_in_termi_betaD"; |
67 |
67 |
68 Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta"; |
68 Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta"; |
69 be acc_induct 1; |
69 by (etac acc_induct 1); |
70 by(force_tac (claset() addIs [accI],simpset()) 1); |
70 by (force_tac (claset() addIs [accI],simpset()) 1); |
71 val lemma = result(); |
71 val lemma = result(); |
72 |
72 |
73 Goal "Abs r : termi beta ==> r : termi beta"; |
73 Goal "Abs r : termi beta ==> r : termi beta"; |
74 bd lemma 1; |
74 by (dtac lemma 1); |
75 by(Blast_tac 1); |
75 by (Blast_tac 1); |
76 qed "Abs_in_termi_betaD"; |
76 qed "Abs_in_termi_betaD"; |
77 |
77 |
78 Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta"; |
78 Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta"; |
79 be acc_induct 1; |
79 by (etac acc_induct 1); |
80 by(force_tac (claset() addIs [accI],simpset()) 1); |
80 by (force_tac (claset() addIs [accI],simpset()) 1); |
81 val lemma = result(); |
81 val lemma = result(); |
82 |
82 |
83 Goal "r$s : termi beta ==> r : termi beta & s : termi beta"; |
83 Goal "r$s : termi beta ==> r : termi beta & s : termi beta"; |
84 bd lemma 1; |
84 by (dtac lemma 1); |
85 by(Blast_tac 1); |
85 by (Blast_tac 1); |
86 qed "App_in_termi_betaD"; |
86 qed "App_in_termi_betaD"; |
87 *) |
87 *) |
88 |
88 |
89 Goal "r : termi beta ==> r : IT"; |
89 Goal "r : termi beta ==> r : IT"; |
90 be acc_induct 1; |
90 by (etac acc_induct 1); |
91 by(rename_tac "r" 1); |
91 by (rename_tac "r" 1); |
92 be thin_rl 1; |
92 by (etac thin_rl 1); |
93 be rev_mp 1; |
93 by (etac rev_mp 1); |
94 by(Simp_tac 1); |
94 by (Simp_tac 1); |
95 by(res_inst_tac [("t","r")] Apps_dB_induct 1); |
95 by (res_inst_tac [("t","r")] Apps_dB_induct 1); |
96 by(rename_tac "n ts" 1); |
96 by (rename_tac "n ts" 1); |
97 by(Clarify_tac 1); |
97 by (Clarify_tac 1); |
98 brs IT.intrs 1; |
98 brs IT.intrs 1; |
99 by(Clarify_tac 1); |
99 by (Clarify_tac 1); |
100 by(EVERY1[dtac bspec, atac]); |
100 by (EVERY1[dtac bspec, atac]); |
101 be mp 1; |
101 by (etac mp 1); |
102 by(Clarify_tac 1); |
102 by (Clarify_tac 1); |
103 bd converseI 1; |
103 by (dtac converseI 1); |
104 by(EVERY1[dtac ex_step1I, atac]); |
104 by (EVERY1[dtac ex_step1I, atac]); |
105 by(Clarify_tac 1); |
105 by (Clarify_tac 1); |
106 by(rename_tac "us" 1); |
106 by (rename_tac "us" 1); |
107 by(eres_inst_tac [("x","Var n $$ us")] allE 1); |
107 by (eres_inst_tac [("x","Var n $$ us")] allE 1); |
108 by(Force_tac 1); |
108 by (Force_tac 1); |
109 by(rename_tac "u ts" 1); |
109 by (rename_tac "u ts" 1); |
110 by(exhaust_tac "ts" 1); |
110 by (exhaust_tac "ts" 1); |
111 by(Asm_full_simp_tac 1); |
111 by (Asm_full_simp_tac 1); |
112 by(blast_tac (claset() addIs IT.intrs) 1); |
112 by (blast_tac (claset() addIs IT.intrs) 1); |
113 by(rename_tac "s ss" 1); |
113 by (rename_tac "s ss" 1); |
114 by(Asm_full_simp_tac 1); |
114 by (Asm_full_simp_tac 1); |
115 by(Clarify_tac 1); |
115 by (Clarify_tac 1); |
116 brs IT.intrs 1; |
116 brs IT.intrs 1; |
117 by(blast_tac (claset() addIs [apps_preserves_beta]) 1); |
117 by (blast_tac (claset() addIs [apps_preserves_beta]) 1); |
118 be mp 1; |
118 by (etac mp 1); |
119 by(Clarify_tac 1); |
119 by (Clarify_tac 1); |
120 by(rename_tac "t" 1); |
120 by (rename_tac "t" 1); |
121 by(eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1); |
121 by (eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1); |
122 by(Force_tac 1); |
122 by (Force_tac 1); |
123 qed "termi_implies_IT"; |
123 qed "termi_implies_IT"; |