wenzelm@29265: (* Title: FOLP/simp.ML clasohm@0: Author: Tobias Nipkow clasohm@0: Copyright 1993 University of Cambridge clasohm@0: clasohm@0: FOLP version of... clasohm@0: clasohm@0: Generic simplifier, suitable for most logics. (from Provers) clasohm@0: clasohm@0: This version allows instantiation of Vars in the subgoal, since the proof clasohm@0: term must change. clasohm@0: *) clasohm@0: clasohm@0: signature SIMP_DATA = clasohm@0: sig clasohm@0: val case_splits : (thm * string) list clasohm@0: val dest_red : term -> term * term * term clasohm@0: val mk_rew_rules : thm -> thm list clasohm@0: val norm_thms : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *) clasohm@0: val red1 : thm (* ?P>>?Q ==> ?P ==> ?Q *) clasohm@0: val red2 : thm (* ?P>>?Q ==> ?Q ==> ?P *) clasohm@0: val refl_thms : thm list clasohm@0: val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) clasohm@0: val trans_thms : thm list clasohm@0: end; clasohm@0: clasohm@0: clasohm@0: infix 4 addrews addcongs delrews delcongs setauto; clasohm@0: clasohm@0: signature SIMP = clasohm@0: sig clasohm@0: type simpset clasohm@0: val empty_ss : simpset clasohm@0: val addcongs : simpset * thm list -> simpset clasohm@0: val addrews : simpset * thm list -> simpset clasohm@0: val delcongs : simpset * thm list -> simpset clasohm@0: val delrews : simpset * thm list -> simpset clasohm@0: val dest_ss : simpset -> thm list * thm list clasohm@0: val print_ss : simpset -> unit clasohm@0: val setauto : simpset * (int -> tactic) -> simpset clasohm@0: val ASM_SIMP_CASE_TAC : simpset -> int -> tactic clasohm@0: val ASM_SIMP_TAC : simpset -> int -> tactic clasohm@0: val CASE_TAC : simpset -> int -> tactic clasohm@0: val SIMP_CASE2_TAC : simpset -> int -> tactic clasohm@0: val SIMP_THM : simpset -> thm -> thm clasohm@0: val SIMP_TAC : simpset -> int -> tactic clasohm@0: val SIMP_CASE_TAC : simpset -> int -> tactic clasohm@0: val mk_congs : theory -> string list -> thm list clasohm@0: val mk_typed_congs : theory -> (string * string) list -> thm list clasohm@0: (* temporarily disabled: clasohm@0: val extract_free_congs : unit -> thm list clasohm@0: *) wenzelm@32740: val tracing : bool Unsynchronized.ref clasohm@0: end; clasohm@0: wenzelm@32449: functor SimpFun (Simp_data: SIMP_DATA) : SIMP = clasohm@0: struct clasohm@0: wenzelm@19805: local open Simp_data in clasohm@0: clasohm@0: (*For taking apart reductions into left, right hand sides*) clasohm@0: val lhs_of = #2 o dest_red; clasohm@0: val rhs_of = #3 o dest_red; clasohm@0: clasohm@0: (*** Indexing and filtering of theorems ***) clasohm@0: wenzelm@22360: fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); clasohm@0: clasohm@0: (*insert a thm in a discrimination net by its lhs*) wenzelm@33339: fun lhs_insert_thm th net = wenzelm@16800: Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net clasohm@0: handle Net.INSERT => net; clasohm@0: clasohm@0: (*match subgoal i against possible theorems in the net. clasohm@0: Similar to match_from_nat_tac, but the net does not contain numbers; clasohm@0: rewrite rules are not ordered.*) clasohm@0: fun net_tac net = wenzelm@32449: SUBGOAL(fn (prem,i) => wenzelm@19805: resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i); clasohm@0: clasohm@0: (*match subgoal i against possible theorems indexed by lhs in the net*) clasohm@0: fun lhs_net_tac net = wenzelm@32449: SUBGOAL(fn (prem,i) => clasohm@1459: biresolve_tac (Net.unify_term net wenzelm@19805: (lhs_of (Logic.strip_assums_concl prem))) i); clasohm@0: wenzelm@42364: fun nth_subgoal i thm = nth (prems_of thm) (i - 1); clasohm@0: wenzelm@19805: fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm); clasohm@0: clasohm@0: fun lhs_of_eq i thm = lhs_of(goal_concl i thm) clasohm@0: and rhs_of_eq i thm = rhs_of(goal_concl i thm); clasohm@0: clasohm@0: fun var_lhs(thm,i) = clasohm@0: let fun var(Var _) = true clasohm@0: | var(Abs(_,_,t)) = var t clasohm@0: | var(f$_) = var f clasohm@0: | var _ = false; clasohm@0: in var(lhs_of_eq i thm) end; clasohm@0: clasohm@0: fun contains_op opns = haftmann@36692: let fun contains(Const(s,_)) = member (op =) opns s | clasohm@0: contains(s$t) = contains s orelse contains t | clasohm@0: contains(Abs(_,_,t)) = contains t | clasohm@0: contains _ = false; clasohm@0: in contains end; clasohm@0: clasohm@0: fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i; clasohm@0: clasohm@0: val (normI_thms,normE_thms) = split_list norm_thms; clasohm@0: clasohm@0: (*Get the norm constants from norm_thms*) clasohm@0: val norms = wenzelm@32449: let fun norm thm = clasohm@0: case lhs_of(concl_of thm) of clasohm@1459: Const(n,_)$_ => n wenzelm@32091: | _ => error "No constant in lhs of a norm_thm" clasohm@0: in map norm normE_thms end; clasohm@0: clasohm@0: fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of haftmann@36692: Const(s,_)$_ => member (op =) norms s | _ => false; clasohm@0: clasohm@0: val refl_tac = resolve_tac refl_thms; clasohm@0: clasohm@0: fun find_res thms thm = wenzelm@32091: let fun find [] = error "Check Simp_Data" wenzelm@6969: | find(th::thms) = thm RS th handle THM _ => find thms clasohm@0: in find thms end; clasohm@0: clasohm@0: val mk_trans = find_res trans_thms; clasohm@0: clasohm@0: fun mk_trans2 thm = clasohm@0: let fun mk[] = error"Check transitivity" wenzelm@6969: | mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts clasohm@0: in mk trans_thms end; clasohm@0: clasohm@0: (*Applies tactic and returns the first resulting state, FAILS if none!*) wenzelm@4271: fun one_result(tac,thm) = case Seq.pull(tac thm) of skalberg@15531: SOME(thm',_) => thm' skalberg@15531: | NONE => raise THM("Simplifier: could not continue", 0, [thm]); clasohm@0: clasohm@0: fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm); clasohm@0: clasohm@0: clasohm@0: (**** Adding "NORM" tags ****) clasohm@0: clasohm@0: (*get name of the constant from conclusion of a congruence rule*) wenzelm@32449: fun cong_const cong = clasohm@0: case head_of (lhs_of (concl_of cong)) of clasohm@1459: Const(c,_) => c clasohm@1459: | _ => "" (*a placeholder distinct from const names*); clasohm@0: clasohm@0: (*true if the term is an atomic proposition (no ==> signs) *) wenzelm@19805: val atomic = null o Logic.strip_assums_hyp; clasohm@0: clasohm@0: (*ccs contains the names of the constants possessing congruence rules*) clasohm@0: fun add_hidden_vars ccs = haftmann@21078: let fun add_hvars tm hvars = case tm of wenzelm@44121: Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars) wenzelm@32449: | _$_ => let val (f,args) = strip_comb tm clasohm@1459: in case f of wenzelm@32449: Const(c,T) => haftmann@21078: if member (op =) ccs c haftmann@21078: then fold_rev add_hvars args hvars wenzelm@44121: else Misc_Legacy.add_term_vars (tm, hvars) wenzelm@44121: | _ => Misc_Legacy.add_term_vars (tm, hvars) clasohm@1459: end clasohm@1459: | _ => hvars; clasohm@0: in add_hvars end; clasohm@0: clasohm@0: fun add_new_asm_vars new_asms = haftmann@21078: let fun itf (tm, at) vars = wenzelm@44121: if at then vars else Misc_Legacy.add_term_vars(tm,vars) clasohm@1459: fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm clasohm@1459: in if length(tml)=length(al) haftmann@21078: then fold_rev itf (tml ~~ al) vars clasohm@1459: else vars clasohm@1459: end clasohm@1459: fun add_vars (tm,vars) = case tm of clasohm@1459: Abs (_,_,body) => add_vars(body,vars) clasohm@1459: | r$s => (case head_of tm of haftmann@17325: Const(c,T) => (case AList.lookup (op =) new_asms c of skalberg@15531: NONE => add_vars(r,add_vars(s,vars)) skalberg@15531: | SOME(al) => add_list(tm,al,vars)) clasohm@1459: | _ => add_vars(r,add_vars(s,vars))) clasohm@1459: | _ => vars clasohm@0: in add_vars end; clasohm@0: clasohm@0: clasohm@0: fun add_norms(congs,ccs,new_asms) thm = clasohm@0: let val thm' = mk_trans2 thm; clasohm@0: (* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *) clasohm@0: val nops = nprems_of thm' clasohm@0: val lhs = rhs_of_eq 1 thm' clasohm@0: val rhs = lhs_of_eq nops thm' clasohm@0: val asms = tl(rev(tl(prems_of thm'))) haftmann@21078: val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] clasohm@0: val hvars = add_new_asm_vars new_asms (rhs,hvars) haftmann@21078: fun it_asms asm hvars = clasohm@1459: if atomic asm then add_new_asm_vars new_asms (asm,hvars) wenzelm@44121: else Misc_Legacy.add_term_frees(asm,hvars) haftmann@21078: val hvars = fold_rev it_asms asms hvars clasohm@0: val hvs = map (#1 o dest_Var) hvars clasohm@0: val refl1_tac = refl_tac 1 paulson@3537: fun norm_step_tac st = st |> wenzelm@32449: (case head_of(rhs_of_eq 1 st) of haftmann@36692: Var(ixn,_) => if member (op =) hvs ixn then refl1_tac wenzelm@32449: else resolve_tac normI_thms 1 ORELSE refl1_tac wenzelm@32449: | Const _ => resolve_tac normI_thms 1 ORELSE wenzelm@32449: resolve_tac congs 1 ORELSE refl1_tac wenzelm@32449: | Free _ => resolve_tac congs 1 ORELSE refl1_tac wenzelm@32449: | _ => refl1_tac) paulson@3537: val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac skalberg@15531: val SOME(thm'',_) = Seq.pull(add_norm_tac thm') clasohm@0: in thm'' end; clasohm@0: clasohm@0: fun add_norm_tags congs = clasohm@0: let val ccs = map cong_const congs wenzelm@33317: val new_asms = filter (exists not o #2) clasohm@1459: (ccs ~~ (map (map atomic o prems_of) congs)); clasohm@0: in add_norms(congs,ccs,new_asms) end; clasohm@0: clasohm@0: fun normed_rews congs = wenzelm@19925: let val add_norms = add_norm_tags congs in wenzelm@21287: fn thm => Variable.tradeT wenzelm@36603: (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm] clasohm@0: end; clasohm@0: clasohm@1459: fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; clasohm@0: clasohm@0: val trans_norms = map mk_trans normE_thms; clasohm@0: clasohm@0: clasohm@0: (* SIMPSET *) clasohm@0: clasohm@0: datatype simpset = clasohm@1459: SS of {auto_tac: int -> tactic, clasohm@1459: congs: thm list, clasohm@1459: cong_net: thm Net.net, clasohm@1459: mk_simps: thm -> thm list, clasohm@1459: simps: (thm * thm list) list, clasohm@1459: simp_net: thm Net.net} clasohm@0: clasohm@0: val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty, clasohm@1459: mk_simps=normed_rews[], simps=[], simp_net=Net.empty}; clasohm@0: clasohm@0: (** Insertion of congruences and rewrites **) clasohm@0: clasohm@0: (*insert a thm in a thm net*) wenzelm@32449: fun insert_thm_warn th net = wenzelm@22360: Net.insert_term Thm.eq_thm_prop (concl_of th, th) net wenzelm@32449: handle Net.INSERT => wenzelm@32091: (writeln ("Duplicate rewrite or congruence rule:\n" ^ wenzelm@32091: Display.string_of_thm_without_context th); net); clasohm@0: haftmann@21078: val insert_thms = fold_rev insert_thm_warn; clasohm@0: wenzelm@33245: fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = clasohm@0: let val thms = mk_simps thm clasohm@0: in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, haftmann@21078: simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} clasohm@0: end; clasohm@0: wenzelm@33245: fun ss addrews thms = fold addrew thms ss; clasohm@0: clasohm@0: fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = clasohm@0: let val congs' = thms @ congs; clasohm@0: in SS{auto_tac=auto_tac, congs= congs', haftmann@21078: cong_net= insert_thms (map mk_trans thms) cong_net, clasohm@0: mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} clasohm@0: end; clasohm@0: clasohm@0: (** Deletion of congruences and rewrites **) clasohm@0: clasohm@0: (*delete a thm from a thm net*) wenzelm@32449: fun delete_thm_warn th net = wenzelm@22360: Net.delete_term Thm.eq_thm_prop (concl_of th, th) net wenzelm@32449: handle Net.DELETE => wenzelm@32091: (writeln ("No such rewrite or congruence rule:\n" ^ wenzelm@32091: Display.string_of_thm_without_context th); net); clasohm@0: haftmann@21078: val delete_thms = fold_rev delete_thm_warn; clasohm@0: clasohm@0: fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = wenzelm@22360: let val congs' = fold (remove Thm.eq_thm_prop) thms congs clasohm@0: in SS{auto_tac=auto_tac, congs= congs', haftmann@21078: cong_net= delete_thms (map mk_trans thms) cong_net, clasohm@0: mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} clasohm@0: end; clasohm@0: wenzelm@33245: fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = clasohm@0: let fun find((p as (th,ths))::ps',ps) = wenzelm@22360: if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) wenzelm@32091: | find([],simps') = wenzelm@32091: (writeln ("No such rewrite or congruence rule:\n" ^ wenzelm@32091: Display.string_of_thm_without_context thm); ([], simps')) clasohm@0: val (thms,simps') = find(simps,[]) clasohm@0: in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, haftmann@21078: simps = simps', simp_net = delete_thms thms simp_net } clasohm@0: end; clasohm@0: wenzelm@33245: fun ss delrews thms = fold delrew thms ss; clasohm@0: clasohm@0: clasohm@0: fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) = clasohm@0: SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, clasohm@0: simps=simps, simp_net=simp_net}; clasohm@0: clasohm@0: clasohm@0: (** Inspection of a simpset **) clasohm@0: clasohm@0: fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); clasohm@0: clasohm@0: fun print_ss(SS{congs,simps,...}) = wenzelm@32091: writeln (cat_lines wenzelm@32091: (["Congruences:"] @ map Display.string_of_thm_without_context congs @ wenzelm@32091: ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps)); clasohm@0: clasohm@0: clasohm@0: (* Rewriting with conditionals *) clasohm@0: clasohm@0: val (case_thms,case_consts) = split_list case_splits; clasohm@0: val case_rews = map mk_trans case_thms; clasohm@0: clasohm@0: fun if_rewritable ifc i thm = clasohm@0: let val tm = goal_concl i thm clasohm@1459: fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1) clasohm@1459: | nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k) clasohm@1459: | nobound(Bound n,j,k) = n < k orelse k+j <= n clasohm@1459: | nobound(_) = true; clasohm@1459: fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al clasohm@1459: fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1) clasohm@1459: | find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in clasohm@1459: case f of Const(c,_) => if c=ifc then check_args(al,j) clasohm@1459: else find_if(s,j) orelse find_if(t,j) clasohm@1459: | _ => find_if(s,j) orelse find_if(t,j) end clasohm@1459: | find_if(_) = false; clasohm@0: in find_if(tm,0) end; clasohm@0: clasohm@0: fun IF1_TAC cong_tac i = wenzelm@32449: let fun seq_try (ifth::ifths,ifc::ifcs) thm = paulson@1512: (COND (if_rewritable ifc i) (DETERM(rtac ifth i)) paulson@1512: (seq_try(ifths,ifcs))) thm paulson@1512: | seq_try([],_) thm = no_tac thm paulson@1512: and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm clasohm@1459: and one_subt thm = clasohm@1459: let val test = has_fewer_prems (nprems_of thm + 1) wenzelm@32449: fun loop thm = wenzelm@32449: COND test no_tac paulson@1512: ((try_rew THEN DEPTH_FIRST test (refl_tac i)) wenzelm@32449: ORELSE (refl_tac i THEN loop)) thm paulson@1512: in (cong_tac THEN loop) thm end paulson@1512: in COND (may_match(case_consts,i)) try_rew no_tac end; clasohm@0: clasohm@0: fun CASE_TAC (SS{cong_net,...}) i = clasohm@0: let val cong_tac = net_tac cong_net i clasohm@0: in NORM (IF1_TAC cong_tac) i end; clasohm@0: clasohm@0: (* Rewriting Automaton *) clasohm@0: clasohm@0: datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE clasohm@1459: | PROVE | POP_CS | POP_ARTR | IF; wenzelm@22578: clasohm@0: fun simp_refl([],_,ss) = ss clasohm@0: | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) clasohm@1459: else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); clasohm@0: clasohm@0: (** Tracing **) clasohm@0: wenzelm@32740: val tracing = Unsynchronized.ref false; clasohm@0: clasohm@0: (*Replace parameters by Free variables in P*) clasohm@0: fun variants_abs ([],P) = P clasohm@0: | variants_abs ((a,T)::aTs, P) = wenzelm@42284: variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P))); clasohm@0: clasohm@0: (*Select subgoal i from proof state; substitute parameters, for printing*) clasohm@0: fun prepare_goal i st = clasohm@0: let val subgi = nth_subgoal i st wenzelm@19805: val params = rev (Logic.strip_params subgi) wenzelm@19805: in variants_abs (params, Logic.strip_assums_concl subgi) end; clasohm@0: clasohm@0: (*print lhs of conclusion of subgoal i*) clasohm@0: fun pr_goal_lhs i st = wenzelm@32449: writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) clasohm@1459: (lhs_of (prepare_goal i st))); clasohm@0: clasohm@0: (*print conclusion of subgoal i*) clasohm@0: fun pr_goal_concl i st = wenzelm@32449: writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) clasohm@0: clasohm@0: (*print subgoals i to j (inclusive)*) clasohm@0: fun pr_goals (i,j) st = clasohm@0: if i>j then () clasohm@0: else (pr_goal_concl i st; pr_goals (i+1,j) st); clasohm@0: clasohm@0: (*Print rewrite for tracing; i=subgoal#, n=number of new subgoals, clasohm@0: thm=old state, thm'=new state *) clasohm@0: fun pr_rew (i,n,thm,thm',not_asms) = clasohm@0: if !tracing clasohm@0: then (if not_asms then () else writeln"Assumption used in"; clasohm@0: pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm'; clasohm@1459: if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm') clasohm@0: else (); clasohm@0: writeln"" ) clasohm@0: else (); clasohm@0: clasohm@0: (* Skip the first n hyps of a goal, and return the rest in generalized form *) wenzelm@56245: fun strip_varify(Const(@{const_name Pure.imp}, _) $ H $ B, n, vs) = clasohm@1459: if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) clasohm@1459: else strip_varify(B,n-1,vs) wenzelm@56245: | strip_varify(Const(@{const_name Pure.all},_)$Abs(_,T,t), n, vs) = clasohm@1459: strip_varify(t,n,Var(("?",length vs),T)::vs) clasohm@0: | strip_varify _ = []; clasohm@0: clasohm@0: fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let clasohm@0: clasohm@0: fun simp_lhs(thm,ss,anet,ats,cs) = clasohm@0: if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else clasohm@0: if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs) wenzelm@4271: else case Seq.pull(cong_tac i thm) of skalberg@15531: SOME(thm',_) => haftmann@33955: let val ps = prems_of thm haftmann@33955: and ps' = prems_of thm'; clasohm@1459: val n = length(ps')-length(ps); wenzelm@42364: val a = length(Logic.strip_assums_hyp(nth ps (i - 1))) haftmann@33955: val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps')); clasohm@1459: in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end skalberg@15531: | NONE => (REW::ss,thm,anet,ats,cs); clasohm@0: clasohm@0: (*NB: the "Adding rewrites:" trace will look strange because assumptions clasohm@0: are represented by rules, generalized over their parameters*) clasohm@0: fun add_asms(ss,thm,a,anet,ats,cs) = clasohm@0: let val As = strip_varify(nth_subgoal i thm, a, []); wenzelm@36945: val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As; wenzelm@32952: val new_rws = maps mk_rew_rules thms; wenzelm@32952: val rwrls = map mk_trans (maps mk_rew_rules thms); wenzelm@33339: val anet' = fold_rev lhs_insert_thm rwrls anet; clasohm@0: in if !tracing andalso not(null new_rws) wenzelm@32091: then writeln (cat_lines wenzelm@32091: ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws)) clasohm@1459: else (); wenzelm@32449: (ss,thm,anet',anet::ats,cs) clasohm@0: end; clasohm@0: wenzelm@4271: fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of skalberg@15531: SOME(thm',seq') => clasohm@1459: let val n = (nprems_of thm') - (nprems_of thm) clasohm@1459: in pr_rew(i,n,thm,thm',more); clasohm@1459: if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) clasohm@1459: else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), clasohm@1459: thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) clasohm@1459: end skalberg@15531: | NONE => if more paulson@1512: then rew((lhs_net_tac anet i THEN assume_tac i) thm, clasohm@1459: thm,ss,anet,ats,cs,false) clasohm@1459: else (ss,thm,anet,ats,cs); clasohm@0: clasohm@0: fun try_true(thm,ss,anet,ats,cs) = wenzelm@4271: case Seq.pull(auto_tac i thm) of skalberg@15531: SOME(thm',_) => (ss,thm',anet,ats,cs) skalberg@15531: | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs clasohm@1459: in if !tracing clasohm@1459: then (writeln"*** Failed to prove precondition. Normal form:"; clasohm@1459: pr_goal_concl i thm; writeln"") clasohm@1459: else (); clasohm@1459: rew(seq,thm0,ss0,anet0,ats0,cs0,more) clasohm@1459: end; clasohm@0: clasohm@0: fun if_exp(thm,ss,anet,ats,cs) = wenzelm@4271: case Seq.pull (IF1_TAC (cong_tac i) i thm) of skalberg@15531: SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) skalberg@15531: | NONE => (ss,thm,anet,ats,cs); clasohm@0: clasohm@0: fun step(s::ss, thm, anet, ats, cs) = case s of clasohm@1459: MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) clasohm@1459: | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) clasohm@1459: | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) paulson@1512: | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) clasohm@1459: | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) clasohm@1459: | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) clasohm@1459: | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss clasohm@1459: else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs) clasohm@1459: | POP_ARTR => (ss,thm,hd ats,tl ats,cs) clasohm@1459: | POP_CS => (ss,thm,anet,ats,tl cs) clasohm@1459: | IF => if_exp(thm,ss,anet,ats,cs); clasohm@0: clasohm@0: fun exec(state as (s::ss, thm, _, _, _)) = clasohm@1459: if s=STOP then thm else exec(step(state)); clasohm@0: clasohm@0: in exec(ss, thm, Net.empty, [], []) end; clasohm@0: clasohm@0: clasohm@0: fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = clasohm@0: let val cong_tac = net_tac cong_net wenzelm@32449: in fn i => paulson@1512: (fn thm => wenzelm@4271: if i <= 0 orelse nprems_of thm < i then Seq.empty wenzelm@4271: else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) paulson@1512: THEN TRY(auto_tac i) clasohm@0: end; clasohm@0: clasohm@0: val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false); clasohm@0: val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); clasohm@0: clasohm@0: val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); clasohm@0: val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); clasohm@0: clasohm@0: val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); clasohm@0: clasohm@0: fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = clasohm@0: let val cong_tac = net_tac cong_net clasohm@0: in fn thm => let val state = thm RSN (2,red1) clasohm@1459: in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end clasohm@0: end; clasohm@0: clasohm@0: val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false); clasohm@0: clasohm@0: clasohm@0: (* Compute Congruence rules for individual constants using the substition clasohm@0: rules *) clasohm@0: wenzelm@35021: val subst_thms = map Drule.export_without_context subst_thms; clasohm@0: clasohm@0: clasohm@0: fun exp_app(0,t) = t clasohm@0: | exp_app(i,t) = exp_app(i-1,t $ Bound (i-1)); clasohm@0: clasohm@0: fun exp_abs(Type("fun",[T1,T2]),t,i) = clasohm@1459: Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) clasohm@0: | exp_abs(T,t,i) = exp_app(i,t); clasohm@0: clasohm@0: fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0); clasohm@0: clasohm@0: clasohm@0: fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = clasohm@0: let fun xn_list(x,n) = haftmann@33063: let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1); haftmann@33955: in ListPair.map eta_Var (ixs, take (n+1) Ts) end clasohm@0: val lhs = list_comb(f,xn_list("X",k-1)) clasohm@0: val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) clasohm@0: in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; clasohm@0: wenzelm@16931: fun find_subst sg T = clasohm@0: let fun find (thm::thms) = clasohm@1459: let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); wenzelm@44121: val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, [])); clasohm@1459: val eqT::_ = binder_types cT wenzelm@16931: in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) clasohm@1459: else find thms clasohm@1459: end skalberg@15531: | find [] = NONE clasohm@0: in find subst_thms end; clasohm@0: clasohm@0: fun mk_cong sg (f,aTs,rT) (refl,eq) = wenzelm@16931: let val k = length aTs; clasohm@0: fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = clasohm@1459: let val ca = cterm_of sg va clasohm@1459: and cx = cterm_of sg (eta_Var(("X"^si,0),T)) clasohm@1459: val cb = cterm_of sg vb clasohm@1459: and cy = cterm_of sg (eta_Var(("Y"^si,0),T)) clasohm@1459: val cP = cterm_of sg P clasohm@1459: and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) clasohm@1459: in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; clasohm@0: fun mk(c,T::Ts,i,yik) = clasohm@1459: let val si = radixstring(26,"a",i) wenzelm@16931: in case find_subst sg T of skalberg@15531: NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) skalberg@15531: | SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) clasohm@1459: in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end clasohm@1459: end clasohm@0: | mk(c,[],_,_) = c; clasohm@0: in mk(refl,rev aTs,k-1,[]) end; clasohm@0: clasohm@0: fun mk_cong_type sg (f,T) = clasohm@0: let val (aTs,rT) = strip_type T; clasohm@0: fun find_refl(r::rs) = clasohm@1459: let val (Const(eq,eqT),_,_) = dest_red(concl_of r) wenzelm@16931: in if Sign.typ_instance sg (rT, hd(binder_types eqT)) skalberg@15531: then SOME(r,(eq,body_type eqT)) else find_refl rs clasohm@1459: end skalberg@15531: | find_refl([]) = NONE; clasohm@0: in case find_refl refl_thms of skalberg@15531: NONE => [] | SOME(refl) => [mk_cong sg (f,aTs,rT) refl] clasohm@0: end; clasohm@0: clasohm@0: fun mk_cong_thy thy f = wenzelm@22578: let val T = case Sign.const_type thy f of skalberg@15531: NONE => error(f^" not declared") | SOME(T) => T; wenzelm@16876: val T' = Logic.incr_tvar 9 T; wenzelm@22578: in mk_cong_type thy (Const(f,T'),T') end; clasohm@0: wenzelm@32952: fun mk_congs thy = maps (mk_cong_thy thy); clasohm@0: clasohm@0: fun mk_typed_congs thy = wenzelm@22675: let wenzelm@22675: fun readfT(f,s) = wenzelm@22675: let wenzelm@24707: val T = Logic.incr_tvar 9 (Syntax.read_typ_global thy s); wenzelm@22675: val t = case Sign.const_type thy f of wenzelm@22675: SOME(_) => Const(f,T) | NONE => Free(f,T) wenzelm@22675: in (t,T) end wenzelm@32952: in maps (mk_cong_type thy o readfT) end; clasohm@0: wenzelm@22675: end; wenzelm@22675: end;