neuper@37906: (* isac's rewriter neuper@37906: (c) Walther Neuper 2000 neuper@37906: neuper@37947: use"ProgLang/rewrite.sml"; neuper@37906: use"rewrite.sml"; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: exception NO_REWRITE; neuper@37906: exception STOP_REW_SUB; (*WN050820 quick and dirty*) neuper@37906: neuper@37906: (*17.6.00: rewrite by going down the term with rew_sub*) neuper@37906: (* val (thy, i, bdv, tless, rls, put_asm, thm, ct) = neuper@37906: (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term); neuper@37906: *) neuper@37906: fun rewrite__ thy i bdv tless rls put_asm thm ct = neuper@38022: (let neuper@37906: val (t',asms,lrd,rew) = neuper@37906: rew_sub thy i bdv tless rls put_asm [(*root of the term*)] neuper@37906: (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct; neuper@37906: in if rew then SOME (t', distinct asms) neuper@37906: else NONE end) neuper@38022: (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *) neuper@37906: and rew_sub thy i bdv tless rls put_asm lrd r t = neuper@38015: ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));*) neuper@37906: let (* copy from Pure/thm.ML: fun rewritec *) neuper@37906: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop neuper@37906: o Logic.strip_imp_concl) r; neuper@37906: val r' = Envir.subst_term (Pattern.match thy (lhs, t) neuper@37906: (Vartab.empty, Vartab.empty)) r; neuper@38022: val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) neuper@38022: (Logic.count_prems r', [], r')); neuper@37906: val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop neuper@37906: o Logic.strip_imp_concl) r'; neuper@38015: (*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*) neuper@37906: val _= if ! trace_rewrite andalso i < ! depth andalso p' <> [] neuper@38015: then tracing((idt"#"(i+1))^" eval asms: "^(term2str r')) else(); neuper@37976: val (t'',p'') = (*conditional rewriting*) neuper@37906: let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls neuper@37906: in if nofalse neuper@37906: then (if ! trace_rewrite andalso i < ! depth andalso p' <> [] neuper@38015: then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^ neuper@37906: " stored: "^(terms2str simpl_p')) neuper@38022: else(); (t',simpl_p')) (* uncond.rew. from above*) neuper@37906: else neuper@37906: (if ! trace_rewrite andalso i < ! depth neuper@38015: then tracing((idt"#"(i+1))^" asms false: "^(terms2str p')) neuper@37906: else(); raise STOP_REW_SUB (*dont go into subterms of cond*)) neuper@37906: end neuper@37976: in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*) neuper@37906: then (if ! trace_rewrite andalso i < ! depth neuper@38015: then tracing((idt"#"i)^" not: \""^ neuper@37906: (term2str t)^"\" > \""^ neuper@37906: (term2str t')^"\"") else (); neuper@37906: raise NO_REWRITE ) neuper@38015: else ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^ neuper@37906: ", p'' ="^(terms2str p'')^", true)");*) neuper@37906: (t'',p'',[],true)) neuper@37906: end neuper@37906: ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) => neuper@38015: ((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*) neuper@37906: case t of neuper@37906: Const(s,T) => (Const(s,T),[],lrd,false) neuper@37906: | Free(s,T) => (Free(s,T),[],lrd,false) neuper@37906: | Var(n,T) => (Var(n,T),[],lrd,false) neuper@37906: | Bound i => (Bound i,[],lrd,false) neuper@37906: | Abs(s,T,body) => neuper@37906: let val (t', asms, lrd, rew) = neuper@37906: rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body neuper@37906: in (Abs(s,T,t'), asms, [], rew) end neuper@37906: | t1 $ t2 => neuper@37906: let val (t2', asm2, lrd, rew2) = neuper@37906: rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2 neuper@37906: in if rew2 then (t1 $ t2', asm2, lrd, true) neuper@37906: else let val (t1', asm1, lrd, rew1) = neuper@37906: rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1 neuper@37906: in if rew1 then (t1' $ t2, asm1, lrd, true) neuper@37906: else (t1 $ t2,[], lrd, false) end neuper@37906: end) neuper@38022: (* simplify asumptions until one evaluates to false, store intermined's (x~=0)*) neuper@37906: and eval__true thy i asms bdv rls = neuper@38036: if asms = [HOLogic.true_const] orelse asms = [] then ([], true) neuper@38036: (* this allows to check Rrls with prepat = ([HOLogic.true_const], pat) *) neuper@38022: else if asms = [HOLogic.false_const] then ([], false) neuper@37906: else let neuper@37906: fun chk indets [] = (indets, true)(*return asms<>True until false*) neuper@37906: | chk indets (a::asms) = neuper@37906: (case rewrite__set_ thy (i+1) false bdv rls a of neuper@37906: NONE => (chk (indets @ [a]) asms) neuper@37906: | SOME (t, a') => neuper@37906: if t = HOLogic.true_const neuper@37906: then (chk (indets @ a') asms) neuper@37906: else if t = HOLogic.false_const then ([], false) neuper@37906: (*asm false .. thm not applied ^^^; continue until False vvv*) neuper@38022: else chk (indets @ [t] @ a') asms); neuper@37906: in chk [] asms end neuper@38022: (* rewrite with a rule set, which must not be the empty Erls *) neuper@37906: and rewrite__set_ _ _ __ Erls t = neuper@38031: error("rewrite__set_ called with 'Erls' for '"^term2str t^"'") neuper@38036: (* rewrite with a 'reverse rule set' implemented by ML code *) neuper@37906: | rewrite__set_ thy i _ _ (rrls as Rrls _) t = neuper@37906: let val _= if ! trace_rewrite andalso i < ! depth neuper@38015: then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^ neuper@37906: (term2str t)) else () neuper@37906: val (t', asm, rew) = app_rev thy (i+1) rrls t neuper@37906: in if rew then SOME (t', distinct asm) neuper@37906: else NONE end neuper@38022: (* rewrite with a rule set containing Thms or Calculations *) neuper@37906: | rewrite__set_ thy i put_asm bdv rls ct = neuper@37906: (* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term); neuper@37906: *) neuper@37906: let neuper@37906: datatype switch = Appl | Noap; neuper@37906: fun rew_once ruls asm ct Noap [] = (ct,asm) neuper@37906: | rew_once ruls asm ct Appl [] = neuper@37906: (case rls of Rls _ => rew_once ruls asm ct Noap ruls neuper@37906: | Seq _ => (ct,asm)) neuper@37906: | rew_once ruls asm ct apno (rul::thms) = neuper@37906: (* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls); neuper@37906: val Thm (thmid, thm) = rul; neuper@37906: *) neuper@37906: case rul of neuper@37906: Thm (thmid, thm) => neuper@37906: (if !trace_rewrite andalso i < ! depth neuper@38015: then tracing((idt"#"(i+1))^" try thm: "^thmid) else (); neuper@37906: case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) neuper@37906: ((#erls o rep_rls) rls) put_asm thm ct of neuper@37906: NONE => rew_once ruls asm ct apno thms neuper@37906: | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth neuper@38015: then tracing((idt"="(i+1))^" rewrites to: "^ neuper@37906: (term2str ct')) else (); neuper@37906: rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms))) neuper@37906: | Calc (cc as (op_,_)) => neuper@37906: (let val _= if !trace_rewrite andalso i < ! depth then neuper@38015: tracing((idt"#"(i+1))^" try calc: "^op_^"'") else (); neuper@37906: val ct = uminus_to_string ct neuper@37906: in case get_calculation_ thy cc ct of neuper@38022: NONE => rew_once ruls asm ct apno thms neuper@37906: | SOME (thmid, thm') => neuper@37906: let neuper@37906: val pairopt = neuper@37906: rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) neuper@37906: ((#erls o rep_rls) rls) put_asm thm' ct; neuper@37906: val _ = if pairopt <> NONE then () neuper@38031: else error("rewrite_set_, rewrite_ \""^ neuper@37906: (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") neuper@37906: val _ = if ! trace_rewrite andalso i < ! depth neuper@38015: then tracing((idt"="(i+1))^" calc. to: "^ neuper@37906: (term2str ((fst o the) pairopt))) neuper@37906: else() neuper@38022: in rew_once ruls asm ((fst o the) pairopt) Appl (rul::thms) end neuper@37906: end) neuper@37906: | Cal1 (cc as (op_,_)) => neuper@37906: (let val _= if !trace_rewrite andalso i < ! depth then neuper@38015: tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else (); neuper@37906: val ct = uminus_to_string ct neuper@37906: in case get_calculation1_ thy cc ct of neuper@37906: NONE => (ct, asm) neuper@37906: | SOME (thmid, thm') => neuper@37906: let neuper@37906: val pairopt = neuper@37906: rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) neuper@37906: ((#erls o rep_rls) rls) put_asm thm' ct; neuper@37906: val _ = if pairopt <> NONE then () neuper@38031: else error("rewrite_set_, rewrite_ \""^ neuper@37906: (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") neuper@37906: val _ = if ! trace_rewrite andalso i < ! depth neuper@38015: then tracing((idt"="(i+1))^" cal1. to: "^ neuper@37906: (term2str ((fst o the) pairopt))) neuper@37906: else() neuper@37906: in the pairopt end neuper@37906: end) neuper@37906: | Rls_ rls' => neuper@37906: (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of neuper@37906: SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms neuper@37906: | NONE => rew_once ruls asm ct apno thms); neuper@37906: neuper@37906: val ruls = (#rules o rep_rls) rls; neuper@37906: val _= if ! trace_rewrite andalso i < ! depth neuper@38015: then tracing ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^ neuper@37906: (term2str ct)) else () neuper@37906: val (ct',asm') = rew_once ruls [] ct Noap ruls; neuper@37906: in if ct = ct' then NONE else SOME (ct', distinct asm') end neuper@37906: neuper@37906: and app_rev thy i rrls t = neuper@38036: let (* check a (precond, pattern) of a rev-set; stops with 1st true *) neuper@37906: fun chk_prepat thy erls [] t = true neuper@37906: | chk_prepat thy erls prepat t = neuper@37906: let fun chk (pres, pat) = neuper@37906: (let val subst: Type.tyenv * Envir.tenv = neuper@37906: Pattern.match thy (pat, t) neuper@37906: (Vartab.empty, Vartab.empty) neuper@38036: val _ = tracing ("app_rev: pres=------------------"); neuper@38036: val _ = tracing ("app_rev: pres=" ^ terms2str pres); neuper@38036: val _ = tracing ("app_rev: pat =" ^ term2str pat); neuper@38036: val _ = tracing ("app_rev: t =" ^ term2str t); neuper@37906: in snd (eval__true thy (i+1) neuper@37906: (map (Envir.subst_term subst) pres) neuper@37906: [] erls) neuper@37906: end) neuper@37906: handle _ => false neuper@37906: fun scan_ f [] = false (*scan_ NEVER called by []*) neuper@37906: | scan_ f (pp::pps) = if f pp then true neuper@37906: else scan_ f pps; neuper@37906: in scan_ chk prepat end; neuper@37906: neuper@38036: (* apply the normal_form of a rev-set *) neuper@37906: fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t = neuper@37906: if chk_prepat thy erls prepat t neuper@38015: then ((*tracing("### app_rev': t = "^(term2str t));*) neuper@37906: normal_form t) neuper@37906: else NONE; neuper@37906: neuper@37906: val opt = app_rev' thy rrls t neuper@37906: in case opt of neuper@37906: SOME (t', asm) => (t', asm, true) neuper@37906: | NONE => app_sub thy i rrls t neuper@37906: end neuper@37906: and app_sub thy i rrls t = neuper@38015: ((*tracing("### app_sub: subterm = "^(term2str t));*) neuper@37906: case t of neuper@37906: Const (s, T) => (Const(s, T), [], false) neuper@37906: | Free (s, T) => (Free(s, T), [], false) neuper@37906: | Var (n, T) => (Var(n, T), [], false) neuper@37906: | Bound i => (Bound i, [], false) neuper@37906: | Abs (s, T, body) => neuper@37906: let val (t', asm, rew) = app_rev thy i rrls body neuper@37906: in (Abs(s, T, t'), asm, rew) end neuper@37906: | t1 $ t2 => neuper@37906: let val (t2', asm2, rew2) = app_rev thy i rrls t2 neuper@37906: in if rew2 then (t1 $ t2', asm2, true) neuper@37906: else let val (t1', asm1, rew1) = app_rev thy i rrls t1 neuper@37906: in if rew1 then (t1' $ t2, asm1, true) neuper@37906: else (t1 $ t2, [], false) end neuper@37906: end); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.rewriting without argument [] for rew_ord.*) neuper@37906: (*WN.11.6.03: shouldnt asm<>[] lead to false ????*) neuper@37906: fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls; neuper@37906: neuper@37906: neuper@37906: (*.rewriting without internal argument [] for rew_ord.*) neuper@37906: (* val (thy, rew_ord, erls, bool, thm, term) = neuper@37906: (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f); neuper@37906: val (thy, rew_ord, erls, bool, thm, term) = neuper@37906: (thy, rew_ord, erls, false, thm, t''); neuper@37906: *) neuper@37906: fun rewrite_ thy rew_ord erls bool thm term = neuper@37906: rewrite__ thy 1 [] rew_ord erls bool thm term; neuper@37906: fun rewrite_set_ thy bool rls term = neuper@37906: (* val (thy, bool, rls, term) = (thy, false, srls, t); neuper@37906: *) neuper@37906: rewrite__set_ thy 1 bool [] rls term; neuper@37906: neuper@37906: neuper@37906: fun subs'2subst thy (s:subs') = neuper@37906: (((map (apfst (term_of o the o (parse thy)))) neuper@37906: o (map (apsnd (term_of o the o (parse thy))))) s):subst; neuper@37906: neuper@37906: (*.variants of rewrite.*) neuper@37906: (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, neuper@37906: thus the argument put_asm IS NOT NECESSARY -- FIXME*) neuper@37906: (* val (rew_ord,rls,put_asm,thm,ct)= neuper@37906: (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t); neuper@37906: *) neuper@37906: fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool) neuper@37906: (subst:(term * term) list) (thm:thm) (ct:term) = neuper@37906: rewrite__ thy 1 subst rew_ord rls put_asm thm ct; neuper@37906: neuper@37906: fun rewrite_set_inst_ (thy:theory) neuper@37906: (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) = neuper@37906: (*let neuper@37906: val subst = subs'2subst thy subs'; neuper@37906: val subrls = instantiate_rls subs' rls neuper@37906: in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct neuper@37906: (*end*); neuper@37906: neuper@38025: (* given a list of equalities (lhs = rhs) and a term, neuper@38025: replace all occurrences of lhs in the term with rhs; neuper@38025: thus the order or equalities matters: put variables in lhs first. *) neuper@38025: fun rewrite_terms_ thy ord erls equs t = neuper@38025: let (*val _=tracing("### rewrite_terms_ equs= '"^terms2str equs^"' ..."^ neuper@38025: term_detail2str (hd equs)^ neuper@37906: "### rewrite_terms_ t= '"^term2str t^"' ..."^ neuper@37906: term_detail2str t);*) neuper@37906: fun rew_ (t', asm') [] _ = (t', asm') neuper@38025: (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], equs, t); neuper@37906: 2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t''); neuper@37906: rew_ (t', asm') (r::rs) t; neuper@37906: *) neuper@37906: | rew_ (t', asm') (rules as r::rs) t = neuper@38015: let val _ = tracing("rew_ "^term2str t); neuper@37906: val (t'', asm'', lrd, rew) = neuper@38025: rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t neuper@37906: in if rew neuper@38025: then (tracing ("true rew_ " ^ term2str t''); neuper@37906: rew_ (t'', asm' @ asm'') rules t'') neuper@38025: else (tracing ("false rew_ " ^ term2str t''); neuper@37906: rew_ (t', asm') rs t') neuper@37906: end neuper@38025: val (t'', asm'') = rew_ (e_term, []) equs t neuper@37906: in if t'' = e_term neuper@37906: then NONE else SOME (t'', asm'') neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: (*. search ct for adjacent numerals and calculate them by operator isa_fn .*) neuper@37906: fun calculate_ thy isa_fn ct = neuper@37906: let val ct = uminus_to_string ct neuper@37906: in case get_calculation_ thy isa_fn ct of neuper@37906: NONE => NONE neuper@37906: | SOME (thmID, thm) => neuper@37906: (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct neuper@37906: in SOME (rew,(thmID, thm)) end) neuper@37906: handle _ => error ("calculate_: "^thmID^" does not rewrite") neuper@37906: end; neuper@37906: (* neuper@37906: > val thy = InsSort.thy; neuper@37906: > val op_ = "le"; (* < *) neuper@37906: > val ct = (the o (parse thy)) neuper@37906: "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"; neuper@37906: > calculate_ thy op_ ct; neuper@37906: SOME neuper@37906: ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])", neuper@37906: "(#1 < #3) = True") : (cterm * thm) option *) neuper@37906: neuper@37906: neuper@37906: (* for test-printouts: neuper@38015: val _ = tracing("in rew_sub : "^( Syntax.string_of_term (thy2ctxt thy) t)) neuper@38015: val _ = tracing("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems'))) neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs')) neuper@38031: handle _ => error ("get_rls_scr: no script for "^rs'); neuper@37906: neuper@37906: neuper@37906: (*make_thm added to Pure/thm.ML*) neuper@37906: fun mk_thm thy str = neuper@37906: let val t = (term_of o the o (parse thy)) str neuper@37906: val t' = case t of neuper@37906: Const ("==>",_) $ _ $ _ => t neuper@37906: | _ => Trueprop $ t neuper@37938: in make_thm (cterm_of thy t') end; neuper@37906: (* neuper@37906: val str = "?r ^^^ 2 = ?r * ?r"; neuper@37906: val thm = realpow_twoI; neuper@37906: neuper@37906: val t1 = (#prop o rep_thm) (num_str thm); neuper@37906: val t2 = Trueprop $ ((term_of o the o (parse thy)) str); neuper@37906: t1 = t2; neuper@37906: val it = true : bool ... !!! neuper@37906: val th1 = (num_str thm); neuper@37906: val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e; neuper@37906: th1 = th2; neuper@37906: ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?! neuper@37906: neuper@37906: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ neuper@37906: val str = "k ~= 0 ==> m * k / (n * k) = m / n"; neuper@37906: val thm = real_mult_div_cancel2; neuper@37906: neuper@37906: val t1 = (#prop o rep_thm) (num_str thm); neuper@37906: val t2 = ((term_of o the o (parse thy)) str); neuper@37906: t1 = t2; neuper@37906: val it = false : bool ... Var .. Free neuper@37906: val th1 = (num_str thm); neuper@37906: val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e; neuper@37906: th1 = th2; neuper@37906: ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?! neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (*prints subgoal etc. neuper@37906: ((goal thy);(topthm()) o ) str; *) neuper@37906: (*assume rejects scheme variables neuper@37938: assume ((cterm_of thy) (Trueprop $ neuper@37906: (term_of o the o (parse thy)) str)); *) neuper@37906: neuper@37906: neuper@37906: (* outcommented 18.11.xx, xx < 02 ------- neuper@37906: fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm) neuper@37906: | rul2rul' (Calc op_) = Calc' op_; neuper@37906: fun rul'2rul thy (Thm'(thmid, ct')) = neuper@37906: Thm (thmid, mk_thm thy ct') neuper@37906: | rul'2rul thy' (Calc' op_) = Calc op_; neuper@37906: neuper@37906: neuper@37906: fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) = neuper@37906: Rls'{preconds'= map string_of_cterm preconds, neuper@37906: rew_ord' = fst rew_ord, neuper@37906: rules' = map rul2rul' rules}:rlsdat'; neuper@37906: neuper@37906: fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord, neuper@37906: rules'=rules}:rlsdat') = neuper@37906: let val thy = the (assoc' (theory',thy')) neuper@37906: in Rls{preconds = map (the o (parse thy)) preconds, neuper@37906: rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))), neuper@37906: rules = map (rul'2rul thy) rules}:rls end; neuper@37906: ------- *) neuper@37906: neuper@37906: (*.get the theorem associated with the xstring-identifier; neuper@37906: if the identifier starts with "sym_" then swap lhs = rhs around = neuper@37906: (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI); neuper@37906: identifiers starting with "#" come from Calc and neuper@37906: get a hand-made theorem (containing numerals only).*) neuper@37906: fun assoc_thm' (thy:theory) ((thmid, ct'):thm') = neuper@37906: (case explode thmid of neuper@37906: "s"::"y"::"m"::"_"::id => neuper@37906: if hd id = "#" neuper@37906: then mk_thm thy ct' neuper@37906: else ((num_str o (PureThy.get_thm thy)) (implode id)) RS sym neuper@37906: | id => neuper@37906: if hd id = "#" neuper@37906: then mk_thm thy ct' neuper@37906: else (num_str o (PureThy.get_thm thy)) thmid neuper@37906: ) handle _ => neuper@38031: error ("assoc_thm': '"^thmid^"' not in '"^ neuper@37906: (theory2domID thy)^"' (and parents)"); neuper@37906: (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3"); neuper@37906: val it = "6 = 2 * 3" : thm neuper@37906: neuper@37965: > assoc_thm' Isac.thy ("add_0_left",""); neuper@37906: val it = "0 + ?z = ?z" : thm neuper@37906: neuper@37906: > assoc_thm' Isac.thy ("sym_real_add_zero_left",""); neuper@37906: val it = "?t = 0 + ?t" [.] : thm neuper@37906: neuper@37906: > assoc_thm' HOL.thy ("sym_real_add_zero_left",""); neuper@37965: *** Unknown theorem(s) "add_0_left" neuper@37906: *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents) neuper@37906: uncaught exception ERROR*) neuper@37906: neuper@37906: neuper@37906: fun parse' (thy:theory') (ct:cterm') = neuper@37906: case parse ((the o assoc')(!theory',thy)) ct of neuper@37906: NONE => NONE neuper@37906: | SOME ct => SOME ((term2str (term_of ct)):cterm'); neuper@37906: neuper@37906: neuper@37906: (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst neuper@37906: thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) neuper@37906: fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') neuper@37906: (put_asm:bool) (thm:thm') (ct:cterm') = neuper@37906: (* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f); neuper@37906: *) neuper@37906: let val thy = (the o assoc')(!theory',thy'); neuper@37906: in neuper@37906: case rewrite_ thy neuper@37906: ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls)) neuper@37906: put_asm ((assoc_thm' thy) thm) neuper@37906: ((term_of o the o (parse thy)) ct) of neuper@37906: NONE => NONE neuper@37906: | SOME (t, ts) => SOME (term2str t, terms2str ts) neuper@37906: end; neuper@37906: neuper@37906: (* neuper@37906: val thy = "RatArith.thy"; neuper@37906: val rew_ord = "dummy_ord"; neuper@37906: > val rls = "eval_rls"; neuper@37906: val put_asm = true; neuper@37906: val thm = ("square_equation_left",""); neuper@37906: val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)"; neuper@37906: neuper@37906: val Zthy = ((the o assoc')(!theory',thy)); neuper@37906: val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord)); neuper@37906: val Zrls = ((the o assoc')(!ruleset',rls)); neuper@37906: val Zput_asm = put_asm; neuper@37906: val Zthm = ((the o (assoc'_thm' thy)) thm); neuper@37906: val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct); neuper@37906: neuper@37906: rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct; neuper@37906: neuper@37906: use"Isa99/interface_ME_ISA.sml"; neuper@37906: *) neuper@37906: neuper@37906: (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst neuper@37906: thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) neuper@37906: fun rewrite_set (thy':theory') (put_asm:bool) neuper@37906: (rls:rls') (ct:cterm') = neuper@37906: let val thy = (the o assoc')(!theory',thy'); neuper@37906: in neuper@37906: case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls)) neuper@37906: ((term_of o the o (parse thy)) ct) of neuper@37906: NONE => NONE neuper@37906: | SOME (t, ts) => SOME (term2str t, terms2str ts) neuper@37906: end; neuper@37906: neuper@37906: (*evaluate list-expressions neuper@37906: should work on term, and stand in Isa99/rewrite-parse.sml, neuper@37906: but there list_rls <- eval_binop is not yet defined*) neuper@37906: (*fun eval_listexpr' ct = neuper@37947: let val rew = rewrite_set "ListC.thy" false "list_rls" ct; neuper@37906: in case rew of neuper@37906: SOME (res,_) => res neuper@37906: | NONE => ct end;-----------------30.9.02---*) neuper@37906: fun eval_listexpr_ thy srls t = neuper@37906: (* val (thy, srls, t) = neuper@37906: ((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t)); neuper@37906: *) neuper@37906: let val rew = rewrite_set_ thy false srls t; neuper@37906: in case rew of neuper@37906: SOME (res,_) => res neuper@37906: | NONE => t end; neuper@37906: neuper@37906: neuper@37906: fun get_calculation' (thy:theory') op_ (ct:cterm') = neuper@37906: case get_calculation_ ((the o assoc')(!theory',thy)) op_ neuper@37906: ((uminus_to_string o term_of o the o neuper@37906: (parse ((the o assoc')(!theory',thy)))) ct) of neuper@37906: NONE => NONE neuper@37906: | SOME (thmid, thm) => neuper@37906: SOME ((thmid, string_of_thmI thm):thm'); neuper@37906: neuper@37906: fun calculate (thy':theory') op_ (ct:cterm') = neuper@37906: let val thy = (the o assoc')(!theory',thy'); neuper@37906: in neuper@37906: case calculate_ thy op_ neuper@37906: ((term_of o the o (parse thy)) ct) of neuper@37906: NONE => NONE neuper@37906: | SOME (ct,(thmID,thm)) => neuper@37906: SOME (term2str ct, neuper@37906: (thmID, string_of_thmI thm):thm') neuper@37906: end; neuper@37906: (* neuper@37906: fun instantiate'' thy' subs ((thmid,ct'):thm') = neuper@37906: let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*) neuper@37906: in (thmid_, (string_of_thmI o (read_instantiate subs)) neuper@37906: ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end; neuper@37906: neuper@37906: fun instantiate_rls' thy' subs (rls:rls') = neuper@37906: rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat'; neuper@37906: neuper@37906: ... problem with these functions: neuper@37906: > val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)"; neuper@37906: val thm = "(bdv + a = b) = (bdv = b - a)" : thm neuper@37906: > show_types:=true; thm; neuper@37906: val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm neuper@37906: ... and this doesn't match because of too general typing (?!) neuper@37906: and read_insitantiate doesn't instantiate the types (?!) neuper@37906: === solutions: neuper@37906: (1) hard-coded type-instantiation ("'a", "RatArith.rat") neuper@37906: (2) instantiate', instantiate ... no help by isabelle-users@ !!! neuper@37906: === conclusion: neuper@37906: rewrite_inst, rewrite_set_inst circumvent the problem, neuper@37906: according functions out-commented with 'instantiate'' neuper@37906: *) neuper@37906: neuper@37906: (* instantiate'' neuper@37906: fun instantiate'' thy' subs ((thmid,ct'):thm') = neuper@37906: let neuper@37906: val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*) neuper@37906: val thy = (the o assoc')(!theory',thy'); neuper@37906: val typs = map (#T o rep_cterm o the o (parse thy)) neuper@37906: ((snd o split_list) subs); neuper@37906: val ctyps = map neuper@37906: ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy)) neuper@37906: ((snd o split_list) subs); neuper@37906: neuper@37906: > val thy' = "RatArith.thy"; neuper@37906: > val subs = [("bdv","x::rat"),("zzz","z::nat")]; neuper@37906: > (the o (parse ((the o assoc')(!theory',thy')))) "x::rat"; neuper@37906: > (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy')))); neuper@37906: neuper@37906: > val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o neuper@37906: (parse ((the o assoc')(!theory',thy')))) "x::rat"; neuper@37906: > val bdv = (the o (parse thy)) "bdv"; neuper@37906: > val x = (the o (parse thy)) "x"; neuper@37906: > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add) neuper@37906: handle e => print_exn e; neuper@37906: uncaught exception THM neuper@37906: raised at: thm.ML:1085.18-1085.69 neuper@37906: thm.ML:1092.34 neuper@37906: goals.ML:536.61 neuper@37906: neuper@37906: > val bdv = (the o (parse thy)) "bdv::nat"; neuper@37906: > val x = (the o (parse thy)) "x::nat"; neuper@37906: > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add) neuper@37906: handle e => print_exn e; neuper@37906: uncaught exception THM neuper@37906: raised at: thm.ML:1085.18-1085.69 neuper@37906: thm.ML:1092.34 neuper@37906: goals.ML:536.61 neuper@37906: neuper@37906: > (instantiate' [SOME ctyp] [] isolate_bdv_add) neuper@37906: handle e => print_exn e; neuper@37906: uncaught exception TYPE neuper@37906: raised at: drule.ML:613.13-615.44 neuper@37906: goals.ML:536.61 neuper@37906: neuper@37906: > val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat"; neuper@37906: *) neuper@37906: neuper@37906: (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst neuper@37906: thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) neuper@37906: fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls') neuper@37906: (put_asm:bool) subs (thm:thm') (ct:cterm') = neuper@37906: let neuper@37906: val thy = (the o assoc')(!theory',thy'); neuper@37906: val thm = assoc_thm' thy thm; (*28.10.02*) neuper@37906: (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*) neuper@37906: in neuper@37906: case rewrite_ thy neuper@37906: ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls)) neuper@37906: put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of neuper@37906: NONE => NONE neuper@37906: | SOME (ctm, ctms) => neuper@37906: SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list) neuper@37906: end; neuper@37906: neuper@37906: (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst neuper@37906: thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) neuper@37906: fun rewrite_set_inst (thy':theory') (put_asm:bool) neuper@37906: subs' (rls:rls') (ct:cterm') = neuper@37906: let neuper@37906: val thy = (the o assoc')(!theory',thy'); neuper@37906: val rls = assoc_rls rls neuper@37906: val subst = subs'2subst thy subs' neuper@37906: (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*) neuper@37906: in case rewrite_set_inst_ thy put_asm subst (*sub*)rls neuper@37906: ((term_of o the o (parse thy)) ct) of neuper@37906: NONE => NONE neuper@37906: | SOME (t, ts) => SOME (term2str t, terms2str ts) neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: (*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *) neuper@37906: fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true neuper@37906: neuper@37906: | eval_true' (thy':theory') (rls':rls') (t:term) = neuper@37906: (* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres'; neuper@37906: *) neuper@37906: let val ct' = term2str t; neuper@37906: in case rewrite_set thy' false rls' ct' of neuper@37906: SOME ("True",_) => true neuper@37906: | _ => false neuper@37906: end; neuper@37906: fun eval_true_ _ _ (Const ("True",_)) = true neuper@37906: | eval_true_ (thy':theory') rls t = neuper@37906: case rewrite_set_ (assoc_thy thy') false rls t of neuper@37906: SOME (Const ("True",_),_) => true neuper@37906: | _ => false; neuper@37906: neuper@37906: (* neuper@37906: val test_rls = neuper@37906: Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right), neuper@37906: rules = [Calc ("matches",eval_matches "") neuper@37906: ], neuper@37906: scr = Script ((term_of o the o (parse thy)) neuper@37906: "empty_script") neuper@37906: }:rls; neuper@37906: neuper@37906: neuper@37906: neuper@37906: rewrite_set_ Isac.thy eval_rls false test_rls neuper@37906: ((the o (parse thy)) "matches (?a = ?b) (x = #0)"); neuper@37906: val xxx = (term_of o the o (parse thy)) neuper@37906: "matches (?a = ?b) (x = #0)"; neuper@37906: eval_matches """" xxx thy; neuper@37906: SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True", neuper@37906: Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#))) neuper@37906: neuper@37906: neuper@37906: neuper@37906: rewrite_set_ Isac.thy eval_rls false eval_rls neuper@37906: ((the o (parse thy)) "contains_root (sqrt #0)"); neuper@37906: val it = SOME ("True",[]) : (cterm * cterm list) option neuper@37906: neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise neuper@37906: datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03 neuper@37906: introduced with quick-and-dirty code*) neuper@37906: fun determine dts = neuper@37906: let val false_indet = neuper@37906: filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts neuper@37906: val ts = map (#2: det * term -> term) dts neuper@37906: in if nil = false_indet then (TRUE, ts) neuper@37906: else if nil = filter ((curry op= FALSE) o (#1:det * term -> det)) neuper@37906: false_indet neuper@37906: then (INDET, ts) neuper@37906: else (FALSE, ts) end; neuper@37906: (* val dts = [(INDET,e_term), (FALSE,HOLogic.false_const), neuper@37906: (INDET,e_term), (TRUE,HOLogic.true_const)]; neuper@37906: determine dts; neuper@37906: val it = neuper@37906: (FALSE, neuper@37906: [Const ("empty","'a"),Const ("False","bool"),Const ("empty","'a"), neuper@37906: Const ("True","bool")]) : det * term list*) neuper@37906: neuper@37906: fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*) neuper@37906: if cs = [HOLogic.true_const] orelse cs = [] then (TRUE, []) neuper@37906: else if cs = [HOLogic.false_const] then (FALSE, cs) neuper@37906: else neuper@37906: let fun eval t = neuper@37906: let val taopt = rewrite__set_ thy 1 false [] rls t neuper@37906: in case taopt of neuper@37906: SOME (t,_) => neuper@37906: if t = HOLogic.true_const then (TRUE, t) neuper@37906: else if t = HOLogic.false_const then (FALSE, t) neuper@37906: else (INDET, t) neuper@37906: | NONE => (INDET, t) end neuper@37906: in (determine o (map eval)) cs end; neuper@37906: WN.16.5.0-------------------------------------------------------------*)