llist.ML

 
 open LList;
 
 (** Simplification **)
 
-val llist_simps = [case_Inl, case_Inr];
+val llist_simps = [sum_case_Inl, sum_case_Inr];
 val llist_ss = univ_ss delsimps [Pair_eq] 
                        addsimps llist_simps
-                       addcongs [split_weak_cong, case_weak_cong]
-                       setloop (split_tac [expand_split, expand_case]);
+                       addcongs [split_weak_cong, sum_case_weak_cong]
+                       setloop (split_tac [expand_split, expand_sum_case]);
 
 (** the llist functional **)
 
 val LList_unfold = rewrite_rule [List_Fun_def]
 	 (List_Fun_mono RS (LList_def RS def_gfp_Tarski));

 val CONS_UN1 = result();
 
 goal Prod.thy "split(p, %x y.UN z.f(x,y,z)) = (UN z. split(p, %x y.f(x,y,z)))";
 by (simp_tac (pair_ss setloop (split_tac [expand_split])) 1);
 val split_UN1 = result();
-
-goal Sum.thy "case(s, f, %y. UN z.g(y,z)) = (UN z. case(s, f, %y. g(y,z)))";
-by (simp_tac (sum_ss setloop (split_tac [expand_case])) 1);
-val case2_UN1 = result();
-
+(* Does not seem to be used
+goal Sum.thy "sum_case(s,f,%y.UN z.g(y,z)) = (UN z.sum_case(s,f,%y. g(y,z)))";
+by (simp_tac (sum_ss setloop (split_tac [expand_sum_case])) 1);
+val sum_case2_UN1 = result();
+*)
 val prems = goalw LList.thy [CONS_def]
     "[| M<=M';  N<=N' |] ==> CONS(M,N) <= CONS(M',N')";
 by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
 val CONS_mono = result();
 

 val corec_fun_ss = llist_ss addsimps corec_fun_simps;
 
 (** The directions of the equality are proved separately **)
 
 goalw LList.thy [LList_corec_def]
-    "LList_corec(a,f) <= case(f(a), %u.NIL, \
+    "LList_corec(a,f) <= sum_case(f(a), %u.NIL, \
 \			   %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
 by (rtac UN1_least 1);
 by (res_inst_tac [("n","k")] natE 1);
 by (ALLGOALS (asm_simp_tac corec_fun_ss));
 by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
 val LList_corec_subset1 = result();
 
 goalw LList.thy [LList_corec_def]
-    "case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, LList_corec(w,f)))) <= \
+    "sum_case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, LList_corec(w,f)))) <= \
 \    LList_corec(a,f)";
 by (simp_tac (corec_fun_ss addsimps [CONS_UN1]) 1);
 by (safe_tac set_cs);
 by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' 
 	      asm_simp_tac corec_fun_ss));
 val LList_corec_subset2 = result();
 
 (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
 goal LList.thy
-    "LList_corec(a,f) = case(f(a), %u. NIL, \
+    "LList_corec(a,f) = sum_case(f(a), %u. NIL, \
 \			     %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
 by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
 			 LList_corec_subset2] 1));
 val LList_corec = result();
 
 (*definitional version of same*)
 val [rew] = goal LList.thy
     "[| !!x. h(x) == LList_corec(x,f) |] ==>	\
-\    h(a) = case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, h(w))))";
+\    h(a) = sum_case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, h(w))))";
 by (rewtac rew);
 by (rtac LList_corec 1);
 val def_LList_corec = result();
 
 (*A typical use of co-induction to show membership in the gfp. 

 *)
 val LList_corec_type = result();
 
 (*Lemma for the proof of llist_corec*)
 goal LList.thy
-    "LList_corec(a, %z. case(f(z),Inl,%x. split(x,%v w. Inr(<Leaf(v),w>)))) : \
-\    LList(range(Leaf))";
+   "LList_corec(a, %z.sum_case(f(z),Inl,%x.split(x,%v w.Inr(<Leaf(v),w>)))) : \
+\   LList(range(Leaf))";
 by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] LList_coinduct 1);
 by (rtac rangeI 1);
 by (safe_tac set_cs);
 by (stac LList_corec 1);
-(*nested "case"; requires an explicit split*)
+(*nested "sum_case"; requires an explicit split*)
 by (res_inst_tac [("s", "f(xa)")] sumE 1);
 by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_NIL_I])) 1);
 by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_CONS_I, range_eqI])
                      setloop (split_tac [expand_split])) 1);
 (* FIXME: can the selection of the case split be automated?

 
 (*** Finality of LList(A): Uniqueness of functions defined by corecursion ***)
 
 (*abstract proof using a bisimulation*)
 val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w))));   \
-\    !!x. h2(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |] \
+ "[| !!x. h1(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w))));  \
+\    !!x. h2(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |]\
 \ ==> h1=h2";
 by (rtac ext 1);
 (*next step avoids an unknown (and flexflex pair) in simplification*)
 by (res_inst_tac [("A", "{u.True}"),
 		  ("r", "range(%u. <h1(u),h2(u)>)")] LList_equalityI 1);

 by (ASM_SIMP_TAC (llist_ss addsimps [LListD_Fun_NIL_I, rangeI,
 				    CollectI RS LListD_Fun_CONS_I]) 1);*)
 val LList_corec_unique = result();
 
 val [prem] = goal LList.thy
- "[| !!x. h(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h(w)))) |] \
+ "[| !!x. h(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h(w)))) |] \
 \ ==> h = (%x.LList_corec(x,f))";
 by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
 val equals_LList_corec = result();
 
 

     "ntrunc(Suc(Suc(k)), CONS(M,N)) = CONS (ntrunc(k,M), ntrunc(k,N))";
 by (simp_tac (HOL_ss addsimps [ntrunc_Scons,ntrunc_In1]) 1);
 val ntrunc_CONS = result();
 
 val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w))));  \
-\    !!x. h2(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |] \
+ "[| !!x. h1(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w))));  \
+\    !!x. h2(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |]\
 \ ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
 by (res_inst_tac [("x", "x")] spec 1);
 by (res_inst_tac [("n", "k")] less_induct 1);
 by (rtac allI 1);
 by (stac prem1 1);
 by (stac prem2 1);
-by (simp_tac (sum_ss setloop (split_tac [expand_split,expand_case])) 1);
+by (simp_tac (sum_ss setloop (split_tac [expand_split,expand_sum_case])) 1);
 by (strip_tac 1);
 by (res_inst_tac [("n", "n")] natE 1);
 by (res_inst_tac [("n", "xc")] natE 2);
 by (ALLGOALS(asm_simp_tac(nat_ss addsimps
             [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS])));

 val llistE = result();
 
 (** llist_corec: corecursion for 'a llist **)
 
 goalw LList.thy [llist_corec_def,LNil_def,LCons_def]
-    "llist_corec(a,f) = case(f(a), %u. LNil, \
+    "llist_corec(a,f) = sum_case(f(a), %u. LNil, \
 \			     %v. split(v, %z w. LCons(z, llist_corec(w,f))))";
 by (stac LList_corec 1);
 by (res_inst_tac [("s","f(a)")] sumE 1);
 by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_LList_inverse]) 1);
 by (res_inst_tac [("p","y")] PairE 1);

 val llist_corec = result();
 
 (*definitional version of same*)
 val [rew] = goal LList.thy
     "[| !!x. h(x) == llist_corec(x,f) |] ==>	\
-\    h(a) = case(f(a), %u.LNil, %v. split(v, %z w. LCons(z, h(w))))";
+\    h(a) = sum_case(f(a), %u.LNil, %v. split(v, %z w. LCons(z, h(w))))";
 by (rewtac rew);
 by (rtac llist_corec 1);
 val def_llist_corec = result();
 
 (**** Proofs about type 'a llist functions ****)