src/HOL/Bali/Term.thy
changeset 13690 ac335b2f4a39
parent 13688 a0b16d42d489
child 14981 e73f8140af78
--- a/src/HOL/Bali/Term.thy	Fri Nov 01 10:35:50 2002 +0100
+++ b/src/HOL/Bali/Term.thy	Fri Nov 01 13:16:28 2002 +0100
@@ -383,6 +383,14 @@
 lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
   by (simp add: inj_term_simps)
 
+lemma term_cases: "
+  \<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
+  \<Longrightarrow> P t"
+  apply (cases t)
+  apply (case_tac a)
+  apply auto
+  done
+
 section {* Evaluation of unary operations *}
 consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
 primrec