# HG changeset patch # User nipkow # Date 786365000 -3600 # Node ID b93cc55cb7ab214616c4fd5e40d272bc7d02f785 # Parent 61f39dcc1685f854e9f1adf61b29d48277b69273 small updates because datatype list is now used. In particular Nil -> [] diff -r 61f39dcc1685 -r b93cc55cb7ab Subst/AList.ML --- a/Subst/AList.ML Fri Dec 02 10:26:59 1994 +0100 +++ b/Subst/AList.ML Fri Dec 02 11:43:20 1994 +0100 @@ -7,28 +7,19 @@ open AList; -(*********) - -val al_defs = [alist_rec_def,assoc_def]; - -val alist_ss = prod_ss addsimps [Nil_not_Cons,Cons_not_Nil,Cons_Cons_eq, - list_rec_Nil,list_rec_Cons]; - val al_rews = - let fun mk_thm s = prove_goalw AList.thy al_defs s - (fn _ => [simp_tac alist_ss 1]) + let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s + (fn _ => [simp_tac list_ss 1]) in map mk_thm - ["alist_rec(Nil,c,d) = c", + ["alist_rec([],c,d) = c", "alist_rec(#al,c,d) = d(a,b,al,alist_rec(al,c,d))", - "assoc(v,d,Nil) = d", + "assoc(v,d,[]) = d", "assoc(v,d,#al) = if(v=a,b,assoc(v,d,al))"] end; -(*********) - val prems = goal AList.thy - "[| P(Nil); \ + "[| P([]); \ \ !!x y xs. P(xs) ==> P(#xs) |] ==> P(l)"; -by (list_ind_tac "l" 1); +by (list.induct_tac "l" 1); by (resolve_tac prems 1); by (rtac PairE 1); by (etac ssubst 1); @@ -40,13 +31,3 @@ fun alist_ind_tac a M = EVERY [res_inst_tac [("l",a)] alist_induct M, rename_last_tac a ["1"] (M+1)]; - -(* -val prems = goal AList.thy - "[| P(Nil); !! x y xs. P(xs) --> P(#xs) |] ==> P(a)"; -by (alist_ind_tac "a" 1); -by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs)); -qed "alist_induct2"; - -add_inds alist_induct2; -*) diff -r 61f39dcc1685 -r b93cc55cb7ab Subst/AList.thy --- a/Subst/AList.thy Fri Dec 02 10:26:59 1994 +0100 +++ b/Subst/AList.thy Fri Dec 02 11:43:20 1994 +0100 @@ -14,7 +14,7 @@ rules - alist_rec_def "alist_rec(al,b,c) == list_rec(al, b, split(c))" + alist_rec_def "alist_rec(al,b,c) == list_rec(b, split(c), al)" assoc_def "assoc(v,d,al) == alist_rec(al,d,%x y xs g.if(v=x,y,g))" diff -r 61f39dcc1685 -r b93cc55cb7ab Subst/Subst.ML --- a/Subst/Subst.ML Fri Dec 02 10:26:59 1994 +0100 +++ b/Subst/Subst.ML Fri Dec 02 11:43:20 1994 +0100 @@ -18,9 +18,9 @@ in val subst_rews = map mk_thm ["Const(c) <| al = Const(c)", "Comb(t,u) <| al = Comb(t <| al, u <| al)", - "Nil <> bl = bl", + "[] <> bl = bl", "#al <> bl = # (al <> bl)", - "sdom(Nil) = {}", + "sdom([]) = {}", "sdom(#al) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})" ]; (* This rewrite isn't always desired *) @@ -31,7 +31,7 @@ (**** Substitutions ****) -goal Subst.thy "t <| Nil = t"; +goal Subst.thy "t <| [] = t"; by (uterm_ind_tac "t" 1); by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst]))); qed "subst_Nil"; @@ -95,7 +95,7 @@ (**** Composition of Substitutions ****) -goal Subst.thy "s <> Nil = s"; +goal Subst.thy "s <> [] = s"; by (alist_ind_tac "s" 1); by (ALLGOALS (asm_simp_tac (subst_ss addsimps [subst_Nil]))); qed "comp_Nil"; diff -r 61f39dcc1685 -r b93cc55cb7ab Subst/Unifier.ML --- a/Subst/Unifier.ML Fri Dec 02 10:26:59 1994 +0100 +++ b/Subst/Unifier.ML Fri Dec 02 11:43:20 1994 +0100 @@ -35,7 +35,7 @@ by (rtac refl 1); qed "MoreGen_iff"; -goal Unifier.thy "Nil >> s"; +goal Unifier.thy "[] >> s"; by (simp_tac (subst_ss addsimps [MoreGen_iff]) 1); by (fast_tac (set_cs addIs [refl RS subst_refl]) 1); qed "MoreGen_Nil"; @@ -49,7 +49,7 @@ qed "MGU_iff"; val [prem] = goal Unifier.thy - "~ Var(v) <: t ==> MGUnifier(#Nil,Var(v),t)"; + "~ Var(v) <: t ==> MGUnifier([],Var(v),t)"; by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1); by (REPEAT_SOME (step_tac set_cs)); by (etac subst 1); @@ -81,11 +81,11 @@ invariance,dom_range_disjoint])1); qed "Idem_iff"; -goal Unifier.thy "Idem(Nil)"; +goal Unifier.thy "Idem([])"; by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1); qed "Idem_Nil"; -goal Unifier.thy "~ (Var(v) <: t) --> Idem(#Nil)"; +goal Unifier.thy "~ (Var(v) <: t) --> Idem([])"; by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff] setloop (split_tac [expand_if])) 1); by (fast_tac set_cs 1); @@ -181,7 +181,7 @@ by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp])))); qed "Unify_comm"; -goal Unifier.thy "MGIUnifier(Nil,Const(n),Const(n))"; +goal Unifier.thy "MGIUnifier([],Const(n),Const(n))"; by (simp_tac (subst_ss addsimps [MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1); qed "Unify1"; @@ -191,7 +191,7 @@ val Unify2 = store_thm("Unify2", result() RS mp); val [prem] = goalw Unifier.thy [MGIUnifier_def] - "~Var(v) <: t ==> MGIUnifier(#Nil,Var(v),t)"; + "~Var(v) <: t ==> MGIUnifier([],Var(v),t)"; by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1); qed "Unify3";