12 |
12 |
13 theory InductTermi imports ListBeta begin |
13 theory InductTermi imports ListBeta begin |
14 |
14 |
15 subsection {* Terminating lambda terms *} |
15 subsection {* Terminating lambda terms *} |
16 |
16 |
17 consts |
17 inductive2 IT :: "dB => bool" |
18 IT :: "dB set" |
18 where |
19 |
19 Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)" |
20 inductive IT |
20 | Lambda [intro]: "IT r ==> IT (Abs r)" |
21 intros |
21 | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)" |
22 Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT" |
|
23 Lambda [intro]: "r : IT ==> Abs r : IT" |
|
24 Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> ss : IT" |
|
25 |
22 |
26 |
23 |
27 subsection {* Every term in IT terminates *} |
24 subsection {* Every term in IT terminates *} |
28 |
25 |
29 lemma double_induction_lemma [rule_format]: |
26 lemma double_induction_lemma [rule_format]: |
30 "s : termi beta ==> \<forall>t. t : termi beta --> |
27 "termi beta s ==> \<forall>t. termi beta t --> |
31 (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)" |
28 (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termi beta (Abs r \<degree> s \<degree>\<degree> ss))" |
32 apply (erule acc_induct) |
29 apply (erule acc_induct) |
33 apply (rule allI) |
30 apply (rule allI) |
34 apply (rule impI) |
31 apply (rule impI) |
35 apply (erule thin_rl) |
32 apply (erule thin_rl) |
36 apply (erule acc_induct) |
33 apply (erule acc_induct) |
37 apply clarify |
34 apply clarify |
38 apply (rule accI) |
35 apply (rule accI) |
39 apply (safe elim!: apps_betasE) |
36 apply (safe elim!: apps_betasE) |
40 apply assumption |
37 apply assumption |
41 apply (blast intro: subst_preserves_beta apps_preserves_beta) |
38 apply (blast intro: subst_preserves_beta apps_preserves_beta) |
42 apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI |
39 apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI' |
43 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) *) |
44 apply (blast dest: apps_preserves_betas) |
41 apply (blast dest: apps_preserves_betas) |
45 done |
42 done |
46 |
43 |
47 lemma IT_implies_termi: "t : IT ==> t : termi beta" |
44 lemma IT_implies_termi: "IT t ==> termi beta t" |
48 apply (induct set: IT) |
45 apply (induct set: IT) |
49 apply (drule rev_subsetD) |
46 apply (drule rev_predicate1D [OF _ listsp_mono [where B="termi beta"]]) |
50 apply (rule lists_mono) |
47 apply fast |
51 apply (rule Int_lower2) |
|
52 apply simp |
|
53 apply (drule lists_accD) |
48 apply (drule lists_accD) |
54 apply (erule acc_induct) |
49 apply (erule acc_induct) |
55 apply (rule accI) |
50 apply (rule accI) |
56 apply (blast dest: head_Var_reduction) |
51 apply (blast dest: head_Var_reduction) |
57 apply (erule acc_induct) |
52 apply (erule acc_induct) |
70 |
65 |
71 lemma [simp]: |
66 lemma [simp]: |
72 "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
67 "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
73 by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
68 by (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
74 |
69 |
75 inductive_cases [elim!]: |
70 inductive_cases2 [elim!]: |
76 "Var n \<degree>\<degree> ss : IT" |
71 "IT (Var n \<degree>\<degree> ss)" |
77 "Abs t : IT" |
72 "IT (Abs t)" |
78 "Abs r \<degree> s \<degree>\<degree> ts : IT" |
73 "IT (Abs r \<degree> s \<degree>\<degree> ts)" |
79 |
74 |
80 theorem termi_implies_IT: "r : termi beta ==> r : IT" |
75 theorem termi_implies_IT: "termi beta r ==> IT r" |
81 apply (erule acc_induct) |
76 apply (erule acc_induct) |
82 apply (rename_tac r) |
77 apply (rename_tac r) |
83 apply (erule thin_rl) |
78 apply (erule thin_rl) |
84 apply (erule rev_mp) |
79 apply (erule rev_mp) |
85 apply simp |
80 apply simp |
88 apply (rule IT.intros) |
83 apply (rule IT.intros) |
89 apply clarify |
84 apply clarify |
90 apply (drule bspec, assumption) |
85 apply (drule bspec, assumption) |
91 apply (erule mp) |
86 apply (erule mp) |
92 apply clarify |
87 apply clarify |
93 apply (drule converseI) |
88 apply (drule_tac r=beta in conversepI) |
94 apply (drule ex_step1I, assumption) |
89 apply (drule_tac r="beta^--1" in ex_step1I, assumption) |
95 apply clarify |
90 apply clarify |
96 apply (rename_tac us) |
91 apply (rename_tac us) |
97 apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
92 apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
98 apply force |
93 apply force |
99 apply (rename_tac u ts) |
94 apply (rename_tac u ts) |