equal
deleted
inserted
replaced
17 consts |
17 consts |
18 IT :: "dB set" |
18 IT :: "dB set" |
19 |
19 |
20 inductive IT |
20 inductive IT |
21 intros |
21 intros |
22 Var [intro]: "rs : lists IT ==> Var n $$ rs : IT" |
22 Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT" |
23 Lambda [intro]: "r : IT ==> Abs r : IT" |
23 Lambda [intro]: "r : IT ==> Abs r : IT" |
24 Beta [intro]: "(r[s/0]) $$ ss : IT ==> s : IT ==> (Abs r $ s) $$ ss : IT" |
24 Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> ss : IT" |
25 |
25 |
26 |
26 |
27 subsection {* Every term in IT terminates *} |
27 subsection {* Every term in IT terminates *} |
28 |
28 |
29 lemma double_induction_lemma [rule_format]: |
29 lemma double_induction_lemma [rule_format]: |
30 "s : termi beta ==> \<forall>t. t : termi beta --> |
30 "s : termi beta ==> \<forall>t. t : termi beta --> |
31 (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)" |
31 (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)" |
32 apply (erule acc_induct) |
32 apply (erule acc_induct) |
33 apply (erule thin_rl) |
33 apply (erule thin_rl) |
34 apply (rule allI) |
34 apply (rule allI) |
35 apply (rule impI) |
35 apply (rule impI) |
36 apply (erule acc_induct) |
36 apply (erule acc_induct) |
63 |
63 |
64 subsection {* Every terminating term is in IT *} |
64 subsection {* Every terminating term is in IT *} |
65 |
65 |
66 declare Var_apps_neq_Abs_apps [THEN not_sym, simp] |
66 declare Var_apps_neq_Abs_apps [THEN not_sym, simp] |
67 |
67 |
68 lemma [simp, THEN not_sym, simp]: "Var n $$ ss \<noteq> Abs r $ s $$ ts" |
68 lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts" |
69 apply (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
69 apply (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
70 done |
70 done |
71 |
71 |
72 lemma [simp]: |
72 lemma [simp]: |
73 "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
73 "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" |
74 apply (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
74 apply (simp add: foldl_Cons [symmetric] del: foldl_Cons) |
75 done |
75 done |
76 |
76 |
77 inductive_cases [elim!]: |
77 inductive_cases [elim!]: |
78 "Var n $$ ss : IT" |
78 "Var n \<degree>\<degree> ss : IT" |
79 "Abs t : IT" |
79 "Abs t : IT" |
80 "Abs r $ s $$ ts : IT" |
80 "Abs r \<degree> s \<degree>\<degree> ts : IT" |
81 |
81 |
82 theorem termi_implies_IT: "r : termi beta ==> r : IT" |
82 theorem termi_implies_IT: "r : termi beta ==> r : IT" |
83 apply (erule acc_induct) |
83 apply (erule acc_induct) |
84 apply (rename_tac r) |
84 apply (rename_tac r) |
85 apply (erule thin_rl) |
85 apply (erule thin_rl) |
94 apply clarify |
94 apply clarify |
95 apply (drule converseI) |
95 apply (drule converseI) |
96 apply (drule ex_step1I, assumption) |
96 apply (drule ex_step1I, assumption) |
97 apply clarify |
97 apply clarify |
98 apply (rename_tac us) |
98 apply (rename_tac us) |
99 apply (erule_tac x = "Var n $$ us" in allE) |
99 apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) |
100 apply force |
100 apply force |
101 apply (rename_tac u ts) |
101 apply (rename_tac u ts) |
102 apply (case_tac ts) |
102 apply (case_tac ts) |
103 apply simp |
103 apply simp |
104 apply blast |
104 apply blast |
108 apply (rule IT.intros) |
108 apply (rule IT.intros) |
109 apply (blast intro: apps_preserves_beta) |
109 apply (blast intro: apps_preserves_beta) |
110 apply (erule mp) |
110 apply (erule mp) |
111 apply clarify |
111 apply clarify |
112 apply (rename_tac t) |
112 apply (rename_tac t) |
113 apply (erule_tac x = "Abs u $ t $$ ss" in allE) |
113 apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE) |
114 apply force |
114 apply force |
115 done |
115 done |
116 |
116 |
117 end |
117 end |