1680 foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms)); |
1680 foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms)); |
1681 |
1681 |
1682 fun extract_safe_rrules(mss,thm) = |
1682 fun extract_safe_rrules(mss,thm) = |
1683 flat (map (orient_rrule mss) (extract_rews(mss,[thm]))); |
1683 flat (map (orient_rrule mss) (extract_rews(mss,[thm]))); |
1684 |
1684 |
|
1685 fun add_safe_simp(mss,thm) = |
|
1686 foldl insert_rrule (mss, extract_safe_rrules(mss,thm)) |
|
1687 |
1685 (* del_simps *) |
1688 (* del_simps *) |
1686 |
1689 |
1687 fun del_rrule(mss as Mss {rules,...}, |
1690 fun del_rrule(mss as Mss {rules,...}, |
1688 rrule as {thm = thm, lhs = lhs, perm = perm}) = |
1691 rrule as {thm = thm, lhs = lhs, perm = perm}) = |
1689 (upd_rules(mss, Net.delete_term ((lhs, rrule), rules, eq_rrule)) |
1692 (upd_rules(mss, Net.delete_term ((lhs, rrule), rules, eq_rrule)) |
1998 in case botc true mss' (subst_bound(v,t),etc) of |
2001 in case botc true mss' (subst_bound(v,t),etc) of |
1999 Some(t',etc') => Some(Abs(a, T, abstract_over(v,t')), etc') |
2002 Some(t',etc') => Some(Abs(a, T, abstract_over(v,t')), etc') |
2000 | None => None |
2003 | None => None |
2001 end |
2004 end |
2002 | t$u => (case t of |
2005 | t$u => (case t of |
2003 Const("==>",_)$s => Some(snd(impc([],s,u,mss,etc))) |
2006 Const("==>",_)$s => Some(impc(s,u,mss,etc)) |
2004 | Abs(_,_,body) => |
2007 | Abs(_,_,body) => |
2005 let val trec = (subst_bound(u,body), etc) |
2008 let val trec = (subst_bound(u,body), etc) |
2006 in case subc mss trec of |
2009 in case subc mss trec of |
2007 None => Some(trec) |
2010 None => Some(trec) |
2008 | trec => trec |
2011 | trec => trec |
2028 handle Pattern.MATCH => appc() ) ) |
2031 handle Pattern.MATCH => appc() ) ) |
2029 | _ => appc() |
2032 | _ => appc() |
2030 end) |
2033 end) |
2031 | _ => None) |
2034 | _ => None) |
2032 |
2035 |
2033 and impc(prems, prem, conc, mss, etc) = |
2036 and impc args = |
2034 let val (prem1,etc1) = if simprem then try_botc mss (prem,etc) |
2037 if mutsimp |
2035 else (prem,etc) |
2038 then let val (prem, conc, mss, etc) = args |
2036 in impc1(prems, prem1, conc, mss, etc1) end |
2039 in snd(mut_impc([], prem, conc, mss, etc)) end |
2037 |
2040 else nonmut_impc args |
2038 and impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) = |
2041 |
|
2042 and mut_impc (prems, prem, conc, mss, etc) = |
|
2043 let val (prem1,etc1) = try_botc mss (prem,etc) |
|
2044 in mut_impc1(prems, prem1, conc, mss, etc1) end |
|
2045 |
|
2046 and mut_impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) = |
2039 let |
2047 let |
2040 fun uncond({thm,lhs,...}:rrule) = |
2048 fun uncond({thm,lhs,...}:rrule) = |
2041 if nprems_of thm = 0 then Some lhs else None |
2049 if nprems_of thm = 0 then Some lhs else None |
2042 |
2050 |
2043 val (rrules1,lhss1,mss1) = |
2051 val (lhss1,mss1) = |
2044 if not useprem then ([],[],mss) else |
|
2045 if maxidx_of_term prem1 <> ~1 |
2052 if maxidx_of_term prem1 <> ~1 |
2046 then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:" |
2053 then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:" |
2047 (Sign.deref sign_ref) prem1; |
2054 (Sign.deref sign_ref) prem1; |
2048 ([],[],mss)) |
2055 ([],mss)) |
2049 else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, |
2056 else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, |
2050 T=propT, maxidx= ~1}) |
2057 T=propT, maxidx= ~1}) |
2051 val rrules1 = extract_safe_rrules(mss,thm) |
2058 val rrules1 = extract_safe_rrules(mss,thm) |
2052 val lhss1 = if mutsimp then mapfilter uncond rrules1 else [] |
2059 val lhss1 = mapfilter uncond rrules1 |
2053 val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1) |
2060 val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1) |
2054 in (rrules1, lhss1, mss1) end |
2061 in (lhss1, mss1) end |
2055 |
2062 |
2056 fun disch1(conc2,(shyps2,hyps2,ders2)) = |
2063 fun disch1(conc2,(shyps2,hyps2,ders2)) = |
2057 let val hyps2' = if gen_mem (op aconv) (prem1, hyps1) |
2064 let val hyps2' = if gen_mem (op aconv) (prem1, hyps1) |
2058 then hyps2 else hyps2\prem1 |
2065 then hyps2 else hyps2\prem1 |
2059 in (Logic.mk_implies(prem1,conc2),(shyps2,hyps2',ders2)) end |
2066 in (Logic.mk_implies(prem1,conc2),(shyps2,hyps2',ders2)) end |
2061 fun rebuild trec2 = |
2068 fun rebuild trec2 = |
2062 let val trec = disch1 trec2 |
2069 let val trec = disch1 trec2 |
2063 in case rewritec (prover,sign_ref,maxidx) mss trec of |
2070 in case rewritec (prover,sign_ref,maxidx) mss trec of |
2064 None => (None,trec) |
2071 None => (None,trec) |
2065 | Some(Const("==>",_)$prem$conc,etc) => |
2072 | Some(Const("==>",_)$prem$conc,etc) => |
2066 impc(prems,prem,conc,mss,etc) |
2073 mut_impc(prems,prem,conc,mss,etc) |
2067 | Some(trec') => (None,trec') |
2074 | Some(trec') => (None,trec') |
2068 end |
2075 end |
2069 |
2076 |
2070 fun simpconc() = |
2077 fun simpconc() = |
2071 case conc of |
2078 case conc of |
2072 Const("==>",_)$s$t => |
2079 Const("==>",_)$s$t => |
2073 (case impc(prems@[prem1],s,t,mss1,etc1) of |
2080 (case mut_impc(prems@[prem1],s,t,mss1,etc1) of |
2074 (Some(i,prem),trec2) => |
2081 (Some(i,prem),trec2) => |
2075 let val trec2' = disch1 trec2 |
2082 let val trec2' = disch1 trec2 |
2076 in if i=0 then impc1(prems,prem,fst trec2',mss,snd trec2') |
2083 in if i=0 then mut_impc1(prems,prem,fst trec2',mss,snd trec2') |
2077 else (Some(i-1,prem),trec2') |
2084 else (Some(i-1,prem),trec2') |
2078 end |
2085 end |
2079 | (None,trec) => rebuild(trec)) |
2086 | (None,trec) => rebuild(trec)) |
2080 | _ => rebuild(try_botc mss1 (conc,etc1)) |
2087 | _ => rebuild(try_botc mss1 (conc,etc1)) |
2081 |
2088 |
2082 in if mutsimp |
2089 in let val sg = Sign.deref sign_ref |
2083 then let val sg = Sign.deref sign_ref |
|
2084 val tsig = #tsig(Sign.rep_sg sg) |
2090 val tsig = #tsig(Sign.rep_sg sg) |
2085 fun reducible t = |
2091 fun reducible t = |
2086 exists (fn lhs => Pattern.matches_subterm tsig (lhs,t)) |
2092 exists (fn lhs => Pattern.matches_subterm tsig (lhs,t)) |
2087 lhss1; |
2093 lhss1; |
2088 in case dropwhile (not o reducible) prems of |
2094 in case dropwhile (not o reducible) prems of |
2089 [] => simpconc() |
2095 [] => simpconc() |
2090 | red::rest => (trace_term false "Can now reduce premise" sg |
2096 | red::rest => (trace_term false "Can now reduce premise" sg |
2091 red; |
2097 red; |
2092 (Some(length rest,prem1),(conc,etc1))) |
2098 (Some(length rest,prem1),(conc,etc1))) |
2093 end |
2099 end |
2094 else simpconc() |
|
2095 end |
2100 end |
|
2101 |
|
2102 (* legacy code - only for backwards compatibility *) |
|
2103 and nonmut_impc(prem, conc, mss, etc as (_,hyps1,_)) = |
|
2104 let val (prem1,etc1) = if simprem then try_botc mss (prem,etc) |
|
2105 else (prem,etc) |
|
2106 val maxidx1 = maxidx_of_term prem1 |
|
2107 val mss1 = |
|
2108 if not useprem then mss else |
|
2109 if maxidx1 <> ~1 |
|
2110 then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:" |
|
2111 (Sign.deref sign_ref) prem1; |
|
2112 mss) |
|
2113 else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, |
|
2114 T=propT, maxidx= ~1}) |
|
2115 in add_safe_simp(add_prems(mss,[thm]), thm) end |
|
2116 val (conc2,(shyps2,hyps2,ders2)) = try_botc mss1 (conc,etc1) |
|
2117 val hyps2' = if prem1 mem hyps1 then hyps2 else hyps2\prem1 |
|
2118 in (Logic.mk_implies(prem1,conc2), (shyps2, hyps2', ders2)) end |
2096 |
2119 |
2097 in try_botc end; |
2120 in try_botc end; |
2098 |
2121 |
2099 |
2122 |
2100 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***) |
2123 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***) |