src/Provers/simp.ML
 author wenzelm Sat Jul 10 21:44:26 1999 +0200 (1999-07-10 ago) changeset 6966 cfa87aef9ccd parent 5961 6cf4e46ce95a child 7645 c67115c0e105 permissions -rw-r--r--
handle THM exn;
 clasohm@0 ` 1` ```(* Title: Provers/simp ``` clasohm@0 ` 2` ``` Author: Tobias Nipkow ``` clasohm@0 ` 3` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 4` clasohm@0 ` 5` ```Generic simplifier, suitable for most logics. The only known exception is ``` clasohm@0 ` 6` ```Constructive Type Theory. The reflexivity axiom must be unconditional, ``` clasohm@0 ` 7` ```namely a=a not a:A ==> a=a:A. Used typedsimp.ML otherwise. ``` clasohm@0 ` 8` ```*) ``` clasohm@0 ` 9` clasohm@0 ` 10` ```signature SIMP_DATA = ``` clasohm@0 ` 11` ```sig ``` clasohm@0 ` 12` ``` val dest_red : term -> term * term * term ``` clasohm@0 ` 13` ``` val mk_rew_rules : thm -> thm list ``` clasohm@0 ` 14` ``` val norm_thms : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *) ``` clasohm@0 ` 15` ``` val red1 : thm (* ?P>>?Q ==> ?P ==> ?Q *) ``` clasohm@0 ` 16` ``` val red2 : thm (* ?P>>?Q ==> ?Q ==> ?P *) ``` clasohm@0 ` 17` ``` val refl_thms : thm list ``` clasohm@0 ` 18` ``` val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) ``` clasohm@0 ` 19` ``` val trans_thms : thm list ``` clasohm@0 ` 20` ```end; ``` clasohm@0 ` 21` clasohm@0 ` 22` clasohm@0 ` 23` ```infix 4 addrews addcongs addsplits delrews delcongs setauto; ``` clasohm@0 ` 24` clasohm@0 ` 25` ```signature SIMP = ``` clasohm@0 ` 26` ```sig ``` clasohm@0 ` 27` ``` type simpset ``` clasohm@0 ` 28` ``` val empty_ss : simpset ``` clasohm@0 ` 29` ``` val addcongs : simpset * thm list -> simpset ``` clasohm@0 ` 30` ``` val addrews : simpset * thm list -> simpset ``` clasohm@0 ` 31` ``` val addsplits : simpset * thm list -> simpset ``` clasohm@0 ` 32` ``` val delcongs : simpset * thm list -> simpset ``` clasohm@0 ` 33` ``` val delrews : simpset * thm list -> simpset ``` clasohm@0 ` 34` ``` val dest_ss : simpset -> thm list * thm list ``` clasohm@0 ` 35` ``` val print_ss : simpset -> unit ``` clasohm@0 ` 36` ``` val setauto : simpset * (thm list -> int -> tactic) -> simpset ``` clasohm@0 ` 37` ``` val ASM_SIMP_TAC : simpset -> int -> tactic ``` clasohm@0 ` 38` ``` val SPLIT_TAC : simpset -> int -> tactic ``` clasohm@0 ` 39` ``` val SIMP_SPLIT2_TAC : simpset -> int -> tactic ``` clasohm@0 ` 40` ``` val SIMP_THM : simpset -> thm -> thm ``` clasohm@0 ` 41` ``` val SIMP_TAC : simpset -> int -> tactic ``` clasohm@0 ` 42` ``` val mk_congs : theory -> string list -> thm list ``` clasohm@0 ` 43` ``` val mk_typed_congs : theory -> (string * string) list -> thm list ``` clasohm@0 ` 44` ```(* temporarily disabled: ``` clasohm@0 ` 45` ``` val extract_free_congs : unit -> thm list ``` clasohm@0 ` 46` ```*) ``` clasohm@0 ` 47` ``` val tracing : bool ref ``` clasohm@0 ` 48` ```end; ``` clasohm@0 ` 49` clasohm@0 ` 50` ```functor SimpFun (Simp_data: SIMP_DATA) : SIMP = ``` clasohm@0 ` 51` ```struct ``` clasohm@0 ` 52` clasohm@0 ` 53` ```local open Simp_data Logic in ``` clasohm@0 ` 54` clasohm@0 ` 55` ```(*For taking apart reductions into left, right hand sides*) ``` clasohm@0 ` 56` ```val lhs_of = #2 o dest_red; ``` clasohm@0 ` 57` ```val rhs_of = #3 o dest_red; ``` clasohm@0 ` 58` clasohm@0 ` 59` ```(*** Indexing and filtering of theorems ***) ``` clasohm@0 ` 60` clasohm@0 ` 61` ```fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2); ``` clasohm@0 ` 62` clasohm@0 ` 63` ```(*insert a thm in a discrimination net by its lhs*) ``` clasohm@0 ` 64` ```fun lhs_insert_thm (th,net) = ``` clasohm@0 ` 65` ``` Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl) ``` clasohm@0 ` 66` ``` handle Net.INSERT => net; ``` clasohm@0 ` 67` clasohm@0 ` 68` ```(*match subgoal i against possible theorems in the net. ``` clasohm@0 ` 69` ``` Similar to match_from_nat_tac, but the net does not contain numbers; ``` clasohm@0 ` 70` ``` rewrite rules are not ordered.*) ``` clasohm@0 ` 71` ```fun net_tac net = ``` clasohm@0 ` 72` ``` SUBGOAL(fn (prem,i) => ``` clasohm@0 ` 73` ``` match_tac (Net.match_term net (strip_assums_concl prem)) i); ``` clasohm@0 ` 74` clasohm@0 ` 75` ```(*match subgoal i against possible theorems indexed by lhs in the net*) ``` clasohm@0 ` 76` ```fun lhs_net_tac net = ``` clasohm@0 ` 77` ``` SUBGOAL(fn (prem,i) => ``` clasohm@0 ` 78` ``` bimatch_tac (Net.match_term net ``` clasohm@0 ` 79` ``` (lhs_of (strip_assums_concl prem))) i); ``` clasohm@0 ` 80` clasohm@0 ` 81` ```fun nth_subgoal i thm = nth_elem(i-1,prems_of thm); ``` clasohm@0 ` 82` clasohm@0 ` 83` ```fun goal_concl i thm = strip_assums_concl(nth_subgoal i thm); ``` clasohm@0 ` 84` clasohm@0 ` 85` ```fun lhs_of_eq i thm = lhs_of(goal_concl i thm) ``` clasohm@0 ` 86` ```and rhs_of_eq i thm = rhs_of(goal_concl i thm); ``` clasohm@0 ` 87` clasohm@0 ` 88` ```fun var_lhs(thm,i) = ``` clasohm@0 ` 89` ```let fun var(Var _) = true ``` clasohm@0 ` 90` ``` | var(Abs(_,_,t)) = var t ``` clasohm@0 ` 91` ``` | var(f\$_) = var f ``` clasohm@0 ` 92` ``` | var _ = false; ``` clasohm@0 ` 93` ```in var(lhs_of_eq i thm) end; ``` clasohm@0 ` 94` clasohm@0 ` 95` ```fun contains_op opns = ``` clasohm@0 ` 96` ``` let fun contains(Const(s,_)) = s mem opns | ``` clasohm@0 ` 97` ``` contains(s\$t) = contains s orelse contains t | ``` clasohm@0 ` 98` ``` contains(Abs(_,_,t)) = contains t | ``` clasohm@0 ` 99` ``` contains _ = false; ``` clasohm@0 ` 100` ``` in contains end; ``` clasohm@0 ` 101` clasohm@0 ` 102` ```fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i; ``` clasohm@0 ` 103` clasohm@0 ` 104` ```val (normI_thms,normE_thms) = split_list norm_thms; ``` clasohm@0 ` 105` clasohm@0 ` 106` ```(*Get the norm constants from norm_thms*) ``` clasohm@0 ` 107` ```val norms = ``` clasohm@0 ` 108` ``` let fun norm thm = ``` clasohm@0 ` 109` ``` case lhs_of(concl_of thm) of ``` clasohm@0 ` 110` ``` Const(n,_)\$_ => n ``` clasohm@0 ` 111` ``` | _ => (prths normE_thms; error"No constant in lhs of a norm_thm") ``` clasohm@0 ` 112` ``` in map norm normE_thms end; ``` clasohm@0 ` 113` clasohm@0 ` 114` ```fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of ``` clasohm@0 ` 115` ``` Const(s,_)\$_ => s mem norms | _ => false; ``` clasohm@0 ` 116` clasohm@0 ` 117` ```val refl_tac = resolve_tac refl_thms; ``` clasohm@0 ` 118` clasohm@0 ` 119` ```fun find_res thms thm = ``` clasohm@0 ` 120` ``` let fun find [] = (prths thms; error"Check Simp_Data") ``` wenzelm@6966 ` 121` ``` | find(th::thms) = thm RS th handle THM _ => find thms ``` clasohm@0 ` 122` ``` in find thms end; ``` clasohm@0 ` 123` clasohm@0 ` 124` ```val mk_trans = find_res trans_thms; ``` clasohm@0 ` 125` clasohm@0 ` 126` ```fun mk_trans2 thm = ``` clasohm@0 ` 127` ```let fun mk[] = error"Check transitivity" ``` wenzelm@6966 ` 128` ``` | mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts ``` clasohm@0 ` 129` ```in mk trans_thms end; ``` clasohm@0 ` 130` clasohm@0 ` 131` ```(*Applies tactic and returns the first resulting state, FAILS if none!*) ``` wenzelm@4271 ` 132` ```fun one_result(tac,thm) = case Seq.pull(tac thm) of ``` clasohm@0 ` 133` ``` Some(thm',_) => thm' ``` clasohm@0 ` 134` ``` | None => raise THM("Simplifier: could not continue", 0, [thm]); ``` clasohm@0 ` 135` clasohm@0 ` 136` ```fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm); ``` clasohm@0 ` 137` clasohm@0 ` 138` clasohm@0 ` 139` ```(**** Adding "NORM" tags ****) ``` clasohm@0 ` 140` clasohm@0 ` 141` ```(*get name of the constant from conclusion of a congruence rule*) ``` clasohm@0 ` 142` ```fun cong_const cong = ``` clasohm@0 ` 143` ``` case head_of (lhs_of (concl_of cong)) of ``` clasohm@0 ` 144` ``` Const(c,_) => c ``` clasohm@0 ` 145` ``` | _ => "" (*a placeholder distinct from const names*); ``` clasohm@0 ` 146` clasohm@0 ` 147` ```(*true if the term is an atomic proposition (no ==> signs) *) ``` clasohm@0 ` 148` ```val atomic = null o strip_assums_hyp; ``` clasohm@0 ` 149` clasohm@0 ` 150` ```(*ccs contains the names of the constants possessing congruence rules*) ``` clasohm@0 ` 151` ```fun add_hidden_vars ccs = ``` clasohm@0 ` 152` ``` let fun add_hvars(tm,hvars) = case tm of ``` clasohm@0 ` 153` ``` Abs(_,_,body) => add_term_vars(body,hvars) ``` clasohm@0 ` 154` ``` | _\$_ => let val (f,args) = strip_comb tm ``` clasohm@0 ` 155` ``` in case f of ``` clasohm@0 ` 156` ``` Const(c,T) => ``` clasohm@0 ` 157` ``` if c mem ccs ``` clasohm@0 ` 158` ``` then foldr add_hvars (args,hvars) ``` clasohm@0 ` 159` ``` else add_term_vars(tm,hvars) ``` clasohm@0 ` 160` ``` | _ => add_term_vars(tm,hvars) ``` clasohm@0 ` 161` ``` end ``` clasohm@0 ` 162` ``` | _ => hvars; ``` clasohm@0 ` 163` ``` in add_hvars end; ``` clasohm@0 ` 164` clasohm@0 ` 165` ```fun add_new_asm_vars new_asms = ``` clasohm@0 ` 166` ``` let fun itf((tm,at),vars) = ``` clasohm@0 ` 167` ``` if at then vars else add_term_vars(tm,vars) ``` clasohm@0 ` 168` ``` fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm ``` clasohm@0 ` 169` ``` in if length(tml)=length(al) ``` clasohm@0 ` 170` ``` then foldr itf (tml~~al,vars) ``` clasohm@0 ` 171` ``` else vars ``` clasohm@0 ` 172` ``` end ``` clasohm@0 ` 173` ``` fun add_vars (tm,vars) = case tm of ``` clasohm@0 ` 174` ``` Abs (_,_,body) => add_vars(body,vars) ``` clasohm@0 ` 175` ``` | r\$s => (case head_of tm of ``` clasohm@0 ` 176` ``` Const(c,T) => (case assoc(new_asms,c) of ``` clasohm@0 ` 177` ``` None => add_vars(r,add_vars(s,vars)) ``` clasohm@0 ` 178` ``` | Some(al) => add_list(tm,al,vars)) ``` clasohm@0 ` 179` ``` | _ => add_vars(r,add_vars(s,vars))) ``` clasohm@0 ` 180` ``` | _ => vars ``` clasohm@0 ` 181` ``` in add_vars end; ``` clasohm@0 ` 182` clasohm@0 ` 183` clasohm@0 ` 184` ```fun add_norms(congs,ccs,new_asms) thm = ``` clasohm@0 ` 185` ```let val thm' = mk_trans2 thm; ``` clasohm@0 ` 186` ```(* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *) ``` clasohm@0 ` 187` ``` val nops = nprems_of thm' ``` clasohm@0 ` 188` ``` val lhs = rhs_of_eq 1 thm' ``` clasohm@0 ` 189` ``` val rhs = lhs_of_eq nops thm' ``` clasohm@0 ` 190` ``` val asms = tl(rev(tl(prems_of thm'))) ``` clasohm@0 ` 191` ``` val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[]) ``` clasohm@0 ` 192` ``` val hvars = add_new_asm_vars new_asms (rhs,hvars) ``` clasohm@0 ` 193` ``` fun it_asms (asm,hvars) = ``` clasohm@0 ` 194` ``` if atomic asm then add_new_asm_vars new_asms (asm,hvars) ``` clasohm@0 ` 195` ``` else add_term_frees(asm,hvars) ``` clasohm@0 ` 196` ``` val hvars = foldr it_asms (asms,hvars) ``` clasohm@0 ` 197` ``` val hvs = map (#1 o dest_Var) hvars ``` clasohm@0 ` 198` ``` val refl1_tac = refl_tac 1 ``` paulson@3537 ` 199` ``` fun norm_step_tac st = st |> ``` paulson@3537 ` 200` ``` (case head_of(rhs_of_eq 1 st) of ``` paulson@3537 ` 201` ``` Var(ixn,_) => if ixn mem hvs then refl1_tac ``` paulson@3537 ` 202` ``` else resolve_tac normI_thms 1 ORELSE refl1_tac ``` paulson@3537 ` 203` ``` | Const _ => resolve_tac normI_thms 1 ORELSE ``` paulson@3537 ` 204` ``` resolve_tac congs 1 ORELSE refl1_tac ``` paulson@3537 ` 205` ``` | Free _ => resolve_tac congs 1 ORELSE refl1_tac ``` paulson@3537 ` 206` ``` | _ => refl1_tac)) ``` paulson@3537 ` 207` ``` val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac ``` wenzelm@4271 ` 208` ``` val Some(thm'',_) = Seq.pull(add_norm_tac thm') ``` clasohm@0 ` 209` ```in thm'' end; ``` clasohm@0 ` 210` clasohm@0 ` 211` ```fun add_norm_tags congs = ``` clasohm@0 ` 212` ``` let val ccs = map cong_const congs ``` clasohm@0 ` 213` ``` val new_asms = filter (exists not o #2) ``` clasohm@0 ` 214` ``` (ccs ~~ (map (map atomic o prems_of) congs)); ``` clasohm@0 ` 215` ``` in add_norms(congs,ccs,new_asms) end; ``` clasohm@0 ` 216` clasohm@0 ` 217` ```fun normed_rews congs = ``` clasohm@0 ` 218` ``` let val add_norms = add_norm_tags congs; ``` clasohm@0 ` 219` ``` in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm)) ``` clasohm@0 ` 220` ``` end; ``` clasohm@0 ` 221` clasohm@0 ` 222` ```fun NORM norm_lhs_tac = EVERY'[resolve_tac [red2], norm_lhs_tac, refl_tac]; ``` clasohm@0 ` 223` clasohm@0 ` 224` ```val trans_norms = map mk_trans normE_thms; ``` clasohm@0 ` 225` clasohm@0 ` 226` clasohm@0 ` 227` ```(* SIMPSET *) ``` clasohm@0 ` 228` clasohm@0 ` 229` ```datatype simpset = ``` clasohm@0 ` 230` ``` SS of {auto_tac: thm list -> int -> tactic, ``` clasohm@0 ` 231` ``` congs: thm list, ``` clasohm@0 ` 232` ``` cong_net: thm Net.net, ``` clasohm@0 ` 233` ``` mk_simps: thm -> thm list, ``` clasohm@0 ` 234` ``` simps: (thm * thm list) list, ``` clasohm@0 ` 235` ``` simp_net: thm Net.net, ``` clasohm@0 ` 236` ``` splits: thm list, ``` clasohm@0 ` 237` ``` split_consts: string list} ``` clasohm@0 ` 238` clasohm@0 ` 239` ```val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty, ``` clasohm@0 ` 240` ``` mk_simps=normed_rews[], simps=[], simp_net=Net.empty, ``` clasohm@0 ` 241` ``` splits=[], split_consts=[]}; ``` clasohm@0 ` 242` clasohm@0 ` 243` ```(** Insertion of congruences, rewrites and case splits **) ``` clasohm@0 ` 244` clasohm@0 ` 245` ```(*insert a thm in a thm net*) ``` clasohm@0 ` 246` ```fun insert_thm_warn (th,net) = ``` clasohm@0 ` 247` ``` Net.insert_term((concl_of th, th), net, eq_thm) ``` clasohm@0 ` 248` ``` handle Net.INSERT => ``` clasohm@0 ` 249` ``` (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th; ``` clasohm@0 ` 250` ``` net); ``` clasohm@0 ` 251` clasohm@0 ` 252` ```val insert_thms = foldr insert_thm_warn; ``` clasohm@0 ` 253` clasohm@0 ` 254` ```fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, ``` clasohm@0 ` 255` ``` splits,split_consts}, thm) = ``` clasohm@0 ` 256` ```let val thms = mk_simps thm ``` clasohm@0 ` 257` ```in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, ``` clasohm@0 ` 258` ``` simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net), ``` clasohm@0 ` 259` ``` splits=splits,split_consts=split_consts} ``` clasohm@0 ` 260` ```end; ``` clasohm@0 ` 261` clasohm@0 ` 262` ```val op addrews = foldl addrew; ``` clasohm@0 ` 263` clasohm@0 ` 264` ```fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, ``` clasohm@0 ` 265` ``` splits,split_consts}, thms) = ``` clasohm@0 ` 266` ```let val congs' = thms @ congs; ``` clasohm@0 ` 267` ```in SS{auto_tac=auto_tac, congs= congs', ``` clasohm@0 ` 268` ``` cong_net= insert_thms (map mk_trans thms,cong_net), ``` clasohm@0 ` 269` ``` mk_simps= normed_rews congs', simps=simps, simp_net=simp_net, ``` clasohm@0 ` 270` ``` splits=splits,split_consts=split_consts} ``` clasohm@0 ` 271` ```end; ``` clasohm@0 ` 272` clasohm@0 ` 273` ```fun split_err() = error("split rule not of the form ?P(c(...)) = ..."); ``` clasohm@0 ` 274` clasohm@0 ` 275` ```fun split_const(_ \$ t) = ``` clasohm@0 ` 276` ``` (case head_of t of Const(a,_) => a | _ => split_err()) ``` clasohm@0 ` 277` ``` | split_const _ = split_err(); ``` clasohm@0 ` 278` clasohm@0 ` 279` ```fun addsplit(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, ``` clasohm@0 ` 280` ``` splits,split_consts}, thm) = ``` clasohm@0 ` 281` ```let val a = split_const(lhs_of(concl_of thm)) ``` clasohm@0 ` 282` ```in SS{auto_tac=auto_tac,congs=congs,cong_net=cong_net, ``` clasohm@0 ` 283` ``` mk_simps=mk_simps,simps=simps,simp_net=simp_net, ``` clasohm@0 ` 284` ``` splits=splits@[mk_trans thm],split_consts=split_consts@[a]} end; ``` clasohm@0 ` 285` clasohm@0 ` 286` ```val op addsplits = foldl addsplit; ``` clasohm@0 ` 287` clasohm@0 ` 288` ```(** Deletion of congruences and rewrites **) ``` clasohm@0 ` 289` clasohm@0 ` 290` ```(*delete a thm from a thm net*) ``` clasohm@0 ` 291` ```fun delete_thm_warn (th,net) = ``` clasohm@0 ` 292` ``` Net.delete_term((concl_of th, th), net, eq_thm) ``` clasohm@0 ` 293` ``` handle Net.DELETE => ``` clasohm@0 ` 294` ``` (writeln"\nNo such rewrite or congruence rule:"; print_thm th; ``` clasohm@0 ` 295` ``` net); ``` clasohm@0 ` 296` clasohm@0 ` 297` ```val delete_thms = foldr delete_thm_warn; ``` clasohm@0 ` 298` clasohm@0 ` 299` ```fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, ``` clasohm@0 ` 300` ``` splits,split_consts}, thms) = ``` clasohm@0 ` 301` ```let val congs' = foldl (gen_rem eq_thm) (congs,thms) ``` clasohm@0 ` 302` ```in SS{auto_tac=auto_tac, congs= congs', ``` clasohm@0 ` 303` ``` cong_net= delete_thms(map mk_trans thms,cong_net), ``` clasohm@0 ` 304` ``` mk_simps= normed_rews congs', simps=simps, simp_net=simp_net, ``` clasohm@0 ` 305` ``` splits=splits,split_consts=split_consts} ``` clasohm@0 ` 306` ```end; ``` clasohm@0 ` 307` clasohm@0 ` 308` ```fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, ``` clasohm@0 ` 309` ``` splits,split_consts}, thm) = ``` clasohm@0 ` 310` ```let fun find((p as (th,ths))::ps',ps) = ``` clasohm@0 ` 311` ``` if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps) ``` clasohm@0 ` 312` ``` | find([],simps') = (writeln"\nNo such rewrite or congruence rule:"; ``` clasohm@0 ` 313` ``` print_thm thm; ``` clasohm@0 ` 314` ``` ([],simps')) ``` clasohm@0 ` 315` ``` val (thms,simps') = find(simps,[]) ``` clasohm@0 ` 316` ```in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, ``` clasohm@0 ` 317` ``` simps = simps', simp_net = delete_thms(thms,simp_net), ``` clasohm@0 ` 318` ``` splits=splits,split_consts=split_consts} ``` clasohm@0 ` 319` ```end; ``` clasohm@0 ` 320` clasohm@0 ` 321` ```val op delrews = foldl delrew; ``` clasohm@0 ` 322` clasohm@0 ` 323` clasohm@0 ` 324` ```fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net, ``` clasohm@0 ` 325` ``` splits,split_consts,...}, auto_tac) = ``` clasohm@0 ` 326` ``` SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, ``` clasohm@0 ` 327` ``` simps=simps, simp_net=simp_net,splits=splits,split_consts=split_consts}; ``` clasohm@0 ` 328` clasohm@0 ` 329` clasohm@0 ` 330` ```(** Inspection of a simpset **) ``` clasohm@0 ` 331` clasohm@0 ` 332` ```fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); ``` clasohm@0 ` 333` clasohm@0 ` 334` ```fun print_ss(SS{congs,simps,splits,...}) = ``` clasohm@0 ` 335` ``` (writeln"Congruences:"; prths congs; ``` clasohm@0 ` 336` ``` writeln"Case Splits"; prths splits; ``` clasohm@0 ` 337` ``` writeln"Rewrite Rules:"; prths (map #1 simps); ()); ``` clasohm@0 ` 338` clasohm@0 ` 339` clasohm@0 ` 340` ```(* Rewriting with case splits *) ``` clasohm@0 ` 341` clasohm@0 ` 342` ```fun splittable a i thm = ``` clasohm@0 ` 343` ``` let val tm = goal_concl i thm ``` clasohm@0 ` 344` ``` fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1) ``` clasohm@0 ` 345` ``` | nobound(s\$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k) ``` clasohm@0 ` 346` ``` | nobound(Bound n,j,k) = n < k orelse k+j <= n ``` clasohm@0 ` 347` ``` | nobound(_) = true; ``` clasohm@0 ` 348` ``` fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al ``` clasohm@0 ` 349` ``` fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1) ``` clasohm@0 ` 350` ``` | find_if(tm as s\$t,j) = let val (f,al) = strip_comb tm in ``` clasohm@0 ` 351` ``` case f of Const(c,_) => if c=a then check_args(al,j) ``` clasohm@0 ` 352` ``` else find_if(s,j) orelse find_if(t,j) ``` clasohm@0 ` 353` ``` | _ => find_if(s,j) orelse find_if(t,j) end ``` clasohm@0 ` 354` ``` | find_if(_) = false; ``` clasohm@0 ` 355` ``` in find_if(tm,0) end; ``` clasohm@0 ` 356` clasohm@0 ` 357` ```fun split_tac (cong_tac,splits,split_consts) i = ``` clasohm@0 ` 358` ``` let fun seq_try (split::splits,a::bs) thm = tapply( ``` clasohm@0 ` 359` ``` COND (splittable a i) (DETERM(resolve_tac[split]i)) ``` paulson@1512 ` 360` ``` ((seq_try(splits,bs))), thm) ``` paulson@1512 ` 361` ``` | seq_try([],_) thm = no_tac thm ``` paulson@1512 ` 362` ``` and try_rew thm = tapply((seq_try(splits,split_consts)) ``` paulson@1512 ` 363` ``` ORELSE one_subt, thm) ``` clasohm@0 ` 364` ``` and one_subt thm = ``` clasohm@0 ` 365` ``` let val test = has_fewer_prems (nprems_of thm + 1) ``` clasohm@0 ` 366` ``` fun loop thm = tapply(COND test no_tac ``` paulson@1512 ` 367` ``` ((try_rew THEN DEPTH_FIRST test (refl_tac i)) ``` paulson@1512 ` 368` ``` ORELSE (refl_tac i THEN loop)), thm) ``` paulson@1512 ` 369` ``` in (cong_tac THEN loop) thm end ``` clasohm@0 ` 370` ``` in if null splits then no_tac ``` paulson@1512 ` 371` ``` else COND (may_match(split_consts,i)) try_rew no_tac ``` clasohm@0 ` 372` ``` end; ``` clasohm@0 ` 373` clasohm@0 ` 374` ```fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i = ``` clasohm@0 ` 375` ```let val cong_tac = net_tac cong_net i ``` clasohm@0 ` 376` ```in NORM (split_tac (cong_tac,splits,split_consts)) i end; ``` clasohm@0 ` 377` clasohm@0 ` 378` ```(* Rewriting Automaton *) ``` clasohm@0 ` 379` clasohm@0 ` 380` ```datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE ``` clasohm@0 ` 381` ``` | PROVE | POP_CS | POP_ARTR | SPLIT; ``` clasohm@0 ` 382` ```(* ``` wenzelm@5961 ` 383` ```fun pr_cntrl c = case c of STOP => std_output("STOP") | MK_EQ => std_output("MK_EQ") | ``` wenzelm@5961 ` 384` ```ASMS i => print_int i | POP_ARTR => std_output("POP_ARTR") | ``` wenzelm@5961 ` 385` ```SIMP_LHS => std_output("SIMP_LHS") | REW => std_output("REW") | REFL => std_output("REFL") | ``` wenzelm@5961 ` 386` ```TRUE => std_output("TRUE") | PROVE => std_output("PROVE") | POP_CS => std_output("POP_CS") | SPLIT ``` wenzelm@5961 ` 387` ```=> std_output("SPLIT"); ``` clasohm@0 ` 388` ```*) ``` clasohm@0 ` 389` ```fun simp_refl([],_,ss) = ss ``` clasohm@0 ` 390` ``` | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) ``` clasohm@0 ` 391` ``` else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); ``` clasohm@0 ` 392` clasohm@0 ` 393` ```(** Tracing **) ``` clasohm@0 ` 394` clasohm@0 ` 395` ```val tracing = ref false; ``` clasohm@0 ` 396` clasohm@0 ` 397` ```(*Replace parameters by Free variables in P*) ``` clasohm@0 ` 398` ```fun variants_abs ([],P) = P ``` clasohm@0 ` 399` ``` | variants_abs ((a,T)::aTs, P) = ``` clasohm@0 ` 400` ``` variants_abs (aTs, #2 (variant_abs(a,T,P))); ``` clasohm@0 ` 401` clasohm@0 ` 402` ```(*Select subgoal i from proof state; substitute parameters, for printing*) ``` clasohm@0 ` 403` ```fun prepare_goal i st = ``` clasohm@0 ` 404` ``` let val subgi = nth_subgoal i st ``` clasohm@0 ` 405` ``` val params = rev(strip_params subgi) ``` clasohm@0 ` 406` ``` in variants_abs (params, strip_assums_concl subgi) end; ``` clasohm@0 ` 407` clasohm@0 ` 408` ```(*print lhs of conclusion of subgoal i*) ``` clasohm@0 ` 409` ```fun pr_goal_lhs i st = ``` clasohm@0 ` 410` ``` writeln (Sign.string_of_term (#sign(rep_thm st)) ``` clasohm@0 ` 411` ``` (lhs_of (prepare_goal i st))); ``` clasohm@0 ` 412` clasohm@0 ` 413` ```(*print conclusion of subgoal i*) ``` clasohm@0 ` 414` ```fun pr_goal_concl i st = ``` clasohm@0 ` 415` ``` writeln (Sign.string_of_term (#sign(rep_thm st)) (prepare_goal i st)) ``` clasohm@0 ` 416` clasohm@0 ` 417` ```(*print subgoals i to j (inclusive)*) ``` clasohm@0 ` 418` ```fun pr_goals (i,j) st = ``` clasohm@0 ` 419` ``` if i>j then () ``` clasohm@0 ` 420` ``` else (pr_goal_concl i st; pr_goals (i+1,j) st); ``` clasohm@0 ` 421` clasohm@0 ` 422` ```(*Print rewrite for tracing; i=subgoal#, n=number of new subgoals, ``` clasohm@0 ` 423` ``` thm=old state, thm'=new state *) ``` clasohm@0 ` 424` ```fun pr_rew (i,n,thm,thm',not_asms) = ``` clasohm@0 ` 425` ``` if !tracing ``` clasohm@0 ` 426` ``` then (if not_asms then () else writeln"Assumption used in"; ``` clasohm@0 ` 427` ``` pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm'; ``` clasohm@0 ` 428` ``` if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm') ``` clasohm@0 ` 429` ``` else (); ``` clasohm@0 ` 430` ``` writeln"" ) ``` clasohm@0 ` 431` ``` else (); ``` clasohm@0 ` 432` clasohm@0 ` 433` ```(* Skip the first n hyps of a goal, and return the rest in generalized form *) ``` clasohm@0 ` 434` ```fun strip_varify(Const("==>", _) \$ H \$ B, n, vs) = ``` clasohm@0 ` 435` ``` if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) ``` clasohm@0 ` 436` ``` else strip_varify(B,n-1,vs) ``` clasohm@0 ` 437` ``` | strip_varify(Const("all",_)\$Abs(_,T,t), n, vs) = ``` clasohm@0 ` 438` ``` strip_varify(t,n,Var(("?",length vs),T)::vs) ``` clasohm@0 ` 439` ``` | strip_varify _ = []; ``` clasohm@0 ` 440` clasohm@0 ` 441` ```fun execute(ss,if_fl,auto_tac,cong_tac,splits,split_consts,net,i) thm = let ``` clasohm@0 ` 442` clasohm@0 ` 443` ```fun simp_lhs(thm,ss,anet,ats,cs) = ``` clasohm@0 ` 444` ``` if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else ``` clasohm@0 ` 445` ``` if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs) ``` wenzelm@4271 ` 446` ``` else case Seq.pull(cong_tac i thm) of ``` clasohm@0 ` 447` ``` Some(thm',_) => ``` clasohm@0 ` 448` ``` let val ps = prems_of thm and ps' = prems_of thm'; ``` clasohm@0 ` 449` ``` val n = length(ps')-length(ps); ``` clasohm@0 ` 450` ``` val a = length(strip_assums_hyp(nth_elem(i-1,ps))) ``` clasohm@0 ` 451` ``` val l = map (fn p => length(strip_assums_hyp(p))) ``` clasohm@0 ` 452` ``` (take(n,drop(i-1,ps'))); ``` clasohm@0 ` 453` ``` in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end ``` clasohm@0 ` 454` ``` | None => (REW::ss,thm,anet,ats,cs); ``` clasohm@0 ` 455` clasohm@0 ` 456` ```(*NB: the "Adding rewrites:" trace will look strange because assumptions ``` clasohm@0 ` 457` ``` are represented by rules, generalized over their parameters*) ``` clasohm@0 ` 458` ```fun add_asms(ss,thm,a,anet,ats,cs) = ``` clasohm@0 ` 459` ``` let val As = strip_varify(nth_subgoal i thm, a, []); ``` lcp@231 ` 460` ``` val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As; ``` clasohm@0 ` 461` ``` val new_rws = flat(map mk_rew_rules thms); ``` clasohm@0 ` 462` ``` val rwrls = map mk_trans (flat(map mk_rew_rules thms)); ``` clasohm@0 ` 463` ``` val anet' = foldr lhs_insert_thm (rwrls,anet) ``` clasohm@0 ` 464` ``` in if !tracing andalso not(null new_rws) ``` clasohm@0 ` 465` ``` then (writeln"Adding rewrites:"; prths new_rws; ()) ``` clasohm@0 ` 466` ``` else (); ``` clasohm@0 ` 467` ``` (ss,thm,anet',anet::ats,cs) ``` clasohm@0 ` 468` ``` end; ``` clasohm@0 ` 469` wenzelm@4271 ` 470` ```fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of ``` clasohm@0 ` 471` ``` Some(thm',seq') => ``` clasohm@0 ` 472` ``` let val n = (nprems_of thm') - (nprems_of thm) ``` clasohm@0 ` 473` ``` in pr_rew(i,n,thm,thm',more); ``` clasohm@0 ` 474` ``` if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) ``` clasohm@0 ` 475` ``` else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), ``` clasohm@0 ` 476` ``` thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) ``` clasohm@0 ` 477` ``` end ``` clasohm@0 ` 478` ``` | None => if more ``` clasohm@0 ` 479` ``` then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm), ``` clasohm@0 ` 480` ``` thm,ss,anet,ats,cs,false) ``` clasohm@0 ` 481` ``` else (ss,thm,anet,ats,cs); ``` clasohm@0 ` 482` clasohm@0 ` 483` ```fun try_true(thm,ss,anet,ats,cs) = ``` wenzelm@4271 ` 484` ``` case Seq.pull(auto_tac i thm) of ``` clasohm@0 ` 485` ``` Some(thm',_) => (ss,thm',anet,ats,cs) ``` clasohm@0 ` 486` ``` | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs ``` clasohm@0 ` 487` ``` in if !tracing ``` clasohm@0 ` 488` ``` then (writeln"*** Failed to prove precondition. Normal form:"; ``` clasohm@0 ` 489` ``` pr_goal_concl i thm; writeln"") ``` clasohm@0 ` 490` ``` else (); ``` clasohm@0 ` 491` ``` rew(seq,thm0,ss0,anet0,ats0,cs0,more) ``` clasohm@0 ` 492` ``` end; ``` clasohm@0 ` 493` clasohm@0 ` 494` ```fun split(thm,ss,anet,ats,cs) = ``` wenzelm@4271 ` 495` ``` case Seq.pull(tapply(split_tac ``` clasohm@0 ` 496` ``` (cong_tac i,splits,split_consts) i,thm)) of ``` clasohm@0 ` 497` ``` Some(thm',_) => (SIMP_LHS::SPLIT::ss,thm',anet,ats,cs) ``` clasohm@0 ` 498` ``` | None => (ss,thm,anet,ats,cs); ``` clasohm@0 ` 499` clasohm@0 ` 500` ```fun step(s::ss, thm, anet, ats, cs) = case s of ``` clasohm@0 ` 501` ``` MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) ``` clasohm@0 ` 502` ``` | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) ``` clasohm@0 ` 503` ``` | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) ``` paulson@1512 ` 504` ``` | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) ``` clasohm@0 ` 505` ``` | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) ``` clasohm@0 ` 506` ``` | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) ``` clasohm@0 ` 507` ``` | PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss ``` clasohm@0 ` 508` ``` else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs) ``` clasohm@0 ` 509` ``` | POP_ARTR => (ss,thm,hd ats,tl ats,cs) ``` clasohm@0 ` 510` ``` | POP_CS => (ss,thm,anet,ats,tl cs) ``` clasohm@0 ` 511` ``` | SPLIT => split(thm,ss,anet,ats,cs); ``` clasohm@0 ` 512` clasohm@0 ` 513` ```fun exec(state as (s::ss, thm, _, _, _)) = ``` clasohm@0 ` 514` ``` if s=STOP then thm else exec(step(state)); ``` clasohm@0 ` 515` clasohm@0 ` 516` ```in exec(ss, thm, Net.empty, [], []) end; ``` clasohm@0 ` 517` clasohm@0 ` 518` clasohm@0 ` 519` ```(*ss = list of commands (not simpset!); ``` clasohm@0 ` 520` ``` fl = even use case splits to solve conditional rewrite rules; ``` clasohm@0 ` 521` ``` addhyps = add hyps to simpset*) ``` clasohm@0 ` 522` ```fun EXEC_TAC (ss,fl,addhyps) simpset = METAHYPS ``` clasohm@0 ` 523` ``` (fn hyps => ``` clasohm@0 ` 524` ``` case (if addhyps then simpset addrews hyps else simpset) of ``` clasohm@0 ` 525` ``` (SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) => ``` clasohm@0 ` 526` ``` PRIMITIVE(execute(ss,fl,auto_tac hyps, ``` clasohm@0 ` 527` ``` net_tac cong_net,splits,split_consts, ``` clasohm@0 ` 528` ``` simp_net, 1)) ``` clasohm@0 ` 529` ``` THEN TRY(auto_tac hyps 1)); ``` clasohm@0 ` 530` clasohm@0 ` 531` ```val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,false); ``` clasohm@0 ` 532` clasohm@0 ` 533` ```val ASM_SIMP_TAC = ``` clasohm@0 ` 534` ``` EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,true); ``` clasohm@0 ` 535` clasohm@0 ` 536` ```val SIMP_SPLIT2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],true,false); ``` clasohm@0 ` 537` clasohm@0 ` 538` ```fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) = ``` clasohm@0 ` 539` ```let val cong_tac = net_tac cong_net ``` clasohm@0 ` 540` ```in fn thm => ``` clasohm@0 ` 541` ``` let val state = thm RSN (2,red1) ``` clasohm@0 ` 542` ``` in execute(ss,fl,auto_tac[],cong_tac,splits,split_consts,simp_net,1)state ``` clasohm@0 ` 543` ``` end ``` clasohm@0 ` 544` ```end; ``` clasohm@0 ` 545` clasohm@0 ` 546` ```val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,SPLIT,REFL,STOP],false); ``` clasohm@0 ` 547` clasohm@0 ` 548` clasohm@0 ` 549` ```(* Compute Congruence rules for individual constants using the substition ``` clasohm@0 ` 550` ``` rules *) ``` clasohm@0 ` 551` clasohm@0 ` 552` ```val subst_thms = map standard subst_thms; ``` clasohm@0 ` 553` clasohm@0 ` 554` clasohm@0 ` 555` ```fun exp_app(0,t) = t ``` clasohm@0 ` 556` ``` | exp_app(i,t) = exp_app(i-1,t \$ Bound (i-1)); ``` clasohm@0 ` 557` clasohm@0 ` 558` ```fun exp_abs(Type("fun",[T1,T2]),t,i) = ``` clasohm@0 ` 559` ``` Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) ``` clasohm@0 ` 560` ``` | exp_abs(T,t,i) = exp_app(i,t); ``` clasohm@0 ` 561` clasohm@0 ` 562` ```fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0); ``` clasohm@0 ` 563` clasohm@0 ` 564` clasohm@0 ` 565` ```fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = ``` clasohm@0 ` 566` ```let fun xn_list(x,n) = ``` clasohm@0 ` 567` ``` let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); ``` paulson@2266 ` 568` ``` in ListPair.map eta_Var (ixs, take(n+1,Ts)) end ``` clasohm@0 ` 569` ``` val lhs = list_comb(f,xn_list("X",k-1)) ``` clasohm@0 ` 570` ``` val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) ``` clasohm@0 ` 571` ```in Abs("", T, Const(eq,[fT,fT]--->eqT) \$ lhs \$ rhs) end; ``` clasohm@0 ` 572` clasohm@0 ` 573` ```fun find_subst tsig T = ``` clasohm@0 ` 574` ```let fun find (thm::thms) = ``` clasohm@0 ` 575` ``` let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); ``` clasohm@0 ` 576` ``` val [P] = term_vars(concl_of thm) \\ [va,vb] ``` clasohm@0 ` 577` ``` val eqT::_ = binder_types cT ``` clasohm@0 ` 578` ``` in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P) ``` clasohm@0 ` 579` ``` else find thms ``` clasohm@0 ` 580` ``` end ``` clasohm@0 ` 581` ``` | find [] = None ``` clasohm@0 ` 582` ```in find subst_thms end; ``` clasohm@0 ` 583` clasohm@0 ` 584` ```fun mk_cong sg (f,aTs,rT) (refl,eq) = ``` clasohm@0 ` 585` ```let val tsig = #tsig(Sign.rep_sg sg); ``` clasohm@0 ` 586` ``` val k = length aTs; ``` clasohm@0 ` 587` ``` fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = ``` lcp@231 ` 588` ``` let val ca = cterm_of sg va ``` lcp@231 ` 589` ``` and cx = cterm_of sg (eta_Var(("X"^si,0),T)) ``` lcp@231 ` 590` ``` val cb = cterm_of sg vb ``` lcp@231 ` 591` ``` and cy = cterm_of sg (eta_Var(("Y"^si,0),T)) ``` lcp@231 ` 592` ``` val cP = cterm_of sg P ``` lcp@231 ` 593` ``` and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) ``` clasohm@0 ` 594` ``` in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; ``` clasohm@0 ` 595` ``` fun mk(c,T::Ts,i,yik) = ``` clasohm@0 ` 596` ``` let val si = radixstring(26,"a",i) ``` clasohm@0 ` 597` ``` in case find_subst tsig T of ``` clasohm@0 ` 598` ``` None => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) ``` clasohm@0 ` 599` ``` | Some s => let val c' = c RSN (2,ri(s,i,si,T,yik)) ``` clasohm@0 ` 600` ``` in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end ``` clasohm@0 ` 601` ``` end ``` clasohm@0 ` 602` ``` | mk(c,[],_,_) = c; ``` clasohm@0 ` 603` ```in mk(refl,rev aTs,k-1,[]) end; ``` clasohm@0 ` 604` clasohm@0 ` 605` ```fun mk_cong_type sg (f,T) = ``` clasohm@0 ` 606` ```let val (aTs,rT) = strip_type T; ``` clasohm@0 ` 607` ``` val tsig = #tsig(Sign.rep_sg sg); ``` clasohm@0 ` 608` ``` fun find_refl(r::rs) = ``` clasohm@0 ` 609` ``` let val (Const(eq,eqT),_,_) = dest_red(concl_of r) ``` clasohm@0 ` 610` ``` in if Type.typ_instance(tsig, rT, hd(binder_types eqT)) ``` clasohm@0 ` 611` ``` then Some(r,(eq,body_type eqT)) else find_refl rs ``` clasohm@0 ` 612` ``` end ``` clasohm@0 ` 613` ``` | find_refl([]) = None; ``` clasohm@0 ` 614` ```in case find_refl refl_thms of ``` clasohm@0 ` 615` ``` None => [] | Some(refl) => [mk_cong sg (f,aTs,rT) refl] ``` clasohm@0 ` 616` ```end; ``` clasohm@0 ` 617` clasohm@0 ` 618` ```fun mk_cong_thy thy f = ``` clasohm@0 ` 619` ```let val sg = sign_of thy; ``` wenzelm@611 ` 620` ``` val T = case Sign.const_type sg f of ``` clasohm@0 ` 621` ``` None => error(f^" not declared") | Some(T) => T; ``` clasohm@0 ` 622` ``` val T' = incr_tvar 9 T; ``` clasohm@0 ` 623` ```in mk_cong_type sg (Const(f,T'),T') end; ``` clasohm@0 ` 624` clasohm@0 ` 625` ```fun mk_congs thy = filter_out is_fact o flat o map (mk_cong_thy thy); ``` clasohm@0 ` 626` clasohm@0 ` 627` ```fun mk_typed_congs thy = ``` clasohm@0 ` 628` ```let val sg = sign_of thy; ``` clasohm@0 ` 629` ``` val S0 = Type.defaultS(#tsig(Sign.rep_sg sg)) ``` clasohm@0 ` 630` ``` fun readfT(f,s) = ``` clasohm@0 ` 631` ``` let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s); ``` wenzelm@611 ` 632` ``` val t = case Sign.const_type sg f of ``` clasohm@0 ` 633` ``` Some(_) => Const(f,T) | None => Free(f,T) ``` clasohm@0 ` 634` ``` in (t,T) end ``` clasohm@0 ` 635` ```in flat o map (mk_cong_type sg o readfT) end; ``` clasohm@0 ` 636` clasohm@0 ` 637` ```(* This code is fishy, esp the "let val T' = ..." ``` clasohm@0 ` 638` ```fun extract_free_congs() = ``` clasohm@0 ` 639` ```let val {prop,sign,...} = rep_thm(topthm()); ``` clasohm@0 ` 640` ``` val frees = add_term_frees(prop,[]); ``` clasohm@0 ` 641` ``` fun filter(Free(a,T as Type("fun",_))) = ``` clasohm@0 ` 642` ``` let val T' = incr_tvar 9 (Type.varifyT T) ``` clasohm@0 ` 643` ``` in [(Free(a,T),T)] end ``` clasohm@0 ` 644` ``` | filter _ = [] ``` clasohm@0 ` 645` ```in flat(map (mk_cong_type sign) (flat (map filter frees))) end; ``` clasohm@0 ` 646` ```*) ``` clasohm@0 ` 647` clasohm@0 ` 648` ```end (* local *) ``` clasohm@0 ` 649` ```end (* SIMP *); ```