--- a/src/HOL/Tools/TFL/tfl.ML Fri Jun 19 07:53:35 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1003 +0,0 @@
-(* Title: HOL/Tools/TFL/tfl.ML
- Author: Konrad Slind, Cambridge University Computer Laboratory
-
-First part of main module.
-*)
-
-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 wfrec_eqns: theory -> xstring -> thm list -> term list ->
- {WFR: term,
- SV: term list,
- proto_def: term,
- extracta: (thm * term list) list,
- pats: pattern list}
- val lazyR_def: theory -> xstring -> thm list -> term list ->
- {theory: theory,
- rules: thm,
- R: term,
- SV: term list,
- full_pats_TCs: (term * term list) list,
- patterns : pattern list}
- val mk_induction: theory ->
- {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
- val postprocess: Proof.context -> bool ->
- {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
- {rules: thm, induction: thm, TCs: term list list} ->
- {rules: thm, induction: thm, nested_tcs: thm list}
-end;
-
-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 hyp = #1 o Rules.dest_thm;
-
-val list_mk_type = Utils.end_itlist (curry (op -->));
-
-fun front_last [] = raise TFL_ERR "front_last" "empty list"
- | front_last [x] = ([],x)
- | front_last (h::t) =
- let val (pref,x) = front_last t
- in
- (h::pref,x)
- end;
-
-
-(*---------------------------------------------------------------------------
- * 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 (#1(dest_Const 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 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.
- *---------------------------------------------------------------------------*)
-fun mk_group name rows =
- fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
- fn (in_group,not_in_group) =>
- let val (pc,args) = USyntax.strip_comb p
- in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
- then (((prfx,args@rst), rhs)::in_group, not_in_group)
- else (in_group, row::not_in_group) end)
- rows ([],[]);
-
-(*---------------------------------------------------------------------------
- * Partition the rows. Not efficient: we should use hashing.
- *---------------------------------------------------------------------------*)
-fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows"
- | partition gv ty_match
- (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
-let val fresh = fresh_constr ty_match colty gv
- fun part {constrs = [], rows, A} = rev A
- | part {constrs = c::crst, rows, A} =
- let val (c',gvars) = fresh c
- val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
- val in_group' =
- if (null in_group) (* Constructor not given *)
- then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
- else in_group
- in
- part{constrs = crst,
- rows = not_in_group,
- A = {constructor = c',
- new_formals = gvars,
- group = in_group'}::A}
- end
-in part{constrs=constructors, rows=rows, A=[]}
-end;
-
-(*---------------------------------------------------------------------------
- * Misc. routines used in mk_case
- *---------------------------------------------------------------------------*)
-
-fun mk_pat (c,l) =
- let val L = length (binder_types (type_of c))
- fun build (prfx,tag,plist) =
- let val (args, plist') = chop L plist
- in (prfx,tag,list_comb(c,args)::plist') end
- in map build l end;
-
-fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
- | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";
-
-fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
- | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats";
-
-
-(*----------------------------------------------------------------------------
- * Translation of pattern terms into nested case expressions.
- *
- * This performs the translation and also builds the full set of patterns.
- * Thus it supports the construction of induction theorems even when an
- * incomplete set of patterns is given.
- *---------------------------------------------------------------------------*)
-
-fun mk_case ty_info ty_match usednames range_ty =
- let
- fun mk_case_fail s = raise TFL_ERR "mk_case" s
- val fresh_var = gvvariant usednames
- val divide = partition fresh_var ty_match
- fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
- | expand constructors ty (row as ((prfx, p::rst), rhs)) =
- if (is_Free p)
- then let val fresh = fresh_constr ty_match ty fresh_var
- fun expnd (c,gvs) =
- let val capp = list_comb(c,gvs)
- in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
- end
- in map expnd (map fresh constructors) end
- else [row]
- fun mk{rows=[],...} = mk_case_fail"no rows"
- | mk{path=[], rows = ((prfx, []), (tm,tag))::_} = (* Done *)
- ([(prfx,tag,[])], tm)
- | mk{path=[], rows = _::_} = mk_case_fail"blunder"
- | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
- mk{path = path,
- rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
- | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
- let val (pat_rectangle,rights) = ListPair.unzip rows
- val col0 = map(hd o #2) pat_rectangle
- in
- if (forall is_Free col0)
- then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
- (ListPair.zip (col0, rights))
- val pat_rectangle' = map v_to_prfx pat_rectangle
- val (pref_patl,tm) = mk{path = rstp,
- rows = ListPair.zip (pat_rectangle',
- rights')}
- in (map v_to_pats pref_patl, tm)
- end
- else
- let val pty as Type (ty_name,_) = type_of p
- in
- case (ty_info ty_name)
- of NONE => mk_case_fail("Not a known datatype: "^ty_name)
- | SOME{case_const,constructors} =>
- let
- val case_const_name = #1(dest_Const case_const)
- val nrows = maps (expand constructors pty) rows
- val subproblems = divide(constructors, pty, range_ty, nrows)
- val groups = map #group subproblems
- and new_formals = map #new_formals subproblems
- and constructors' = map #constructor subproblems
- val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
- (ListPair.zip (new_formals, groups))
- val rec_calls = map mk news
- val (pat_rect,dtrees) = ListPair.unzip rec_calls
- val case_functions = map USyntax.list_mk_abs
- (ListPair.zip (new_formals, dtrees))
- val types = map type_of (case_functions@[u]) @ [range_ty]
- val case_const' = Const(case_const_name, list_mk_type types)
- val tree = list_comb(case_const', case_functions@[u])
- val pat_rect1 = flat (ListPair.map mk_pat (constructors', pat_rect))
- in (pat_rect1,tree)
- end
- end end
- in mk
- end;
-
-
-(* Repeated variable occurrences in a pattern are not allowed. *)
-fun FV_multiset tm =
- case (USyntax.dest_term tm)
- of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
- | USyntax.CONST _ => []
- | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
- | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
-
-fun no_repeat_vars thy pat =
- let fun check [] = true
- | check (v::rst) =
- if member (op aconv) rst v then
- raise TFL_ERR "no_repeat_vars"
- (quote (#1 (dest_Free v)) ^
- " occurs repeatedly in the pattern " ^
- quote (Syntax.string_of_term_global thy pat))
- else check rst
- in check (FV_multiset pat)
- end;
-
-fun dest_atom (Free p) = p
- | dest_atom (Const p) = p
- | dest_atom _ = raise TFL_ERR "dest_atom" "function name not an identifier";
-
-fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
-
-local fun mk_functional_err s = raise TFL_ERR "mk_functional" s
- fun single [_$_] =
- mk_functional_err "recdef does not allow currying"
- | single [f] = f
- | single fs =
- (*multiple function names?*)
- if length (distinct same_name fs) < length fs
- then mk_functional_err
- "The function being declared appears with multiple types"
- else mk_functional_err
- (string_of_int (length fs) ^
- " distinct function names being declared")
-in
-fun mk_functional thy clauses =
- let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
- handle TERM _ => raise TFL_ERR "mk_functional"
- "recursion equations must use the = relation")
- val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
- val atom = single (distinct (op aconv) funcs)
- val (fname,ftype) = dest_atom atom
- val dummy = map (no_repeat_vars thy) pats
- val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
- map_index (fn (i, t) => (t,(i,true))) R)
- val names = List.foldr Misc_Legacy.add_term_names [] R
- val atype = type_of(hd pats)
- and aname = singleton (Name.variant_list names) "a"
- val a = Free(aname,atype)
- val ty_info = Thry.match_info thy
- val ty_match = Thry.match_type thy
- val range_ty = type_of (hd R)
- val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
- {path=[a], rows=rows}
- val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
- handle Match => mk_functional_err "error in pattern-match translation"
- val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
- val finals = map row_of_pat patts2
- val originals = map (row_of_pat o #2) rows
- val dummy = case (subtract (op =) finals originals)
- of [] => ()
- | L => mk_functional_err
- ("The following clauses are redundant (covered by preceding clauses): " ^
- commas (map (fn i => string_of_int (i + 1)) L))
- in {functional = Abs(Long_Name.base_name fname, ftype,
- abstract_over (atom, absfree (aname,atype) case_tm)),
- pats = patts2}
-end end;
-
-
-(*----------------------------------------------------------------------------
- *
- * PRINCIPLES OF DEFINITION
- *
- *---------------------------------------------------------------------------*)
-
-
-(*For Isabelle, the lhs of a definition must be a constant.*)
-fun const_def sign (c, Ty, rhs) =
- singleton (Syntax.check_terms (Proof_Context.init_global sign))
- (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
-
-(*Make all TVars available for instantiation by adding a ? to the front*)
-fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
- | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
- | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
-
-local
- val f_eq_wfrec_R_M =
- #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
- val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
- val (fname,_) = dest_Free f
- val (wfrec,_) = USyntax.strip_comb rhs
-in
-
-fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy =
- let
- val def_name = Thm.def_name (Long_Name.base_name fid)
- val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
- val def_term = const_def thy (fid, Ty, wfrec_R_M)
- val ([def], thy') =
- Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
- in (def, thy') end;
-
-end;
-
-
-
-(*---------------------------------------------------------------------------
- * This structure keeps track of congruence rules that aren't derived
- * from a datatype definition.
- *---------------------------------------------------------------------------*)
-fun extraction_thms thy =
- let val {case_rewrites,case_congs} = Thry.extract_info thy
- in (case_rewrites, case_congs)
- end;
-
-
-(*---------------------------------------------------------------------------
- * Pair patterns with termination conditions. The full list of patterns for
- * a definition is merged with the TCs arising from the user-given clauses.
- * There can be fewer clauses than the full list, if the user omitted some
- * cases. This routine is used to prepare input for mk_induction.
- *---------------------------------------------------------------------------*)
-fun merge full_pats TCs =
-let fun insert (p,TCs) =
- let fun insrt ((x as (h,[]))::rst) =
- if (p aconv h) then (p,TCs)::rst else x::insrt rst
- | insrt (x::rst) = x::insrt rst
- | insrt[] = raise TFL_ERR "merge.insert" "pattern not found"
- in insrt end
- fun pass ([],ptcl_final) = ptcl_final
- | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
-in
- pass (TCs, map (fn p => (p,[])) full_pats)
-end;
-
-
-fun givens pats = map pat_of (filter given pats);
-
-fun post_definition ctxt meta_tflCongs (def, pats) =
- let val thy = Proof_Context.theory_of ctxt
- val tych = Thry.typecheck thy
- val f = #lhs(USyntax.dest_eq(concl def))
- val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
- val pats' = filter given pats
- val given_pats = map pat_of pats'
- val rows = map row_of_pat pats'
- val WFR = #ant(USyntax.dest_imp(concl corollary))
- val R = #Rand(USyntax.dest_comb WFR)
- val corollary' = Rules.UNDISCH corollary (* put WF R on assums *)
- val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
- val (case_rewrites,context_congs) = extraction_thms thy
- (*case_ss causes minimal simplification: bodies of case expressions are
- not simplified. Otherwise large examples (Red-Black trees) are too
- slow.*)
- val case_simpset =
- put_simpset HOL_basic_ss ctxt
- addsimps case_rewrites
- |> fold (Simplifier.add_cong o #case_cong_weak o snd)
- (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
- val corollaries' = map (Simplifier.simplify case_simpset) corollaries
- val extract =
- Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
- val (rules, TCs) = ListPair.unzip (map extract corollaries')
- val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
- val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
- val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
- in
- {rules = rules1,
- rows = rows,
- full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
- TCs = TCs}
- end;
-
-
-(*---------------------------------------------------------------------------
- * Perform the extraction without making the definition. Definition and
- * extraction commute for the non-nested case. (Deferred recdefs)
- *
- * The purpose of wfrec_eqns is merely to instantiate the recursion theorem
- * and extract termination conditions: no definition is made.
- *---------------------------------------------------------------------------*)
-
-fun wfrec_eqns thy fid tflCongs eqns =
- let val ctxt = Proof_Context.init_global thy
- val {lhs,rhs} = USyntax.dest_eq (hd eqns)
- val (f,args) = USyntax.strip_comb lhs
- val (fname,fty) = dest_atom f
- val (SV,a) = front_last args (* SV = schematic variables *)
- val g = list_comb(f,SV)
- val h = Free(fname,type_of g)
- val eqns1 = map (subst_free[(g,h)]) eqns
- val {functional as Abs(x, Ty, _), pats} = mk_functional thy eqns1
- val given_pats = givens pats
- (* val f = Free(x,Ty) *)
- val Type("fun", [f_dty, f_rty]) = Ty
- val dummy = if x<>fid then
- raise TFL_ERR "wfrec_eqns"
- ("Expected a definition of " ^
- quote fid ^ " but found one of " ^
- quote x)
- else ()
- val (case_rewrites,context_congs) = extraction_thms thy
- val tych = Thry.typecheck thy
- val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
- val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
- val R = Free (singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] eqns)) Rname,
- Rtype)
- val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
- val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
- val dummy =
- if !trace then
- writeln ("ORIGINAL PROTO_DEF: " ^
- Syntax.string_of_term_global thy proto_def)
- else ()
- val R1 = USyntax.rand WFR
- val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
- val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
- val corollaries' = map (rewrite_rule ctxt case_rewrites) corollaries
- val extract =
- Rules.CONTEXT_REWRITE_RULE ctxt (f, R1::SV, @{thm cut_apply}, tflCongs @ context_congs)
- in {proto_def = proto_def,
- SV=SV,
- WFR=WFR,
- pats=pats,
- extracta = map extract corollaries'}
- end;
-
-
-(*---------------------------------------------------------------------------
- * Define the constant after extracting the termination conditions. The
- * wellfounded relation used in the definition is computed by using the
- * choice operator on the extracted conditions (plus the condition that
- * such a relation must be wellfounded).
- *---------------------------------------------------------------------------*)
-
-fun lazyR_def thy fid tflCongs eqns =
- let val {proto_def,WFR,pats,extracta,SV} =
- wfrec_eqns thy fid tflCongs eqns
- val R1 = USyntax.rand WFR
- val f = #lhs(USyntax.dest_eq proto_def)
- val (extractants,TCl) = ListPair.unzip extracta
- val dummy = if !trace
- then writeln (cat_lines ("Extractants =" ::
- map (Display.string_of_thm_global thy) extractants))
- else ()
- val TCs = fold_rev (union (op aconv)) TCl []
- val full_rqt = WFR::TCs
- val R' = USyntax.mk_select{Bvar=R1, Body=USyntax.list_mk_conj full_rqt}
- val R'abs = USyntax.rand R'
- val proto_def' = subst_free[(R1,R')] proto_def
- val dummy = if !trace then writeln ("proto_def' = " ^
- Syntax.string_of_term_global
- thy proto_def')
- else ()
- val {lhs,rhs} = USyntax.dest_eq proto_def'
- val (c,args) = USyntax.strip_comb lhs
- val (name,Ty) = dest_atom c
- val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
- val ([def0], thy') =
- thy
- |> Global_Theory.add_defs false
- [Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
- val def = Thm.unvarify_global def0;
- val ctxt' = Syntax.init_pretty_global thy';
- val dummy =
- if !trace then writeln ("DEF = " ^ Display.string_of_thm ctxt' def)
- else ()
- (* val fconst = #lhs(USyntax.dest_eq(concl def)) *)
- val tych = Thry.typecheck thy'
- val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
- (*lcp: a lot of object-logic inference to remove*)
- val baz = Rules.DISCH_ALL
- (fold_rev Rules.DISCH full_rqt_prop
- (Rules.LIST_CONJ extractants))
- val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm ctxt' baz) else ()
- val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
- val SV' = map tych SV;
- val SVrefls = map Thm.reflexive SV'
- val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
- SVrefls def)
- RS meta_eq_to_obj_eq
- val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN ctxt' (tych R1) baz)) def0
- val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
- val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
- theory Hilbert_Choice*)
- ML_Context.thm "Hilbert_Choice.tfl_some"
- handle ERROR msg => cat_error msg
- "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
- val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
- in {theory = thy', R=R1, SV=SV,
- rules = fold (fn a => fn b => Rules.MP b a) (Rules.CONJUNCTS bar) def',
- full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
- patterns = pats}
- end;
-
-
-
-(*----------------------------------------------------------------------------
- *
- * INDUCTION THEOREM
- *
- *---------------------------------------------------------------------------*)
-
-
-(*------------------------ Miscellaneous function --------------------------
- *
- * [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n]
- * -----------------------------------------------------------
- * ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
- * ...
- * (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
- *
- * This function is totally ad hoc. Used in the production of the induction
- * theorem. The nchotomy theorem can have clauses that look like
- *
- * ?v1..vn. z = C vn..v1
- *
- * in which the order of quantification is not the order of occurrence of the
- * quantified variables as arguments to C. Since we have no control over this
- * aspect of the nchotomy theorem, we make the correspondence explicit by
- * pairing the incoming new variable with the term it gets beta-reduced into.
- *---------------------------------------------------------------------------*)
-
-fun alpha_ex_unroll (xlist, tm) =
- let val (qvars,body) = USyntax.strip_exists tm
- val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
- val plist = ListPair.zip (vlist, xlist)
- val args = map (the o AList.lookup (op aconv) plist) qvars
- handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
- fun build ex [] = []
- | build (_$rex) (v::rst) =
- let val ex1 = Term.betapply(rex, v)
- in ex1 :: build ex1 rst
- end
- val (nex::exl) = rev (tm::build tm args)
- in
- (nex, ListPair.zip (args, rev exl))
- end;
-
-
-
-(*----------------------------------------------------------------------------
- *
- * PROVING COMPLETENESS OF PATTERNS
- *
- *---------------------------------------------------------------------------*)
-
-fun mk_case ty_info usednames thy =
- let
- val ctxt = Proof_Context.init_global thy
- val divide = ipartition (gvvariant usednames)
- val tych = Thry.typecheck thy
- fun tych_binding(x,y) = (tych x, tych y)
- fun fail s = raise TFL_ERR "mk_case" s
- fun mk{rows=[],...} = fail"no rows"
- | mk{path=[], rows = [([], (thm, bindings))]} =
- Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
- | mk{path = u::rstp, rows as (p::_, _)::_} =
- let val (pat_rectangle,rights) = ListPair.unzip rows
- val col0 = map hd pat_rectangle
- val pat_rectangle' = map tl pat_rectangle
- in
- if (forall is_Free col0) (* column 0 is all variables *)
- then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
- (ListPair.zip (rights, col0))
- in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
- end
- else (* column 0 is all constructors *)
- let val Type (ty_name,_) = type_of p
- in
- case (ty_info ty_name)
- of NONE => fail("Not a known datatype: "^ty_name)
- | SOME{constructors,nchotomy} =>
- let val thm' = Rules.ISPEC (tych u) nchotomy
- val disjuncts = USyntax.strip_disj (concl thm')
- val subproblems = divide(constructors, rows)
- val groups = map #group subproblems
- and new_formals = map #new_formals subproblems
- val existentials = ListPair.map alpha_ex_unroll
- (new_formals, disjuncts)
- val constraints = map #1 existentials
- val vexl = map #2 existentials
- fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
- val news = map (fn (nf,rows,c) => {path = nf@rstp,
- rows = map (expnd c) rows})
- (Utils.zip3 new_formals groups constraints)
- val recursive_thms = map mk news
- val build_exists = Library.foldr
- (fn((x,t), th) =>
- Rules.CHOOSE ctxt (tych x, Rules.ASSUME (tych t)) th)
- val thms' = ListPair.map build_exists (vexl, recursive_thms)
- val same_concls = Rules.EVEN_ORS thms'
- in Rules.DISJ_CASESL thm' same_concls
- end
- end end
- in mk
- end;
-
-
-fun complete_cases thy =
- let val ctxt = Proof_Context.init_global thy
- val tych = Thry.typecheck thy
- val ty_info = Thry.induct_info thy
- in fn pats =>
- let val names = List.foldr Misc_Legacy.add_term_names [] pats
- val T = type_of (hd pats)
- val aname = singleton (Name.variant_list names) "a"
- val vname = singleton (Name.variant_list (aname::names)) "v"
- val a = Free (aname, T)
- val v = Free (vname, T)
- val a_eq_v = HOLogic.mk_eq(a,v)
- val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
- (Rules.REFL (tych a))
- val th0 = Rules.ASSUME (tych a_eq_v)
- val rows = map (fn x => ([x], (th0,[]))) pats
- in
- Rules.GEN ctxt (tych a)
- (Rules.RIGHT_ASSOC ctxt
- (Rules.CHOOSE ctxt (tych v, ex_th0)
- (mk_case ty_info (vname::aname::names)
- thy {path=[v], rows=rows})))
- end end;
-
-
-(*---------------------------------------------------------------------------
- * Constructing induction hypotheses: one for each recursive call.
- *
- * Note. R will never occur as a variable in the ind_clause, because
- * to do so, it would have to be from a nested definition, and we don't
- * allow nested defns to have R variable.
- *
- * Note. When the context is empty, there can be no local variables.
- *---------------------------------------------------------------------------*)
-(*
-local infix 5 ==>
- fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
-in
-fun build_ih f P (pat,TCs) =
- let val globals = USyntax.free_vars_lr pat
- fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
- fun dest_TC tm =
- let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
- val (R,y,_) = USyntax.dest_relation R_y_pat
- val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
- in case cntxt
- of [] => (P_y, (tm,[]))
- | _ => let
- val imp = USyntax.list_mk_conj cntxt ==> P_y
- val lvs = gen_rems (op aconv) (USyntax.free_vars_lr imp, globals)
- val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
- in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
- end
- in case TCs
- of [] => (USyntax.list_mk_forall(globals, P$pat), [])
- | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
- val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
- in (USyntax.list_mk_forall(globals,ind_clause), TCs_locals)
- end
- end
-end;
-*)
-
-local infix 5 ==>
- fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
-in
-fun build_ih f (P,SV) (pat,TCs) =
- let val pat_vars = USyntax.free_vars_lr pat
- val globals = pat_vars@SV
- fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
- fun dest_TC tm =
- let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
- val (R,y,_) = USyntax.dest_relation R_y_pat
- val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
- in case cntxt
- of [] => (P_y, (tm,[]))
- | _ => let
- val imp = USyntax.list_mk_conj cntxt ==> P_y
- val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
- val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
- in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
- end
- in case TCs
- of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
- | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
- val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
- in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
- end
- end
-end;
-
-(*---------------------------------------------------------------------------
- * This function makes good on the promise made in "build_ih".
- *
- * Input is tm = "(!y. R y pat ==> P y) ==> P pat",
- * TCs = TC_1[pat] ... TC_n[pat]
- * thm = ih1 /\ ... /\ ih_n |- ih[pat]
- *---------------------------------------------------------------------------*)
-fun prove_case ctxt f (tm,TCs_locals,thm) =
- let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
- val antc = tych(#ant(USyntax.dest_imp tm))
- val thm' = Rules.SPEC_ALL thm
- fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
- fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
- fun mk_ih ((TC,locals),th2,nested) =
- Rules.GENL ctxt (map tych locals)
- (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
- else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
- else Rules.MP th2 TC)
- in
- Rules.DISCH antc
- (if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
- then let val th1 = Rules.ASSUME antc
- val TCs = map #1 TCs_locals
- val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
- #2 o USyntax.strip_forall) TCs
- val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
- TCs_locals
- val th2list = map (fn t => Rules.SPEC (tych t) th1) ylist
- val nlist = map nested TCs
- val triples = Utils.zip3 TClist th2list nlist
- val Pylist = map mk_ih triples
- in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
- else thm')
- end;
-
-
-(*---------------------------------------------------------------------------
- *
- * x = (v1,...,vn) |- M[x]
- * ---------------------------------------------
- * ?v1 ... vn. x = (v1,...,vn) |- M[x]
- *
- *---------------------------------------------------------------------------*)
-fun LEFT_ABS_VSTRUCT ctxt tych thm =
- let fun CHOOSER v (tm,thm) =
- let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
- in (ex_tm, Rules.CHOOSE ctxt (tych v, Rules.ASSUME (tych ex_tm)) thm)
- end
- val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
- val {lhs,rhs} = USyntax.dest_eq veq
- val L = USyntax.free_vars_lr rhs
- in #2 (fold_rev CHOOSER L (veq,thm)) end;
-
-
-(*----------------------------------------------------------------------------
- * Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)]
- *
- * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
- * recursion induction (Rinduct) by proving the antecedent of Sinduct from
- * the antecedent of Rinduct.
- *---------------------------------------------------------------------------*)
-fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
-let val ctxt = Proof_Context.init_global thy
- val tych = Thry.typecheck thy
- val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
- val (pats,TCsl) = ListPair.unzip pat_TCs_list
- val case_thm = complete_cases thy pats
- val domain = (type_of o hd) pats
- val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
- [] (pats::TCsl))) "P"
- val P = Free(Pname, domain --> HOLogic.boolT)
- val Sinduct = Rules.SPEC (tych P) Sinduction
- val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
- val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
- val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
- val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
- val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
- val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
- val proved_cases = map (prove_case ctxt fconst) tasks
- val v =
- Free (singleton
- (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
- domain)
- val vtyped = tych v
- val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
- val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
- (substs, proved_cases)
- val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
- val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
- val dc = Rules.MP Sinduct dant
- val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
- val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
- val dc' = fold_rev (Rules.GEN ctxt o tych) vars
- (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
-in
- Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
-end
-handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
-
-
-
-
-(*---------------------------------------------------------------------------
- *
- * POST PROCESSING
- *
- *---------------------------------------------------------------------------*)
-
-
-fun simplify_induction thy hth ind =
- let val tych = Thry.typecheck thy
- val (asl,_) = Rules.dest_thm ind
- val (_,tc_eq_tc') = Rules.dest_thm hth
- val tc = USyntax.lhs tc_eq_tc'
- fun loop [] = ind
- | loop (asm::rst) =
- if (can (Thry.match_term thy asm) tc)
- then Rules.UNDISCH
- (Rules.MATCH_MP
- (Rules.MATCH_MP Thms.simp_thm (Rules.DISCH (tych asm) ind))
- hth)
- else loop rst
- in loop asl
-end;
-
-
-(*---------------------------------------------------------------------------
- * The termination condition is an antecedent to the rule, and an
- * assumption to the theorem.
- *---------------------------------------------------------------------------*)
-fun elim_tc tcthm (rule,induction) =
- (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
-
-
-fun trace_thms ctxt s L =
- if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
- else ();
-
-fun trace_cterm ctxt s ct =
- if !trace then
- writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)])
- else ();
-
-
-fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} =
- let
- val thy = Proof_Context.theory_of ctxt;
- val tych = Thry.typecheck thy;
-
- (*---------------------------------------------------------------------
- * Attempt to eliminate WF condition. It's the only assumption of rules
- *---------------------------------------------------------------------*)
- val (rules1,induction1) =
- let val thm =
- Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
- in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
- end handle Utils.ERR _ => (rules,induction);
-
- (*----------------------------------------------------------------------
- * The termination condition (tc) is simplified to |- tc = tc' (there
- * might not be a change!) and then 3 attempts are made:
- *
- * 1. if |- tc = T, then eliminate it with eqT; otherwise,
- * 2. apply the terminator to tc'. If |- tc' = T then eliminate; else
- * 3. replace tc by tc' in both the rules and the induction theorem.
- *---------------------------------------------------------------------*)
-
- fun simplify_tc tc (r,ind) =
- let val tc1 = tych tc
- val _ = trace_cterm ctxt "TC before simplification: " tc1
- val tc_eq = simplifier tc1
- val _ = trace_thms ctxt "result: " [tc_eq]
- in
- elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
- handle Utils.ERR _ =>
- (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
- (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
- terminator)))
- (r,ind)
- handle Utils.ERR _ =>
- (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq),
- simplify_induction thy tc_eq ind))
- end
-
- (*----------------------------------------------------------------------
- * Nested termination conditions are harder to get at, since they are
- * left embedded in the body of the function (and in induction
- * theorem hypotheses). Our "solution" is to simplify them, and try to
- * prove termination, but leave the application of the resulting theorem
- * to a higher level. So things go much as in "simplify_tc": the
- * termination condition (tc) is simplified to |- tc = tc' (there might
- * not be a change) and then 2 attempts are made:
- *
- * 1. if |- tc = T, then return |- tc; otherwise,
- * 2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
- * 3. return |- tc = tc'
- *---------------------------------------------------------------------*)
- fun simplify_nested_tc tc =
- let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
- in
- Rules.GEN_ALL ctxt
- (Rules.MATCH_MP Thms.eqT tc_eq
- handle Utils.ERR _ =>
- (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
- (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
- terminator))
- handle Utils.ERR _ => tc_eq))
- end
-
- (*-------------------------------------------------------------------
- * Attempt to simplify the termination conditions in each rule and
- * in the induction theorem.
- *-------------------------------------------------------------------*)
- fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
- fun loop ([],extras,R,ind) = (rev R, ind, extras)
- | loop ((r,ftcs)::rst, nthms, R, ind) =
- let val tcs = #1(strip_imp (concl r))
- val extra_tcs = subtract (op aconv) tcs ftcs
- val extra_tc_thms = map simplify_nested_tc extra_tcs
- val (r1,ind1) = fold simplify_tc tcs (r,ind)
- val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
- in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
- end
- val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
- val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
-in
- {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
-end;
-
-
-end;