1361 (case assoc(al,x) of |
1361 (case assoc(al,x) of |
1362 Some(y) => if x mem_string vids orelse y mem_string vids then t |
1362 Some(y) => if x mem_string vids orelse y mem_string vids then t |
1363 else Var((y,i),T) |
1363 else Var((y,i),T) |
1364 | None=> t) |
1364 | None=> t) |
1365 | rename(Abs(x,T,t)) = |
1365 | rename(Abs(x,T,t)) = |
1366 Abs(case assoc_string(al,x) of Some(y) => y | None => x, |
1366 Abs(if_none(assoc_string(al,x)) x, T, rename t) |
1367 T, rename t) |
|
1368 | rename(f$t) = rename f $ rename t |
1367 | rename(f$t) = rename f $ rename t |
1369 | rename(t) = t; |
1368 | rename(t) = t; |
1370 fun strip_ren Ai = strip_apply rename (Ai,B) |
1369 fun strip_ren Ai = strip_apply rename (Ai,B) |
1371 in strip_ren end; |
1370 in strip_ren end; |
1372 |
1371 |
1833 raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
1832 raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
1834 (* val lhs = Pattern.eta_contract lhs; *) |
1833 (* val lhs = Pattern.eta_contract lhs; *) |
1835 val (a, _) = dest_Const (head_of lhs) handle TERM _ => |
1834 val (a, _) = dest_Const (head_of lhs) handle TERM _ => |
1836 raise SIMPLIFIER ("Congruence must start with a constant", thm); |
1835 raise SIMPLIFIER ("Congruence must start with a constant", thm); |
1837 val (alist,weak) = congs |
1836 val (alist,weak) = congs |
|
1837 val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm})) |
|
1838 ("Overwriting congruence rule for " ^ quote a); |
1838 val weak2 = if is_full_cong thm then weak else a::weak |
1839 val weak2 = if is_full_cong thm then weak else a::weak |
1839 in |
1840 in |
1840 mk_mss (rules, ((a, {lhs = lhs, thm = thm}) :: alist, weak2), |
1841 mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless) |
1841 procs, bounds, prems, mk_rews, termless) |
|
1842 end; |
1842 end; |
1843 |
1843 |
1844 val (op add_congs) = foldl add_cong; |
1844 val (op add_congs) = foldl add_cong; |
1845 |
1845 |
1846 |
1846 |
1967 end; |
1967 end; |
1968 |
1968 |
1969 fun ren_inst(insts,prop,pat,obj) = |
1969 fun ren_inst(insts,prop,pat,obj) = |
1970 let val ren = match_bvs(pat,obj,[]) |
1970 let val ren = match_bvs(pat,obj,[]) |
1971 fun renAbs(Abs(x,T,b)) = |
1971 fun renAbs(Abs(x,T,b)) = |
1972 Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b)) |
1972 Abs(if_none(assoc_string(ren,x)) x, T, renAbs(b)) |
1973 | renAbs(f$t) = renAbs(f) $ renAbs(t) |
1973 | renAbs(f$t) = renAbs(f) $ renAbs(t) |
1974 | renAbs(t) = t |
1974 | renAbs(t) = t |
1975 in subst_vars insts (if null(ren) then prop else renAbs(prop)) end; |
1975 in subst_vars insts (if null(ren) then prop else renAbs(prop)) end; |
1976 |
1976 |
1977 fun incr_insts i (in1:(indexname*typ)list,in2:(indexname*term)list) = |
1977 fun incr_insts i (in1:(indexname*typ)list,in2:(indexname*term)list) = |