50 |
50 |
51 lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs" |
51 lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs" |
52 by (induct xs) simp_all |
52 by (induct xs) simp_all |
53 |
53 |
54 lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)" |
54 lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)" |
55 apply (induct xs) |
55 by (induct xs; intro iffI; simp) |
56 apply (rule iffI, simp, simp) |
|
57 apply (rule iffI, simp, simp) |
|
58 done |
|
59 |
56 |
60 lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)" |
57 lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)" |
61 apply (rule iffI) |
58 by (rule iffI; simp add: listall_app) |
62 apply (simp add: listall_app)+ |
|
63 done |
|
64 |
59 |
65 lemma listall_cong [cong, extraction_expand]: |
60 lemma listall_cong [cong, extraction_expand]: |
66 "xs = ys \<Longrightarrow> listall P xs = listall P ys" |
61 "xs = ys \<Longrightarrow> listall P xs = listall P ys" |
67 \<comment> \<open>Currently needed for strange technical reasons\<close> |
62 \<comment> \<open>Currently needed for strange technical reasons\<close> |
68 by (unfold listall_def) simp |
63 by (unfold listall_def) simp |
80 App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)" |
75 App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)" |
81 | Abs: "NF t \<Longrightarrow> NF (Abs t)" |
76 | Abs: "NF t \<Longrightarrow> NF (Abs t)" |
82 monos listall_def |
77 monos listall_def |
83 |
78 |
84 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
79 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
85 apply (induct m) |
80 proof (induction m) |
86 apply (case_tac n) |
81 case 0 |
87 apply (case_tac [3] n) |
82 then show ?case |
88 apply (simp only: nat.simps, iprover?)+ |
83 by (cases n; simp only: nat.simps; iprover) |
89 done |
84 next |
|
85 case (Suc m) |
|
86 then show ?case |
|
87 by (cases n; simp only: nat.simps; iprover) |
|
88 qed |
90 |
89 |
91 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" |
90 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" |
92 apply (induct m) |
91 proof (induction m) |
93 apply (case_tac n) |
92 case 0 |
94 apply (case_tac [3] n) |
93 then show ?case |
95 apply (simp del: simp_thms subst_all, iprover?)+ |
94 by (cases n; simp only: order.irrefl zero_less_Suc; iprover) |
96 done |
95 next |
|
96 case (Suc m) |
|
97 then show ?case |
|
98 by (cases n; simp only: not_less_zero Suc_less_eq; iprover) |
|
99 qed |
97 |
100 |
98 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)" |
101 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)" |
99 shows "listall NF ts" using NF |
102 shows "listall NF ts" using NF |
100 by cases simp_all |
103 by cases simp_all |
101 |
104 |
102 |
105 |
103 subsection \<open>Properties of \<open>NF\<close>\<close> |
106 subsection \<open>Properties of \<open>NF\<close>\<close> |
104 |
107 |
105 lemma Var_NF: "NF (Var n)" |
108 lemma Var_NF: "NF (Var n)" |
106 apply (subgoal_tac "NF (Var n \<degree>\<degree> [])") |
109 proof - |
107 apply simp |
110 have "NF (Var n \<degree>\<degree> [])" |
108 apply (rule NF.App) |
111 by (rule NF.App) simp |
109 apply simp |
112 then show ?thesis by simp |
110 done |
113 qed |
111 |
114 |
112 lemma Abs_NF: |
115 lemma Abs_NF: |
113 assumes NF: "NF (Abs t \<degree>\<degree> ts)" |
116 assumes NF: "NF (Abs t \<degree>\<degree> ts)" |
114 shows "ts = []" using NF |
117 shows "ts = []" using NF |
115 proof cases |
118 proof cases |
125 listall NF (map (\<lambda>t. t[Var i/j]) ts)" |
128 listall NF (map (\<lambda>t. t[Var i/j]) ts)" |
126 by (induct ts) simp_all |
129 by (induct ts) simp_all |
127 |
130 |
128 lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])" |
131 lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])" |
129 apply (induct arbitrary: i j set: NF) |
132 apply (induct arbitrary: i j set: NF) |
130 apply simp |
133 apply simp |
131 apply (frule listall_conj1) |
134 apply (frule listall_conj1) |
132 apply (drule listall_conj2) |
135 apply (drule listall_conj2) |
133 apply (drule_tac i=i and j=j in subst_terms_NF) |
136 apply (drule_tac i=i and j=j in subst_terms_NF) |
134 apply assumption |
137 apply assumption |
135 apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE]) |
138 apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE]) |
136 apply simp |
139 apply simp |
137 apply (erule NF.App) |
140 apply (erule NF.App) |
138 apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE]) |
141 apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE]) |
139 apply simp |
142 apply (simp_all add: NF.App NF.Abs) |
140 apply (iprover intro: NF.App) |
|
141 apply simp |
|
142 apply (iprover intro: NF.App) |
|
143 apply simp |
|
144 apply (iprover intro: NF.Abs) |
|
145 done |
143 done |
146 |
144 |
147 lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
145 lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
148 apply (induct set: NF) |
146 apply (induct set: NF) |
149 apply (simplesubst app_last) \<comment> \<open>Using \<open>subst\<close> makes extraction fail\<close> |
147 apply (simplesubst app_last) \<comment> \<open>Using \<open>subst\<close> makes extraction fail\<close> |
150 apply (rule exI) |
148 apply (rule exI) |
151 apply (rule conjI) |
149 apply (rule conjI) |
152 apply (rule rtranclp.rtrancl_refl) |
150 apply (rule rtranclp.rtrancl_refl) |
153 apply (rule NF.App) |
151 apply (rule NF.App) |
154 apply (drule listall_conj1) |
152 apply (drule listall_conj1) |
155 apply (simp add: listall_app) |
153 apply (simp add: listall_app) |
156 apply (rule Var_NF) |
154 apply (rule Var_NF) |
157 apply (rule exI) |
155 apply (iprover intro: rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl beta subst_Var_NF) |
158 apply (rule conjI) |
|
159 apply (rule rtranclp.rtrancl_into_rtrancl) |
|
160 apply (rule rtranclp.rtrancl_refl) |
|
161 apply (rule beta) |
|
162 apply (erule subst_Var_NF) |
|
163 done |
156 done |
164 |
157 |
165 lemma lift_terms_NF: "listall NF ts \<Longrightarrow> |
158 lemma lift_terms_NF: "listall NF ts \<Longrightarrow> |
166 listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow> |
159 listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow> |
167 listall NF (map (\<lambda>t. lift t i) ts)" |
160 listall NF (map (\<lambda>t. lift t i) ts)" |
168 by (induct ts) simp_all |
161 by (induct ts) simp_all |
169 |
162 |
170 lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)" |
163 lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)" |
171 apply (induct arbitrary: i set: NF) |
164 apply (induct arbitrary: i set: NF) |
172 apply (frule listall_conj1) |
165 apply (frule listall_conj1) |
173 apply (drule listall_conj2) |
166 apply (drule listall_conj2) |
174 apply (drule_tac i=i in lift_terms_NF) |
167 apply (drule_tac i=i in lift_terms_NF) |
175 apply assumption |
168 apply assumption |
176 apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE]) |
169 apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE]) |
177 apply simp |
170 apply (simp_all add: NF.App NF.Abs) |
178 apply (rule NF.App) |
|
179 apply assumption |
|
180 apply simp |
|
181 apply (rule NF.App) |
|
182 apply assumption |
|
183 apply simp |
|
184 apply (rule NF.Abs) |
|
185 apply simp |
|
186 done |
171 done |
187 |
172 |
188 text \<open> |
173 text \<open> |
189 \<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form. |
174 \<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form. |
190 \<close> |
175 \<close> |