| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 108 kB |
|
Quelle old_recdef.ML Sprache: SML |
|||||||||
|
(* Title: HOL/Library/old_recdef.ML
Author: Konrad Slind, Cambridge University Computer Laboratory Author: Lucas Dixon, University of Edinburgh Old TFL/recdef package. *) signature CASE_SPLIT = sig (* try to recursively split conjectured thm to given list of thms *) val splitto : Proof.context -> thm list -> thm -> thm end; signature UTILS = sig exception ERR of {module: string, func: string, mesg: string} val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c val pluck: ('a -> bool) -> 'a list -> 'a * 'a list val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list val take: ('a -> 'b) -> int * 'a list -> 'b list end; signature USYNTAX = sig datatype lambda = VAR of {Name : string, Ty : typ} | CONST of {Name : string, Ty : typ} | COMB of {Rator: term, Rand : term} | LAMB of {Bvar : term, Body : term} val alpha : typ (* Types *) val type_vars : typ -> typ list val type_varsl : typ list -> typ list val mk_vartype : string -> typ val is_vartype : typ -> bool val strip_prod_type : typ -> typ list (* Terms *) val free_vars_lr : term -> term list val type_vars_in_term : term -> typ list val dest_term : term -> lambda (* Prelogic *) val inst : (typ*typ) list -> term -> term (* Construction routines *) val mk_abs :{Bvar : term, Body : term} -> term val mk_imp :{ant : term, conseq : term} -> term val mk_select :{Bvar : term, Body : term} -> term val mk_forall :{Bvar : term, Body : term} -> term val mk_exists :{Bvar : term, Body : term} -> term val mk_conj :{conj1 : term, conj2 : term} -> term val mk_disj :{disj1 : term, disj2 : term} -> term val mk_pabs :{varstruct : term, body : term} -> term (* Destruction routines *) val dest_const: term -> {Name : string, Ty : typ} val dest_comb : term -> {Rator : term, Rand : term} val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list val dest_eq : term -> {lhs : term, rhs : term} val dest_imp : term -> {ant : term, conseq : term} val dest_forall : term -> {Bvar : term, Body : term} val dest_exists : term -> {Bvar : term, Body : term} val dest_neg : term -> term val dest_conj : term -> {conj1 : term, conj2 : term} val dest_disj : term -> {disj1 : term, disj2 : term} val dest_pair : term -> {fst : term, snd : term} val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list} val lhs : term -> term val rhs : term -> term val rand : term -> term (* Query routines *) val is_imp : term -> bool val is_forall : term -> bool val is_exists : term -> bool val is_neg : term -> bool val is_conj : term -> bool val is_disj : term -> bool val is_pair : term -> bool val is_pabs : term -> bool (* Construction of a term from a list of Preterms *) val list_mk_abs : (term list * term) -> term val list_mk_imp : (term list * term) -> term val list_mk_forall : (term list * term) -> term val list_mk_conj : term list -> term (* Destructing a term to a list of Preterms *) val strip_comb : term -> (term * term list) val strip_abs : term -> (term list * term) val strip_imp : term -> (term list * term) val strip_forall : term -> (term list * term) val strip_exists : term -> (term list * term) val strip_disj : term -> term list (* Miscellaneous *) val mk_vstruct : typ -> term list -> term val gen_all : term -> term val find_term : (term -> bool) -> term -> term option val dest_relation : term -> term * term * term val is_WFR : term -> bool val ARB : typ -> term end; signature DCTERM = sig val dest_comb: cterm -> cterm * cterm val dest_abs: cterm -> cterm * cterm val capply: cterm -> cterm -> cterm val cabs: cterm -> cterm -> cterm val mk_conj: cterm * cterm -> cterm val mk_disj: cterm * cterm -> cterm val mk_exists: cterm * cterm -> cterm val dest_conj: cterm -> cterm * cterm val dest_const: cterm -> {Name: string, Ty: typ} val dest_disj: cterm -> cterm * cterm val dest_eq: cterm -> cterm * cterm val dest_exists: cterm -> cterm * cterm val dest_forall: cterm -> cterm * cterm val dest_imp: cterm -> cterm * cterm val dest_neg: cterm -> cterm val dest_pair: cterm -> cterm * cterm val dest_var: cterm -> {Name:string, Ty:typ} val is_conj: cterm -> bool val is_disj: cterm -> bool val is_eq: cterm -> bool val is_exists: cterm -> bool val is_forall: cterm -> bool val is_imp: cterm -> bool val is_neg: cterm -> bool val is_pair: cterm -> bool val list_mk_disj: cterm list -> cterm val strip_abs: cterm -> cterm list * cterm val strip_comb: cterm -> cterm * cterm list val strip_disj: cterm -> cterm list val strip_exists: cterm -> cterm list * cterm val strip_forall: cterm -> cterm list * cterm val strip_imp: cterm -> cterm list * cterm val drop_prop: cterm -> cterm val mk_prop: cterm -> cterm end; signature RULES = sig val dest_thm: thm -> term list * term (* Inference rules *) val REFL: cterm -> thm val ASSUME: cterm -> thm val MP: thm -> thm -> thm val MATCH_MP: thm -> thm -> thm val CONJUNCT1: thm -> thm val CONJUNCT2: thm -> thm val CONJUNCTS: thm -> thm list val DISCH: cterm -> thm -> thm val UNDISCH: thm -> thm val SPEC: cterm -> thm -> thm val ISPEC: cterm -> thm -> thm val ISPECL: cterm list -> thm -> thm val GEN: Proof.context -> cterm -> thm -> thm val GENL: Proof.context -> cterm list -> thm -> thm val LIST_CONJ: thm list -> thm val SYM: thm -> thm val DISCH_ALL: thm -> thm val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm val SPEC_ALL: thm -> thm val GEN_ALL: Proof.context -> thm -> thm val IMP_TRANS: thm -> thm -> thm val PROVE_HYP: thm -> thm -> thm val CHOOSE: Proof.context -> cterm * thm -> thm -> thm val EXISTS: Proof.context -> cterm * cterm -> thm -> thm val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm val EVEN_ORS: thm list -> thm list val DISJ_CASESL: thm -> thm list -> thm val list_beta_conv: cterm -> cterm list -> thm val SUBS: Proof.context -> thm list -> thm -> thm val simpl_conv: Proof.context -> thm list -> cterm -> thm val rbeta: thm -> thm val tracing: bool Unsynchronized.ref val CONTEXT_REWRITE_RULE: Proof.context -> term * term list * thm * thm list -> thm -> thm * term list val RIGHT_ASSOC: Proof.context -> thm -> thm val prove: Proof.context -> bool -> term -> (Proof.context -> tactic) -> thm end; signature THRY = sig val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list val match_type: theory -> typ -> typ -> (typ * typ) list val typecheck: theory -> term -> cterm (*datatype facts of various flavours*) val match_info: theory -> string -> {constructors: term list, case_const: term} option val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list} end; signature PRIM = sig val trace: bool Unsynchronized.ref val trace_thms: Proof.context -> string -> thm list -> unit val trace_cterm: Proof.context -> string -> cterm -> unit type pattern val mk_functional: theory -> term list -> {functional: term, pats: pattern list} val wfrec_definition0: string -> term -> term -> theory -> thm * theory val post_definition: Proof.context -> thm list -> thm * pattern list -> {rules: thm, rows: int list, TCs: term list list, full_pats_TCs: (term * term list) list} val mk_induction: Proof.context -> {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm val postprocess: Proof.context -> bool -> {wf_tac: Proof.context -> tactic, terminator: Proof.context -> tactic, simplifier: Proof.context -> cterm -> thm} -> {rules: thm, induction: thm, TCs: term list list} -> {rules: thm, induction: thm, nested_tcs: thm list} end; signature TFL = sig val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context end; signature OLD_RECDEF = sig val get_recdef: theory -> string -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list} val simp_add: attribute val simp_del: attribute val cong_add: attribute val cong_del: attribute val wf_add: attribute val wf_del: attribute val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list -> Token.src option -> theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list -> theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} end; structure Old_Recdef: OLD_RECDEF = struct (*** extra case splitting for TFL ***) structure CaseSplit: CASE_SPLIT = struct (* make a casethm from an induction thm *) fun cases_thm_of_induct_thm ctxt = Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i))); (* get the case_thm (my version) from a type *) fun case_thm_of_ty ctxt ty = let val thy = Proof_Context.theory_of ctxt val ty_str = case ty of Type(ty_str, _) => ty_str | TFree(s,_) => error ("Free type: " ^ s) | TVar((s,_),_) => error ("Free variable: " ^ s) val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str in cases_thm_of_induct_thm ctxt induct end; (* for use when there are no prems to the subgoal *) (* does a case split on the given variable *) fun mk_casesplit_goal_thm ctxt (vstr,ty) gt = let val thy = Proof_Context.theory_of ctxt; val x = Free(vstr,ty); val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); val case_thm = case_thm_of_ty ctxt ty; val abs_ct = Thm.cterm_of ctxt abst; val free_ct = Thm.cterm_of ctxt x; val (Pv, Dv, type_insts) = case (Thm.concl_of case_thm) of (_ $ (Pv $ (Dv as Var(_, Dty)))) => (Pv, Dv, Sign.typ_match thy (Dty, ty) Vartab.empty) | _ => error "not a valid case thm"; val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest type_insts); val Pv = dest_Var (Envir.subst_term_types type_insts Pv); val Dv = dest_Var (Envir.subst_term_types type_insts Dv); in Conv.fconv_rule Drule.beta_eta_conversion (case_thm |> Thm.instantiate (TVars.make type_cinsts, Vars.empty) |> Thm.instantiate (TVars.empty, Vars.make2 (Pv, abs_ct) (Dv, free_ct))) end; (* the find_XXX_split functions are simply doing a lightwieght (I think) term matching equivalent to find where to do the next split *) (* assuming two twems are identical except for a free in one at a subterm, or constant in another, ie assume that one term is a plit of another, then gives back the free variable that has been split. *) exception find_split_exp of string fun find_term_split (Free v, _ $ _) = SOME v | find_term_split (Free v, Const _) = SOME v | find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *) | find_term_split (Free _, Var _) = NONE (* keep searching *) | find_term_split (a $ b, a2 $ b2) = (case find_term_split (a, a2) of NONE => find_term_split (b,b2) | vopt => vopt) | find_term_split (Abs(_,_,t1), Abs(_,_,t2)) = find_term_split (t1, t2) | find_term_split (Const (x,_), Const(x2,_)) = if x = x2 then NONE else (* keep searching *) raise find_split_exp (* stop now *) "Terms are not identical upto a free varaible! (Consts)" | find_term_split (Bound i, Bound j) = if i = j then NONE else (* keep searching *) raise find_split_exp (* stop now *) "Terms are not identical upto a free varaible! (Bound)" | find_term_split _ = raise find_split_exp (* stop now *) "Terms are not identical upto a free varaible! (Other)"; (* assume that "splitth" is a case split form of subgoal i of "genth", then look for a free variable to split, breaking the subgoal closer to splitth. *) fun find_thm_split splitth i genth = find_term_split (Logic.get_goal (Thm.prop_of genth) i, Thm.concl_of splitth) handle find_split_exp _ => NONE; (* as above but searches "splitths" for a theorem that suggest a case split *) fun find_thms_split splitths i genth = Library.get_first (fn sth => find_thm_split sth i genth) splitths; (* split the subgoal i of "genth" until we get to a member of splitths. Assumes that genth will be a general form of splitths, that can be case-split, as needed. Otherwise fails. Note: We assume that all of "splitths" are split to the same level, and thus it doesn't matter which one we choose to look for the next split. Simply add search on splitthms and split variable, to change this. *) (* Note: possible efficiency measure: when a case theorem is no longer useful, drop it? *) (* Note: This should not be a separate tactic but integrated into the case split done during recdef's case analysis, this would avoid us having to (re)search for variables to split. *) fun splitto ctxt splitths genth = let val _ = not (null splitths) orelse error "splitto: no given splitths"; (* check if we are a member of splitths - FIXME: quicker and more flexible with discrim net. *) fun solve_by_splitth th split = Thm.biresolution (SOME ctxt) false [(false,split)] 1 th; fun split th = (case find_thms_split splitths 1 th of NONE => (writeln (cat_lines (["th:", Thm.string_of_thm ctxt th, "split ths:"] @ map (Thm.string_of_thm ctxt) splitths @ ["\n--"])); error "splitto: cannot find variable to split on") | SOME v => let val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th))); val split_thm = mk_casesplit_goal_thm ctxt v gt; val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm; in expf (map recsplitf subthms) end) and recsplitf th = (* note: multiple unifiers! we only take the first element, probably fine -- there is probably only one anyway. *) (case get_first (Seq.pull o solve_by_splitth th) splitths of NONE => split th | SOME (solved_th, _) => solved_th); in recsplitf genth end; end; (*** basic utilities ***) structure Utils: UTILS = struct (*standard exception for TFL*) exception ERR of {module: string, func: string, mesg: string}; fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg}; fun end_itlist _ [] = raise (UTILS_ERR "end_itlist" "list too short") | end_itlist _ [x] = x | end_itlist f (x :: xs) = f x (end_itlist f xs); fun itlist2 f L1 L2 base_value = let fun it ([],[]) = base_value | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2)) | it _ = raise UTILS_ERR "itlist2" "different length lists" in it (L1,L2) end; fun pluck p = let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found" | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) in fn L => remv(L,[]) end; fun take f = let fun grab(0, _) = [] | grab(n, x::rst) = f x::grab(n-1,rst) in grab end; fun zip3 [][][] = [] | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths"; end; (*** emulation of HOL's abstract syntax functions ***) structure USyntax: USYNTAX = struct infix 4 ##; fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; (*--------------------------------------------------------------------------- * * Types * *---------------------------------------------------------------------------*) val mk_prim_vartype = TVar; fun mk_vartype s = mk_prim_vartype ((s, 0), \<^sort>\<open>type\<close>); (* But internally, it's useful *) fun dest_vtype (TVar x) = x | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; val is_vartype = can dest_vtype; val type_vars = map mk_prim_vartype o Misc_Legacy.typ_tvars fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []); val alpha = mk_vartype "'a" val strip_prod_type = HOLogic.flatten_tupleT; (*--------------------------------------------------------------------------- * * Terms * *---------------------------------------------------------------------------*) (* Free variables, in order of occurrence, from left to right in the * syntax tree. *) fun free_vars_lr tm = let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end fun add (t, frees) = case t of Free _ => if (memb t frees) then frees else t::frees | Abs (_,_,body) => add(body,frees) | f$t => add(t, add(f, frees)) | _ => frees in rev(add(tm,[])) end; val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars; (* Prelogic *) fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) fun inst theta = subst_vars (map dest_tybinding theta,[]) (* Construction routines *) fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable"; fun mk_imp{ant,conseq} = let val c = Const(\<^const_name>\<open>HOL.implies\<close>,HOLogic.boolT --> HOLogic.boolT --> H in list_comb(c,[ant,conseq]) end; fun mk_select (r as {Bvar,Body}) = let val ty = type_of Bvar val c = Const(\<^const_name>\<open>Eps\<close>,(ty --> HOLogic.boolT) --> ty) in list_comb(c,[mk_abs r]) end; fun mk_forall (r as {Bvar,Body}) = let val ty = type_of Bvar val c = Const(\<^const_name>\<open>All\<close>,(ty --> HOLogic.boolT) --> HOLogic.boolT) in list_comb(c,[mk_abs r]) end; fun mk_exists (r as {Bvar,Body}) = let val ty = type_of Bvar val c = Const(\<^const_name>\<open>Ex\<close>,(ty --> HOLogic.boolT) --> HOLogic.boolT) in list_comb(c,[mk_abs r]) end; fun mk_conj{conj1,conj2} = let val c = Const(\<^const_name>\<open>HOL.conj\<close>,HOLogic.boolT --> HOLogic.boolT --> HOLo in list_comb(c,[conj1,conj2]) end; fun mk_disj{disj1,disj2} = let val c = Const(\<^const_name>\<open>HOL.disj\<close>,HOLogic.boolT --> HOLogic.boolT --> HOLo in list_comb(c,[disj1,disj2]) end; fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); local fun mk_uncurry (xt, yt, zt) = Const(\<^const_name>\<open>case_prod\<close>, (xt --> yt --> zt) --> prod_ty xt yt --> zt) fun dest_pair(Const(\<^const_name>\<open>Pair\<close>,_) $ M $ N) = {fst=M, snd=N} | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false in fun mk_pabs{varstruct,body} = let fun mpa (varstruct, body) = if is_var varstruct then mk_abs {Bvar = varstruct, Body = body} else let val {fst, snd} = dest_pair varstruct in mk_uncurry (type_of fst, type_of snd, type_of body) $ mpa (fst, mpa (snd, body)) end in mpa (varstruct, body) end handle TYPE _ => raise USYN_ERR "mk_pabs" ""; end; (* Destruction routines *) datatype lambda = VAR of {Name : string, Ty : typ} | CONST of {Name : string, Ty : typ} | COMB of {Rator: term, Rand : term} | LAMB of {Bvar : term, Body : term}; fun dest_term(Var((s,_),ty)) = VAR{Name = s, Ty = ty} | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} | dest_term(M$N) = COMB{Rator=M,Rand=N} | dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) in LAMB{Bvar = v, Body = Term.betapply (M,v)} end | dest_term(Bound _) = raise USYN_ERR "dest_term" "Bound"; fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} | dest_const _ = raise USYN_ERR "dest_const" "not a constant"; fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} | dest_comb _ = raise USYN_ERR "dest_comb" "not a comb"; fun dest_abs used (a as Abs(s, ty, _)) = let val s' = singleton (Name.variant_list used) s; val v = Free(s', ty); in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used) end | dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction"; fun dest_eq(Const(\<^const_name>\<open>HOL.eq\<close>,_) $ M $ N) = {lhs=M, rhs=N} | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality"; fun dest_imp(Const(\<^const_name>\<open>HOL.implies\<close>,_) $ M $ N) = {ant=M, conseq=N} | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication"; fun dest_forall(Const(\<^const_name>\<open>All\<close>,_) $ (a as Abs _)) = fst (dest_abs [] a) | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall"; fun dest_exists(Const(\<^const_name>\<open>Ex\<close>,_) $ (a as Abs _)) = fst (dest_abs [] a) | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential"; fun dest_neg(Const(\<^const_name>\<open>Not\<close>,_) $ M) = M | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; fun dest_conj(Const(\<^const_name>\<open>HOL.conj\<close>,_) $ M $ N) = {conj1=M, conj2=N} | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction"; fun dest_disj(Const(\<^const_name>\<open>HOL.disj\<close>,_) $ M $ N) = {disj1=M, disj2=N} | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction"; fun mk_pair{fst,snd} = let val ty1 = type_of fst val ty2 = type_of snd val c = Const(\<^const_name>\<open>Pair\<close>,ty1 --> ty2 --> prod_ty ty1 ty2) in list_comb(c,[fst,snd]) end; fun dest_pair(Const(\<^const_name>\<open>Pair\<close>,_) $ M $ N) = {fst=M, snd=N} | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; local fun ucheck t = (if #Name (dest_const t) = \<^const_name>\<open>case_prod\<close> then t else raise Match) in fun dest_pabs used tm = let val ({Bvar,Body}, used') = dest_abs used tm in {varstruct = Bvar, body = Body, used = used'} end handle Utils.ERR _ => let val {Rator,Rand} = dest_comb tm val _ = ucheck Rator val {varstruct = lv, body, used = used'} = dest_pabs used Rand val {varstruct = rv, body, used = used''} = dest_pabs used' body in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''} end end; val lhs = #lhs o dest_eq val rhs = #rhs o dest_eq val rand = #Rand o dest_comb (* Query routines *) val is_imp = can dest_imp val is_forall = can dest_forall val is_exists = can dest_exists val is_neg = can dest_neg val is_conj = can dest_conj val is_disj = can dest_disj val is_pair = can dest_pair val is_pabs = can (dest_pabs []) (* Construction of a cterm from a list of Terms *) fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; (* These others are almost never used *) fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t; val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) (* Need to reverse? *) fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm); (* Destructing a cterm to a list of Terms *) fun strip_comb tm = let fun dest(M$N, A) = dest(M, N::A) | dest x = x in dest(tm,[]) end; fun strip_abs(tm as Abs _) = let val ({Bvar,Body}, _) = dest_abs [] tm val (bvs, core) = strip_abs Body in (Bvar::bvs, core) end | strip_abs M = ([],M); fun strip_imp fm = if (is_imp fm) then let val {ant,conseq} = dest_imp fm val (was,wb) = strip_imp conseq in ((ant::was), wb) end else ([],fm); fun strip_forall fm = if (is_forall fm) then let val {Bvar,Body} = dest_forall fm val (bvs,core) = strip_forall Body in ((Bvar::bvs), core) end else ([],fm); fun strip_exists fm = if (is_exists fm) then let val {Bvar, Body} = dest_exists fm val (bvs,core) = strip_exists Body in (Bvar::bvs, core) end else ([],fm); fun strip_disj w = if (is_disj w) then let val {disj1,disj2} = dest_disj w in (strip_disj disj1@strip_disj disj2) end else [w]; (* Miscellaneous *) fun mk_vstruct ty V = let fun follow_prod_type (Type(\<^type_name>\<open>Product_Type.prod\<close>,[ty1,ty2])) v let val (ltm,vs1) = follow_prod_type ty1 vs val (rtm,vs2) = follow_prod_type ty2 vs1 in (mk_pair{fst=ltm, snd=rtm}, vs2) end | follow_prod_type _ (v::vs) = (v,vs) in #1 (follow_prod_type ty V) end; (* Search a term for a sub-term satisfying the predicate p. *) fun find_term p = let fun find tm = if (p tm) then SOME tm else case tm of Abs(_,_,body) => find body | (t$u) => (case find t of NONE => find u | some => some) | _ => NONE in find end; fun dest_relation tm = if (type_of tm = HOLogic.boolT) then let val (Const(\<^const_name>\<open>Set.member\<close>,_) $ (Const(\<^const_name>\<open>Pa in (R,y,x) end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure" else raise USYN_ERR "dest_relation" "not a boolean term"; fun is_WFR \<^Const_>\<open>Wellfounded.wf_on _ for \<^Const_>\<open>top_class.top _\<close> _\<cl | is_WFR _ = false; fun ARB ty = mk_select{Bvar=Free("v",ty), Body=Const(\<^const_name>\<open>True\<close>,HOLogic.boolT)}; end; (*** derived cterm destructors ***) structure Dcterm: DCTERM = struct fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg}; fun dest_comb t = Thm.dest_comb t handle CTERM (msg, _) => raise ERR "dest_comb" msg; fun dest_abs t = Thm.dest_abs_global t handle CTERM (msg, _) => raise ERR "dest_abs" msg; fun capply t u = Thm.apply t u handle CTERM (msg, _) => raise ERR "capply" msg; fun cabs a t = Thm.lambda a t handle CTERM (msg, _) => raise ERR "cabs" msg; (*--------------------------------------------------------------------------- * Some simple constructor functions. *---------------------------------------------------------------------------*) val mk_hol_const = Thm.cterm_of \<^theory_context>\<open>HOL\<close> o Const; fun mk_exists (r as (Bvar, Body)) = let val ty = Thm.typ_of_cterm Bvar val c = mk_hol_const(\<^const_name>\<open>Ex\<close>, (ty --> HOLogic.boolT) --> HOLogic.boolT) in capply c (uncurry cabs r) end; local val c = mk_hol_const(\<^const_name>\<open>HOL.conj\<close>, HOLogic.boolT --> HOLogic.bo in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2 end; local val c = mk_hol_const(\<^const_name>\<open>HOL.disj\<close>, HOLogic.boolT --> HOLogic.bo in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2 end; (*--------------------------------------------------------------------------- * The primitives. *---------------------------------------------------------------------------*) fun dest_const ctm = (case Thm.term_of ctm of Const(s,ty) => {Name = s, Ty = ty} | _ => raise ERR "dest_const" "not a constant"); fun dest_var ctm = (case Thm.term_of ctm of Var((s,_),ty) => {Name=s, Ty=ty} | Free(s,ty) => {Name=s, Ty=ty} | _ => raise ERR "dest_var" "not a variable"); (*--------------------------------------------------------------------------- * Derived destructor operations. *---------------------------------------------------------------------------*) fun dest_monop expected tm = let fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected); val (c, N) = dest_comb tm handle Utils.ERR _ => err (); val name = #Name (dest_const c handle Utils.ERR _ => err ()); in if name = expected then N else err () end; fun dest_binop expected tm = let fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected); val (M, N) = dest_comb tm handle Utils.ERR _ => err () in (dest_monop expected M, N) handle Utils.ERR _ => err () end; fun dest_binder expected tm = dest_abs (dest_monop expected tm) handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); val dest_neg = dest_monop \<^const_name>\<open>Not\<close> val dest_pair = dest_binop \<^const_name>\<open>Pair\<close> val dest_eq = dest_binop \<^const_name>\<open>HOL.eq\<close> val dest_imp = dest_binop \<^const_name>\<open>HOL.implies\<close> val dest_conj = dest_binop \<^const_name>\<open>HOL.conj\<close> val dest_disj = dest_binop \<^const_name>\<open>HOL.disj\<close> val dest_exists = dest_binder \<^const_name>\<open>Ex\<close> val dest_forall = dest_binder \<^const_name>\<open>All\<close> (* Query routines *) val is_eq = can dest_eq val is_imp = can dest_imp val is_forall = can dest_forall val is_exists = can dest_exists val is_neg = can dest_neg val is_conj = can dest_conj val is_disj = can dest_disj val is_pair = can dest_pair (*--------------------------------------------------------------------------- * Iterated creation. *---------------------------------------------------------------------------*) val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm)); (*--------------------------------------------------------------------------- * Iterated destruction. (To the "right" in a term.) *---------------------------------------------------------------------------*) fun strip break tm = let fun dest (p as (ctm,accum)) = let val (M,N) = break ctm in dest (N, M::accum) end handle Utils.ERR _ => p in dest (tm,[]) end; fun rev2swap (x,l) = (rev l, x); val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *) val strip_imp = rev2swap o strip dest_imp val strip_abs = rev2swap o strip dest_abs val strip_forall = rev2swap o strip dest_forall val strip_exists = rev2swap o strip dest_exists val strip_disj = rev o (op::) o strip dest_disj (*--------------------------------------------------------------------------- * Going into and out of prop *---------------------------------------------------------------------------*) fun mk_prop ct = if HOLogic.is_judgment ct then ct else HOLogic.mk_judgment ct; fun drop_prop ct = if HOLogic.is_judgment ct then Thm.dest_arg ct else ct; end; (*** emulation of HOL inference rules for TFL ***) structure Rules: RULES = struct fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg}; fun cconcl thm = Dcterm.drop_prop (Thm.cprop_of thm); fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm); fun dest_thm thm = (map HOLogic.dest_Trueprop (Thm.hyps_of thm), HOLogic.dest_Trueprop (Thm.prop_of thm)) handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop"; (* Inference rules *) (*--------------------------------------------------------------------------- * Equality (one step) *---------------------------------------------------------------------------*) fun REFL tm = HOLogic.mk_obj_eq (Thm.reflexive tm) handle THM (msg, _, _) => raise RULES_ERR "REFL" msg; fun SYM thm = thm RS sym handle THM (msg, _, _) => raise RULES_ERR "SYM" msg; fun ALPHA thm ctm1 = let val ctm2 = Thm.cprop_of thm; val ctm2_eq = Thm.reflexive ctm2; val ctm1_eq = Thm.reflexive ctm1; in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg; fun rbeta th = (case Dcterm.strip_comb (cconcl th) of (_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r) | _ => raise RULES_ERR "rbeta" ""); (*---------------------------------------------------------------------------- * Implication and the assumption list * * Assumptions get stuck on the meta-language assumption list. Implications * are in the object language, so discharging an assumption "A" from theorem * "B" results in something that looks like "A --> B". *---------------------------------------------------------------------------*) fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm); (*--------------------------------------------------------------------------- * Implication in TFL is -->. Meta-language implication (==>) is only used * in the implementation of some of the inference rules below. *---------------------------------------------------------------------------*) fun MP th1 th2 = th2 RS (th1 RS mp) handle THM (msg, _, _) => raise RULES_ERR "MP" msg; (*forces the first argument to be a proposition if necessary*) fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg; fun DISCH_ALL thm = fold_rev DISCH (Thm.chyps_of thm) thm; fun FILTER_DISCH_ALL P thm = let fun check tm = P (Thm.term_of tm) in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm end; fun UNDISCH thm = let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm))) in Thm.implies_elim (thm RS mp) (ASSUME tm) end handle Utils.ERR _ => raise RULES_ERR "UNDISCH" "" | THM _ => raise RULES_ERR "UNDISCH" ""; fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans}) handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg; (*---------------------------------------------------------------------------- * Conjunction *---------------------------------------------------------------------------*) fun CONJUNCT1 thm = thm RS conjunct1 handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg; fun CONJUNCT2 thm = thm RS conjunct2 handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg; fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list" | LIST_CONJ [th] = th | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst) handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg; (*---------------------------------------------------------------------------- * Disjunction *---------------------------------------------------------------------------*) local val prop = Thm.prop_of disjI1 val [_,Q] = Misc_Legacy.term_vars prop val disj1 = Thm.forall_intr (Thm.cterm_of \<^context> Q) disjI1 in fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1) handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; end; local val prop = Thm.prop_of disjI2 val [P,_] = Misc_Legacy.term_vars prop val disj2 = Thm.forall_intr (Thm.cterm_of \<^context> P) disjI2 in fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2) handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg; end; (*---------------------------------------------------------------------------- * * A1 |- M1, ..., An |- Mn * --------------------------------------------------- * [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn] * *---------------------------------------------------------------------------*) fun EVEN_ORS thms = let fun blue ldisjs [] _ = [] | blue ldisjs (th::rst) rdisjs = let val tail = tl rdisjs val rdisj_tl = Dcterm.list_mk_disj tail in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl) :: blue (ldisjs @ [cconcl th]) rst tail end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th] in blue [] thms (map cconcl thms) end; (*---------------------------------------------------------------------------- * * A |- P \/ Q B,P |- R C,Q |- R * --------------------------------------------------- * A U B U C |- R * *---------------------------------------------------------------------------*) fun DISJ_CASES th1 th2 th3 = let val c = Dcterm.drop_prop (cconcl th1); val (disj1, disj2) = Dcterm.dest_disj c; val th2' = DISCH disj1 th2; val th3' = DISCH disj2 th3; in th3' RS (th2' RS (th1 RS @{thm tfl_disjE})) handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg end; (*----------------------------------------------------------------------------- * * |- A1 \/ ... \/ An [A1 |- M, ..., An |- M] * --------------------------------------------------- * |- M * * Note. The list of theorems may be all jumbled up, so we have to * first organize it to align with the first argument (the disjunctive * theorem). *---------------------------------------------------------------------------*) fun organize eq = (* a bit slow - analogous to insertion sort *) let fun extract a alist = let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1" | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t) in ex ([],alist) end fun place [] [] = [] | place (a::rst) alist = let val (item,next) = extract a alist in item::place rst next end | place _ _ = raise RULES_ERR "organize" "not a permutation.2" in place end; fun DISJ_CASESL disjth thl = let val c = cconcl disjth fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th) val tml = Dcterm.strip_disj c fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases" | DL th [th1] = PROVE_HYP th th1 | DL th [th1,th2] = DISJ_CASES th th1 th2 | DL th (th1::rst) = let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th))) in DISJ_CASES th th1 (DL (ASSUME tm) rst) end in DL disjth (organize eq tml thl) end; (*---------------------------------------------------------------------------- * Universals *---------------------------------------------------------------------------*) local (* this is fragile *) val prop = Thm.prop_of spec val x = hd (tl (Misc_Legacy.term_vars prop)) val TV = dest_TVar (type_of x) val gspec = Thm.forall_intr (Thm.cterm_of \<^context> x) spec in fun SPEC tm thm = let val gspec' = Drule.instantiate_normalize (TVars.make1 (TV, Thm.ctyp_of_cterm tm), Vars.empty) gspec in thm RS (Thm.forall_elim tm gspec') end end; fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm; val ISPEC = SPEC val ISPECL = fold ISPEC; (* Not optimized! Too complicated. *) local val prop = Thm.prop_of allI val [P] = Misc_Legacy.add_term_vars (prop, []) fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty)) fun ctm_theta ctxt = map (fn (i, (_, tm2)) => let val ctm2 = Thm.cterm_of ctxt tm2 in ((i, Thm.typ_of_cterm ctm2), ctm2) end) fun certify ctxt (ty_theta,tm_theta) = (TVars.make (cty_theta ctxt (Vartab.dest ty_theta)), Vars.make (ctm_theta ctxt (Vartab.dest tm_theta))) in fun GEN ctxt v th = let val gth = Thm.forall_intr v th val thy = Proof_Context.theory_of ctxt val Const(\<^const_name>\<open>Pure.all\<close>,_)$Abs(x,ty,rst) = Thm.prop_of gth val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty); val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI val thm = Thm.implies_elim allI2 gth val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm val prop' = tp $ (A $ Abs(x,ty,M)) in ALPHA thm (Thm.cterm_of ctxt prop') end end; fun GENL ctxt = fold_rev (GEN ctxt); fun GEN_ALL ctxt thm = let val prop = Thm.prop_of thm val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, [])) in GENL ctxt vlist thm end; fun MATCH_MP th1 th2 = if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1))) then MATCH_MP (th1 RS spec) th2 else MP th1 th2; (*---------------------------------------------------------------------------- * Existentials *---------------------------------------------------------------------------*) (*--------------------------------------------------------------------------- * Existential elimination * * A1 |- ?x.t[x] , A2, "t[v]" |- t' * ------------------------------------ (variable v occurs nowhere) * A1 u A2 |- t' * *---------------------------------------------------------------------------*) fun CHOOSE ctxt (fvar, exth) fact = let val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth))) val redex = Dcterm.capply lam fvar val t$u = Thm.term_of redex val residue = Thm.cterm_of ctxt (Term.betapply (t, u)) in GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE}) handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg end; fun EXISTS ctxt (template,witness) thm = let val abstr = #2 (Dcterm.dest_comb template) in thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI) handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg end; (*---------------------------------------------------------------------------- * * A |- M[x_1,...,x_n] * ---------------------------- [(x |-> y)_1,...,(x |-> y)_n] * A |- ?y_1...y_n. M * *---------------------------------------------------------------------------*) (* Could be improved, but needs "subst_free" for certified terms *) fun IT_EXISTS ctxt blist th = let val blist' = map (apply2 Thm.term_of) blist fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M}) in fold_rev (fn (b as (r1,r2)) => fn thm => EXISTS ctxt (ex r2 (subst_free [b] (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1) thm) blist' th end; (*---------------------------------------------------------------------------- * Rewriting *---------------------------------------------------------------------------*) fun SUBS ctxt thl = rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl); fun rew_conv ctxt ctm = Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) (Variable.declare_term (Thm.term_of ctm) ctxt) ctm; fun simpl_conv ctxt thl ctm = HOLogic.mk_obj_eq (rew_conv (ctxt |> Simplifier.add_simps thl) ctm); fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc}; (*--------------------------------------------------------------------------- * TERMINATION CONDITION EXTRACTION *---------------------------------------------------------------------------*) (* Object language quantifier, i.e., "!" *) fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M}; (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) fun is_cong thm = case (Thm.prop_of thm) of (Const(\<^const_name>\<open>Pure.imp\<close>,_)$(Const(\<^const_name>\<open>Trueprop\<close> (Const(\<^const_name>\<open>Pure.eq\<close>,_) $ (Const (\<^const_name>\<open>Wfrec.cut\<close> false | _ => true; fun dest_equal(Const (\<^const_name>\<open>Pure.eq\<close>,_) $ (Const (\<^const_name>\<open>Trueprop\<close>,_) $ lhs) $ (Const (\<^const_name>\<open>Trueprop\<close>,_) $ rhs)) = {lhs=lhs, rhs=rhs} | dest_equal(Const (\<^const_name>\<open>Pure.eq\<close>,_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} | dest_equal tm = USyntax.dest_eq tm; fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); fun dest_all used (Const(\<^const_name>\<open>Pure.all\<close>,_) $ (a as Abs _)) = USyntax.dest | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!"; val is_all = can (dest_all []); fun strip_all used fm = if (is_all fm) then let val ({Bvar, Body}, used') = dest_all used fm val (bvs, core, used'') = strip_all used' Body in ((Bvar::bvs), core, used'') end else ([], fm, used); fun list_break_all(Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs (s,ty,body)) = let val (L,core) = list_break_all body in ((s,ty)::L, core) end | list_break_all tm = ([],tm); (*--------------------------------------------------------------------------- * Rename a term of the form * * !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn * ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn. * to one of * * !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn * ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn. * * This prevents name problems in extraction, and helps the result to read * better. There is a problem with varstructs, since they can introduce more * than n variables, and some extra reasoning needs to be done. *---------------------------------------------------------------------------*) fun get ([],_,L) = rev L | get (ant::rst,n,L) = case (list_break_all ant) of ([],_) => get (rst, n+1,L) | (_,body) => let val eq = Logic.strip_imp_concl body val (f,_) = USyntax.strip_comb (get_lhs eq) val (vstrl,_) = USyntax.strip_abs f val names = Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl) in get (rst, n+1, (names,n)::L) end handle TERM _ => get (rst, n+1, L) | Utils.ERR _ => get (rst, n+1, L); (* Note: Thm.rename_params_rule counts from 1, not 0 *) fun rename thm = let val ants = Logic.strip_imp_prems (Thm.prop_of thm) val news = get (ants,1,[]) in fold Thm.rename_params_rule news thm end; (*--------------------------------------------------------------------------- * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml) *---------------------------------------------------------------------------*) fun list_beta_conv tm = let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl fun iter [] = Thm.reflexive tm | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v)) in iter end; (*--------------------------------------------------------------------------- * Trace information for the rewriter *---------------------------------------------------------------------------*) val tracing = Unsynchronized.ref false; fun say s = if !tracing then writeln s else (); fun print_thms ctxt s L = say (cat_lines (s :: map (Thm.string_of_thm ctxt) L)); fun print_term ctxt s t = say (cat_lines [s, Syntax.string_of_term ctxt t]); (*--------------------------------------------------------------------------- * General abstraction handlers, should probably go in USyntax. *---------------------------------------------------------------------------*) fun mk_aabs (vstr, body) = USyntax.mk_abs {Bvar = vstr, Body = body} handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body}; fun list_mk_aabs (vstrl,tm) = fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm; fun dest_aabs used tm = let val ({Bvar,Body}, used') = USyntax.dest_abs used tm in (Bvar, Body, used') end handle Utils.ERR _ => let val {varstruct, body, used} = USyntax.dest_pabs used tm in (varstruct, body, used) end; fun strip_aabs used tm = let val (vstr, body, used') = dest_aabs used tm val (bvs, core, used'') = strip_aabs used' body in (vstr::bvs, core, used'') end handle Utils.ERR _ => ([], tm, used); fun dest_combn tm 0 = (tm,[]) | dest_combn tm n = let val {Rator,Rand} = USyntax.dest_comb tm val (f,rands) = dest_combn Rator (n-1) in (f,Rand::rands) end; local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end fun mk_fst tm = let val ty as Type(\<^type_name>\<open>Product_Type.prod\<close>, [fty,sty]) = type_of tm in Const (\<^const_name>\<open>Product_Type.fst\<close>, ty --> fty) $ tm end fun mk_snd tm = let val ty as Type(\<^type_name>\<open>Product_Type.prod\<close>, [fty,sty]) = type_of tm in Const (\<^const_name>\<open>Product_Type.snd\<close>, ty --> sty) $ tm end in fun XFILL tych x vstruct = let fun traverse p xocc L = if (is_Free p) then tych xocc::L else let val (p1,p2) = dest_pair p in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L) end in traverse vstruct x [] end end; (*--------------------------------------------------------------------------- * Replace a free tuple (vstr) by a universally quantified variable (a). * Note that the notion of "freeness" for a tuple is different than for a * variable: if variables in the tuple also occur in any other place than * an occurrences of the tuple, they aren't "free" (which is thus probably * the wrong word to use). *---------------------------------------------------------------------------*) fun VSTRUCT_ELIM ctxt tych a vstr th = let val L = USyntax.free_vars_lr vstr val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr))) val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th) val thm2 = forall_intr_list (map tych L) thm1 val thm3 = forall_elim_list (XFILL tych a vstr) thm2 in refl RS rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3 end; fun PGEN ctxt tych a vstr th = let val a1 = tych a in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end; (*--------------------------------------------------------------------------- * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into * * (([x,y],N),vstr) *---------------------------------------------------------------------------*) fun dest_pbeta_redex used M n = let val (f,args) = dest_combn M n val _ = dest_aabs used f in (strip_aabs used f,args) end; fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M; fun dest_impl tm = let val ants = Logic.strip_imp_prems tm val eq = Logic.strip_imp_concl tm in (ants,get_lhs eq) end; fun restricted t = is_some (USyntax.find_term (fn (Const(\<^const_name>\<open>Wfrec.cut\<close>,_)) =>true | _ => false) t) fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th = let val globals = func::G val ctxt0 = empty_simpset main_ctxt val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection]; val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref val cut_lemma' = cut_lemma RS eq_reflection fun prover used ctxt thm = let fun cong_prover ctxt thm = let val _ = say "cong_prover:" val cntxt = Simplifier.prems_of ctxt val _ = print_thms ctxt "cntxt:" cntxt val _ = say "cong rule:" val _ = say (Thm.string_of_thm ctxt thm) (* Unquantified eliminate *) fun uq_eliminate (thm,imp) = let val tych = Thm.cterm_of ctxt val _ = print_term ctxt "To eliminate:" imp val ants = map tych (Logic.strip_imp_prems imp) val eq = Logic.strip_imp_concl imp val lhs = tych(get_lhs eq) val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt val lhs_eq_lhs1 = Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs handle Utils.ERR _ => Thm.reflexive lhs val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1] val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 val lhs_eeq_lhs2 = HOLogic.mk_obj_eq lhs_eq_lhs2 in lhs_eeq_lhs2 COMP thm end fun pq_eliminate (thm, vlist, imp_body, lhs_eq) = let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist) val _ = forall (op aconv) (ListPair.zip (vlist, args)) orelse error "assertion failed in CONTEXT_REWRITE_RULE" val imp_body1 = subst_free (ListPair.zip (args, vstrl)) imp_body val tych = Thm.cterm_of ctxt val ants1 = map tych (Logic.strip_imp_prems imp_body1) val eq1 = Logic.strip_imp_concl imp_body1 val Q = get_lhs eq1 val QeqQ1 = pbeta_reduce (tych Q) val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1)) val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt val Q1eeqQ2 = Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1 handle Utils.ERR _ => Thm.reflexive Q1 val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2)) val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection) val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ => (HOLogic.mk_obj_eq Q2eeqQ3 RS (HOLogic.mk_obj_eq thA RS trans)) RS eq_reflection val impth = implies_intr_list ants1 QeeqQ3 val impth1 = HOLogic.mk_obj_eq impth (* Need to abstract *) val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1 in ant_th COMP thm end fun q_eliminate (thm, imp) = let val (vlist, imp_body, used') = strip_all used imp val (ants,Q) = dest_impl imp_body in if (pbeta_redex Q) (length vlist) then pq_eliminate (thm, vlist, imp_body, Q) else let val tych = Thm.cterm_of ctxt val ants1 = map tych ants val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt val Q_eeq_Q1 = Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' (tych Q) handle Utils.ERR _ => Thm.reflexive (tych Q) val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 val lhs_eq_lhs2 = HOLogic.mk_obj_eq lhs_eeq_lhs2 val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2 in ant_th COMP thm end end fun eliminate thm = case Thm.prop_of thm of Const(\<^const_name>\<open>Pure.imp\<close>,_) $ imp $ _ => eliminate (if not(is_all imp) then uq_eliminate (thm, imp) else q_eliminate (thm, imp)) (* Assume that the leading constant is ==, *) | _ => thm (* if it is not a ==> *) in SOME(eliminate (rename thm)) end handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *) fun restrict_prover ctxt thm = let val _ = say "restrict_prover:" val cntxt = rev (Simplifier.prems_of ctxt) val _ = print_thms ctxt "cntxt:" cntxt val Const(\<^const_name>\<open>Pure.imp\<close>,_) $ (Const(\<^const_name>\<open>Trueprop\<clo Thm.prop_of thm fun genl tm = let val vlist = subtract (op aconv) globals (Misc_Legacy.add_term_frees(tm,[])) in fold_rev Forall vlist tm end (*-------------------------------------------------------------- * This actually isn't quite right, since it will think that * not-fully applied occs. of "f" in the context mean that the * current call is nested. The real solution is to pass in a * term "f v1..vn" which is a pattern that any full application * of "f" will match. *-------------------------------------------------------------*) val func_name = dest_Const_name func fun is_func (Const (name,_)) = (name = func_name) | is_func _ = false val rcontext = rev cntxt val cncl = HOLogic.dest_Trueprop o Thm.prop_of val antl = case rcontext of [] => [] | _ => [USyntax.list_mk_conj(map cncl rcontext)] val TC = genl(USyntax.list_mk_imp(antl, A)) val _ = print_term ctxt "func:" func val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC) val _ = tc_list := (TC :: !tc_list) val nestedp = is_some (USyntax.find_term is_func TC) val _ = if nestedp then say "nested" else say "not_nested" val th' = if nestedp then raise RULES_ERR "solver" "nested function" else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC) in case rcontext of [] => SPEC_ALL(ASSUME cTC) | _ => MP (SPEC_ALL (ASSUME cTC)) (LIST_CONJ rcontext) end val th'' = th' RS thm in SOME (th'') end handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *) in (if (is_cong thm) then cong_prover else restrict_prover) ctxt thm end val ctm = Thm.cprop_of th val names = Misc_Legacy.add_term_names (Thm.term_of ctm, []) val th1 = Simplifier.rewrite_cterm (false, true, false) (prover names) (ctxt0 |> Simplifier.add_simp cut_lemma' |> fold Simplifier.add_eqcong val th2 = Thm.equal_elim th1 th in (th2, filter_out restricted (!tc_list)) end; fun prove ctxt strict t tac = let val ctxt' = Proof_Context.augment t ctxt; in if strict then Goal.prove ctxt' [] [] t (tac o #context) else Goal.prove ctxt' [] [] t (tac o #context) handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg) end; end; (*** theory operations ***) structure Thry: THRY = struct fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg}; (*--------------------------------------------------------------------------- * Matching *---------------------------------------------------------------------------*) local fun tybind (ixn, (S, T)) = (TVar (ixn, S), T); in fun match_term thry pat ob = let val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty); fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t) in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) end; fun match_type thry pat ob = map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty)); end; (*--------------------------------------------------------------------------- * Typing *---------------------------------------------------------------------------*) fun typecheck thy t = Thm.global_cterm_of thy t handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg | TERM (msg, _) => raise THRY_ERR "typecheck" msg; (*--------------------------------------------------------------------------- * Get information about datatypes *---------------------------------------------------------------------------*) fun match_info thy dtco = case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco, BNF_LFP_Compat.get_constrs thy dtco) of (SOME {case_name, ... }, SOME constructors) => SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = ma | _ => NONE; fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting NONE => NONE | SOME {nchotomy, ...} => SOME {nchotomy = nchotomy, constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco}; fun extract_info thy = let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nes in {case_congs = map (mk_meta_eq o #case_cong) infos, case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos} end; end; (*** first part of main module ***) structure Prim: PRIM = struct val trace = Unsynchronized.ref false; fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg}; val concl = #2 o Rules.dest_thm; val list_mk_type = Utils.end_itlist (curry (op -->)); (*--------------------------------------------------------------------------- * The next function is common to pattern-match translation and * proof of completeness of cases for the induction theorem. * * The curried function "gvvariant" returns a function to generate distinct * variables that are guaranteed not to be in names. The names of * the variables go u, v, ..., z, aa, ..., az, ... The returned * function contains embedded refs! *---------------------------------------------------------------------------*) fun gvvariant names = let val slist = Unsynchronized.ref names val vname = Unsynchronized.ref "u" fun new() = if member (op =) (!slist) (!vname) then (vname := Symbol.bump_string (!vname); new()) else (slist := !vname :: !slist; !vname) in fn ty => Free(new(), ty) end; (*--------------------------------------------------------------------------- * Used in induction theorem production. This is the simple case of * partitioning up pattern rows by the leading constructor. *---------------------------------------------------------------------------*) fun ipartition gv (constructors,rows) = let fun pfail s = raise TFL_ERR "partition.part" s fun part {constrs = [], rows = [], A} = rev A | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" | part {constrs = c::crst, rows, A} = let val (c, T) = dest_Const c val L = binder_types T val (in_group, not_in_group) = fold_rev (fn (row as (p::rst, rhs)) => fn (in_group,not_in_group) => let val (pc,args) = USyntax.strip_comb p in if (dest_Const_name pc = c) then ((args@rst, rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]) val col_types = Utils.take type_of (length L, #1(hd in_group)) in part{constrs = crst, rows = not_in_group, A = {constructor = c, new_formals = map gv col_types, group = in_group}::A} end in part{constrs = constructors, rows = rows, A = []} end; (*--------------------------------------------------------------------------- * Each pattern carries with it a tag (i,b) where * i is the clause it came from and * b=true indicates that clause was given by the user * (or is an instantiation of a user supplied pattern) * b=false --> i = ~1 *---------------------------------------------------------------------------*) type pattern = term * (int * bool) fun pattern_map f (tm,x) = (f tm, x); fun pattern_subst theta = pattern_map (subst_free theta); val pat_of = fst; fun row_of_pat x = fst (snd x); fun given x = snd (snd x); (*--------------------------------------------------------------------------- * Produce an instance of a constructor, plus genvars for its arguments. *---------------------------------------------------------------------------*) fun fresh_constr ty_match colty gv c = let val Ty = dest_Const_type c val L = binder_types Ty and ty = body_type Ty val ty_theta = ty_match ty colty val c' = USyntax.inst ty_theta c val gvars = map (USyntax.inst ty_theta o gv) L in (c', gvars) end; (*--------------------------------------------------------------------------- * Goes through a list of rows and picks out the ones beginning with a * pattern with constructor = name. --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28