1.1 --- a/TFL/tfl.sml Fri May 05 22:34:40 2000 +0200
1.2 +++ b/TFL/tfl.sml Fri May 05 22:35:51 2000 +0200
1.3 @@ -30,9 +30,9 @@
1.4 fun front_last [] = raise TFL_ERR {func="front_last", mesg="empty list"}
1.5 | front_last [x] = ([],x)
1.6 | front_last (h::t) =
1.7 - let val (pref,x) = front_last t
1.8 - in
1.9 - (h::pref,x)
1.10 + let val (pref,x) = front_last t
1.11 + in
1.12 + (h::pref,x)
1.13 end;
1.14
1.15
1.16 @@ -48,28 +48,28 @@
1.17
1.18 fun congs ths = default_congs @ eq_reflect_list ths;
1.19
1.20 -val default_simps =
1.21 +val default_simps =
1.22 [less_Suc_eq RS iffD2, lex_prod_def, measure_def, inv_image_def];
1.23
1.24
1.25
1.26 (*---------------------------------------------------------------------------
1.27 - * The next function is common to pattern-match translation and
1.28 + * The next function is common to pattern-match translation and
1.29 * proof of completeness of cases for the induction theorem.
1.30 *
1.31 * The curried function "gvvariant" returns a function to generate distinct
1.32 * variables that are guaranteed not to be in names. The names of
1.33 - * the variables go u, v, ..., z, aa, ..., az, ... The returned
1.34 + * the variables go u, v, ..., z, aa, ..., az, ... The returned
1.35 * function contains embedded refs!
1.36 *---------------------------------------------------------------------------*)
1.37 fun gvvariant names =
1.38 let val slist = ref names
1.39 val vname = ref "u"
1.40 - fun new() =
1.41 + fun new() =
1.42 if !vname mem_string (!slist)
1.43 then (vname := bump_string (!vname); new())
1.44 else (slist := !vname :: !slist; !vname)
1.45 - in
1.46 + in
1.47 fn ty => Free(new(), ty)
1.48 end;
1.49
1.50 @@ -95,9 +95,9 @@
1.51 else (in_group, row::not_in_group)
1.52 end) rows ([],[])
1.53 val col_types = U.take type_of (length L, #1(hd in_group))
1.54 - in
1.55 - part{constrs = crst, rows = not_in_group,
1.56 - A = {constructor = c,
1.57 + in
1.58 + part{constrs = crst, rows = not_in_group,
1.59 + A = {constructor = c,
1.60 new_formals = map gv col_types,
1.61 group = in_group}::A}
1.62 end
1.63 @@ -167,10 +167,10 @@
1.64 if (null in_group) (* Constructor not given *)
1.65 then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
1.66 else in_group
1.67 - in
1.68 - part{constrs = crst,
1.69 - rows = not_in_group,
1.70 - A = {constructor = c',
1.71 + in
1.72 + part{constrs = crst,
1.73 + rows = not_in_group,
1.74 + A = {constructor = c',
1.75 new_formals = gvars,
1.76 group = in_group'}::A}
1.77 end
1.78 @@ -194,26 +194,26 @@
1.79
1.80 fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
1.81 | v_to_pats _ = raise TFL_ERR{func="mk_case", mesg="v_to_pats"};
1.82 -
1.83 +
1.84
1.85 (*----------------------------------------------------------------------------
1.86 * Translation of pattern terms into nested case expressions.
1.87 *
1.88 - * This performs the translation and also builds the full set of patterns.
1.89 - * Thus it supports the construction of induction theorems even when an
1.90 + * This performs the translation and also builds the full set of patterns.
1.91 + * Thus it supports the construction of induction theorems even when an
1.92 * incomplete set of patterns is given.
1.93 *---------------------------------------------------------------------------*)
1.94
1.95 fun mk_case ty_info ty_match usednames range_ty =
1.96 - let
1.97 + let
1.98 fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s}
1.99 - val fresh_var = gvvariant usednames
1.100 + val fresh_var = gvvariant usednames
1.101 val divide = partition fresh_var ty_match
1.102 fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
1.103 - | expand constructors ty (row as ((prfx, p::rst), rhs)) =
1.104 - if (is_Free p)
1.105 + | expand constructors ty (row as ((prfx, p::rst), rhs)) =
1.106 + if (is_Free p)
1.107 then let val fresh = fresh_constr ty_match ty fresh_var
1.108 - fun expnd (c,gvs) =
1.109 + fun expnd (c,gvs) =
1.110 let val capp = list_comb(c,gvs)
1.111 in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
1.112 end
1.113 @@ -223,14 +223,14 @@
1.114 | mk{path=[], rows = ((prfx, []), (tm,tag))::_} = (* Done *)
1.115 ([(prfx,tag,[])], tm)
1.116 | mk{path=[], rows = _::_} = mk_case_fail"blunder"
1.117 - | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
1.118 - mk{path = path,
1.119 + | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
1.120 + mk{path = path,
1.121 rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
1.122 | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
1.123 let val (pat_rectangle,rights) = ListPair.unzip rows
1.124 val col0 = map(hd o #2) pat_rectangle
1.125 - in
1.126 - if (forall is_Free col0)
1.127 + in
1.128 + if (forall is_Free col0)
1.129 then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
1.130 (ListPair.zip (col0, rights))
1.131 val pat_rectangle' = map v_to_prfx pat_rectangle
1.132 @@ -246,7 +246,7 @@
1.133 of None => mk_case_fail("Not a known datatype: "^ty_name)
1.134 | Some{case_const,constructors} =>
1.135 let
1.136 - val case_const_name = #1(dest_Const case_const)
1.137 + val case_const_name = #1(dest_Const case_const)
1.138 val nrows = List.concat (map (expand constructors pty) rows)
1.139 val subproblems = divide(constructors, pty, range_ty, nrows)
1.140 val groups = map #group subproblems
1.141 @@ -264,14 +264,14 @@
1.142 val pat_rect1 = List.concat
1.143 (ListPair.map mk_pat (constructors', pat_rect))
1.144 in (pat_rect1,tree)
1.145 - end
1.146 + end
1.147 end end
1.148 in mk
1.149 end;
1.150
1.151
1.152 (* Repeated variable occurrences in a pattern are not allowed. *)
1.153 -fun FV_multiset tm =
1.154 +fun FV_multiset tm =
1.155 case (S.dest_term tm)
1.156 of S.VAR{Name,Ty} => [Free(Name,Ty)]
1.157 | S.CONST _ => []
1.158 @@ -282,39 +282,39 @@
1.159 let fun check [] = true
1.160 | check (v::rst) =
1.161 if mem_term (v,rst) then
1.162 - raise TFL_ERR{func = "no_repeat_vars",
1.163 - mesg = quote(#1(dest_Free v)) ^
1.164 - " occurs repeatedly in the pattern " ^
1.165 - quote (string_of_cterm (Thry.typecheck thy pat))}
1.166 + raise TFL_ERR{func = "no_repeat_vars",
1.167 + mesg = quote(#1(dest_Free v)) ^
1.168 + " occurs repeatedly in the pattern " ^
1.169 + quote (string_of_cterm (Thry.typecheck thy pat))}
1.170 else check rst
1.171 in check (FV_multiset pat)
1.172 end;
1.173
1.174 fun dest_atom (Free p) = p
1.175 | dest_atom (Const p) = p
1.176 - | dest_atom _ = raise TFL_ERR {func="dest_atom",
1.177 - mesg="function name not an identifier"};
1.178 + | dest_atom _ = raise TFL_ERR {func="dest_atom",
1.179 + mesg="function name not an identifier"};
1.180
1.181 fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
1.182
1.183 local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
1.184 - fun single [_$_] =
1.185 - mk_functional_err "recdef does not allow currying"
1.186 + fun single [_$_] =
1.187 + mk_functional_err "recdef does not allow currying"
1.188 | single [f] = f
1.189 - | single fs =
1.190 - (*multiple function names?*)
1.191 - if length (gen_distinct same_name fs) < length fs
1.192 + | single fs =
1.193 + (*multiple function names?*)
1.194 + if length (gen_distinct same_name fs) < length fs
1.195 then mk_functional_err
1.196 - "the function being declared appears with multiple types"
1.197 - else mk_functional_err
1.198 - (Int.toString (length fs) ^
1.199 - " distinct function names being declared")
1.200 + "The function being declared appears with multiple types"
1.201 + else mk_functional_err
1.202 + (Int.toString (length fs) ^
1.203 + " distinct function names being declared")
1.204 in
1.205 fun mk_functional thy clauses =
1.206 let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)
1.207 handle _ => raise TFL_ERR
1.208 - {func = "mk_functional",
1.209 - mesg = "recursion equations must use the = relation"}
1.210 + {func = "mk_functional",
1.211 + mesg = "recursion equations must use the = relation"}
1.212 val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
1.213 val atom = single (gen_distinct (op aconv) funcs)
1.214 val (fname,ftype) = dest_atom atom
1.215 @@ -328,10 +328,10 @@
1.216 val ty_info = Thry.match_info thy
1.217 val ty_match = Thry.match_type thy
1.218 val range_ty = type_of (hd R)
1.219 - val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
1.220 + val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
1.221 {path=[a], rows=rows}
1.222 - val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
1.223 - handle _ => mk_functional_err "error in pattern-match translation"
1.224 + val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
1.225 + handle _ => mk_functional_err "error in pattern-match translation"
1.226 val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1
1.227 val finals = map row_of_pat patts2
1.228 val originals = map (row_of_pat o #2) rows
1.229 @@ -339,10 +339,10 @@
1.230 of [] => ()
1.231 | L => mk_functional_err
1.232 ("The following clauses are redundant (covered by preceding clauses): " ^
1.233 - commas (map Int.toString L) ^ "\n(counting from zero)")
1.234 + commas (map (fn i => Int.toString (i + 1)) L))
1.235 in {functional = Abs(Sign.base_name fname, ftype,
1.236 - abstract_over (atom,
1.237 - absfree(aname,atype, case_tm))),
1.238 + abstract_over (atom,
1.239 + absfree(aname,atype, case_tm))),
1.240 pats = patts2}
1.241 end end;
1.242
1.243 @@ -357,7 +357,7 @@
1.244 (*For Isabelle, the lhs of a definition must be a constant.*)
1.245 fun mk_const_def sign (Name, Ty, rhs) =
1.246 Sign.infer_types sign (K None) (K None) [] false
1.247 - ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
1.248 + ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
1.249 |> #1;
1.250
1.251 (*Make all TVars available for instantiation by adding a ? to the front*)
1.252 @@ -365,22 +365,22 @@
1.253 | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
1.254 | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
1.255
1.256 -local val f_eq_wfrec_R_M =
1.257 +local val f_eq_wfrec_R_M =
1.258 #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
1.259 val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
1.260 val (fname,_) = dest_Free f
1.261 val (wfrec,_) = S.strip_comb rhs
1.262 in
1.263 fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) =
1.264 - let val def_name = if Name<>fid then
1.265 - raise TFL_ERR{func = "wfrec_definition0",
1.266 - mesg = "Expected a definition of " ^
1.267 - quote fid ^ " but found one of " ^
1.268 - quote Name}
1.269 - else Name ^ "_def"
1.270 - val wfrec_R_M = map_term_types poly_tvars
1.271 - (wfrec $ map_term_types poly_tvars R)
1.272 - $ functional
1.273 + let val def_name = if Name<>fid then
1.274 + raise TFL_ERR{func = "wfrec_definition0",
1.275 + mesg = "Expected a definition of " ^
1.276 + quote fid ^ " but found one of " ^
1.277 + quote Name}
1.278 + else Name ^ "_def"
1.279 + val wfrec_R_M = map_term_types poly_tvars
1.280 + (wfrec $ map_term_types poly_tvars R)
1.281 + $ functional
1.282 val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
1.283 in #1 (PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy) end
1.284 end;
1.285 @@ -391,7 +391,7 @@
1.286 * This structure keeps track of congruence rules that aren't derived
1.287 * from a datatype definition.
1.288 *---------------------------------------------------------------------------*)
1.289 -fun extraction_thms thy =
1.290 +fun extraction_thms thy =
1.291 let val {case_rewrites,case_congs} = Thry.extract_info thy
1.292 in (case_rewrites, case_congs)
1.293 end;
1.294 @@ -400,20 +400,20 @@
1.295 (*---------------------------------------------------------------------------
1.296 * Pair patterns with termination conditions. The full list of patterns for
1.297 * a definition is merged with the TCs arising from the user-given clauses.
1.298 - * There can be fewer clauses than the full list, if the user omitted some
1.299 + * There can be fewer clauses than the full list, if the user omitted some
1.300 * cases. This routine is used to prepare input for mk_induction.
1.301 *---------------------------------------------------------------------------*)
1.302 fun merge full_pats TCs =
1.303 let fun insert (p,TCs) =
1.304 - let fun insrt ((x as (h,[]))::rst) =
1.305 + let fun insrt ((x as (h,[]))::rst) =
1.306 if (p aconv h) then (p,TCs)::rst else x::insrt rst
1.307 | insrt (x::rst) = x::insrt rst
1.308 | insrt[] = raise TFL_ERR{func="merge.insert",
1.309 - mesg="pattern not found"}
1.310 + mesg="pattern not found"}
1.311 in insrt end
1.312 fun pass ([],ptcl_final) = ptcl_final
1.313 | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
1.314 -in
1.315 +in
1.316 pass (TCs, map (fn p => (p,[])) full_pats)
1.317 end;
1.318
1.319 @@ -422,7 +422,7 @@
1.320
1.321 (*called only by Tfl.simplify_defn*)
1.322 fun post_definition meta_tflCongs (theory, (def, pats)) =
1.323 - let val tych = Thry.typecheck theory
1.324 + let val tych = Thry.typecheck theory
1.325 val f = #lhs(S.dest_eq(concl def))
1.326 val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
1.327 val pats' = filter given pats
1.328 @@ -431,12 +431,12 @@
1.329 val WFR = #ant(S.dest_imp(concl corollary))
1.330 val R = #Rand(S.dest_comb WFR)
1.331 val corollary' = R.UNDISCH corollary (* put WF R on assums *)
1.332 - val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
1.333 - given_pats
1.334 + val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
1.335 + given_pats
1.336 val (case_rewrites,context_congs) = extraction_thms theory
1.337 val corollaries' = map(rewrite_rule case_rewrites) corollaries
1.338 - val extract = R.CONTEXT_REWRITE_RULE
1.339 - (f, [R], cut_apply, meta_tflCongs@context_congs)
1.340 + val extract = R.CONTEXT_REWRITE_RULE
1.341 + (f, [R], cut_apply, meta_tflCongs@context_congs)
1.342 val (rules, TCs) = ListPair.unzip (map extract corollaries')
1.343 val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
1.344 val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
1.345 @@ -445,7 +445,7 @@
1.346 {theory = theory, (* holds def, if it's needed *)
1.347 rules = rules1,
1.348 rows = rows,
1.349 - full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
1.350 + full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
1.351 TCs = TCs}
1.352 end;
1.353
1.354 @@ -470,93 +470,93 @@
1.355 val given_pats = givens pats
1.356 (* val f = Free(Name,Ty) *)
1.357 val Type("fun", [f_dty, f_rty]) = Ty
1.358 - val dummy = if Name<>fid then
1.359 - raise TFL_ERR{func = "wfrec_eqns",
1.360 - mesg = "Expected a definition of " ^
1.361 - quote fid ^ " but found one of " ^
1.362 - quote Name}
1.363 - else ()
1.364 + val dummy = if Name<>fid then
1.365 + raise TFL_ERR{func = "wfrec_eqns",
1.366 + mesg = "Expected a definition of " ^
1.367 + quote fid ^ " but found one of " ^
1.368 + quote Name}
1.369 + else ()
1.370 val (case_rewrites,context_congs) = extraction_thms thy
1.371 val tych = Thry.typecheck thy
1.372 val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
1.373 val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
1.374 val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
1.375 - Rtype)
1.376 + Rtype)
1.377 val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
1.378 val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
1.379 - val dummy =
1.380 - if !trace then
1.381 - writeln ("ORIGINAL PROTO_DEF: " ^
1.382 - Sign.string_of_term (Theory.sign_of thy) proto_def)
1.383 + val dummy =
1.384 + if !trace then
1.385 + writeln ("ORIGINAL PROTO_DEF: " ^
1.386 + Sign.string_of_term (Theory.sign_of thy) proto_def)
1.387 else ()
1.388 val R1 = S.rand WFR
1.389 val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
1.390 val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
1.391 val corollaries' = map (rewrite_rule case_rewrites) corollaries
1.392 - fun extract X = R.CONTEXT_REWRITE_RULE
1.393 - (f, R1::SV, cut_apply, tflCongs@context_congs) X
1.394 + fun extract X = R.CONTEXT_REWRITE_RULE
1.395 + (f, R1::SV, cut_apply, tflCongs@context_congs) X
1.396 in {proto_def = proto_def,
1.397 SV=SV,
1.398 - WFR=WFR,
1.399 + WFR=WFR,
1.400 pats=pats,
1.401 extracta = map extract corollaries'}
1.402 end;
1.403
1.404
1.405 (*---------------------------------------------------------------------------
1.406 - * Define the constant after extracting the termination conditions. The
1.407 + * Define the constant after extracting the termination conditions. The
1.408 * wellfounded relation used in the definition is computed by using the
1.409 * choice operator on the extracted conditions (plus the condition that
1.410 * such a relation must be wellfounded).
1.411 *---------------------------------------------------------------------------*)
1.412
1.413 fun lazyR_def thy fid tflCongs eqns =
1.414 - let val {proto_def,WFR,pats,extracta,SV} =
1.415 - wfrec_eqns thy fid (congs tflCongs) eqns
1.416 + let val {proto_def,WFR,pats,extracta,SV} =
1.417 + wfrec_eqns thy fid (congs tflCongs) eqns
1.418 val R1 = S.rand WFR
1.419 val f = #lhs(S.dest_eq proto_def)
1.420 val (extractants,TCl) = ListPair.unzip extracta
1.421 - val dummy = if !trace
1.422 - then (writeln "Extractants = ";
1.423 - prths extractants;
1.424 - ())
1.425 - else ()
1.426 + val dummy = if !trace
1.427 + then (writeln "Extractants = ";
1.428 + prths extractants;
1.429 + ())
1.430 + else ()
1.431 val TCs = foldr (gen_union (op aconv)) (TCl, [])
1.432 val full_rqt = WFR::TCs
1.433 val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
1.434 val R'abs = S.rand R'
1.435 val proto_def' = subst_free[(R1,R')] proto_def
1.436 val dummy = if !trace then writeln ("proto_def' = " ^
1.437 - Sign.string_of_term
1.438 - (Theory.sign_of thy) proto_def')
1.439 - else ()
1.440 + Sign.string_of_term
1.441 + (Theory.sign_of thy) proto_def')
1.442 + else ()
1.443 val {lhs,rhs} = S.dest_eq proto_def'
1.444 val (c,args) = S.strip_comb lhs
1.445 val (Name,Ty) = dest_atom c
1.446 - val defn = mk_const_def (Theory.sign_of thy)
1.447 - (Name, Ty, S.list_mk_abs (args,rhs))
1.448 + val defn = mk_const_def (Theory.sign_of thy)
1.449 + (Name, Ty, S.list_mk_abs (args,rhs))
1.450 val (theory, [def0]) =
1.451 thy
1.452 - |> PureThy.add_defs_i
1.453 + |> PureThy.add_defs_i
1.454 [Thm.no_attributes (fid ^ "_def", defn)]
1.455 val def = freezeT def0;
1.456 val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
1.457 - else ()
1.458 + else ()
1.459 (* val fconst = #lhs(S.dest_eq(concl def)) *)
1.460 val tych = Thry.typecheck theory
1.461 val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
1.462 - (*lcp: a lot of object-logic inference to remove*)
1.463 + (*lcp: a lot of object-logic inference to remove*)
1.464 val baz = R.DISCH_ALL
1.465 - (U.itlist R.DISCH full_rqt_prop
1.466 - (R.LIST_CONJ extractants))
1.467 + (U.itlist R.DISCH full_rqt_prop
1.468 + (R.LIST_CONJ extractants))
1.469 val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
1.470 - else ()
1.471 + else ()
1.472 val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
1.473 val SV' = map tych SV;
1.474 val SVrefls = map reflexive SV'
1.475 val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x))
1.476 - SVrefls def)
1.477 - RS meta_eq_to_obj_eq
1.478 + SVrefls def)
1.479 + RS meta_eq_to_obj_eq
1.480 val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
1.481 val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
1.482 val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
1.483 @@ -581,10 +581,10 @@
1.484 * [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n]
1.485 * -----------------------------------------------------------
1.486 * ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
1.487 - * ...
1.488 + * ...
1.489 * (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
1.490 *
1.491 - * This function is totally ad hoc. Used in the production of the induction
1.492 + * This function is totally ad hoc. Used in the production of the induction
1.493 * theorem. The nchotomy theorem can have clauses that look like
1.494 *
1.495 * ?v1..vn. z = C vn..v1
1.496 @@ -600,7 +600,7 @@
1.497 val vlist = #2(S.strip_comb (S.rhs body))
1.498 val plist = ListPair.zip (vlist, xlist)
1.499 val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
1.500 - handle OPTION => error
1.501 + handle OPTION => error
1.502 "TFL fault [alpha_ex_unroll]: no correspondence"
1.503 fun build ex [] = []
1.504 | build (_$rex) (v::rst) =
1.505 @@ -608,7 +608,7 @@
1.506 in ex1 :: build ex1 rst
1.507 end
1.508 val (nex::exl) = rev (tm::build tm args)
1.509 - in
1.510 + in
1.511 (nex, ListPair.zip (args, rev exl))
1.512 end;
1.513
1.514 @@ -621,19 +621,19 @@
1.515 *---------------------------------------------------------------------------*)
1.516
1.517 fun mk_case ty_info usednames thy =
1.518 - let
1.519 + let
1.520 val divide = ipartition (gvvariant usednames)
1.521 val tych = Thry.typecheck thy
1.522 fun tych_binding(x,y) = (tych x, tych y)
1.523 fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
1.524 fun mk{rows=[],...} = fail"no rows"
1.525 - | mk{path=[], rows = [([], (thm, bindings))]} =
1.526 + | mk{path=[], rows = [([], (thm, bindings))]} =
1.527 R.IT_EXISTS (map tych_binding bindings) thm
1.528 | mk{path = u::rstp, rows as (p::_, _)::_} =
1.529 let val (pat_rectangle,rights) = ListPair.unzip rows
1.530 val col0 = map hd pat_rectangle
1.531 val pat_rectangle' = map tl pat_rectangle
1.532 - in
1.533 + in
1.534 if (forall is_Free col0) (* column 0 is all variables *)
1.535 then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
1.536 (ListPair.zip (rights, col0))
1.537 @@ -655,17 +655,17 @@
1.538 val constraints = map #1 existentials
1.539 val vexl = map #2 existentials
1.540 fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
1.541 - val news = map (fn (nf,rows,c) => {path = nf@rstp,
1.542 + val news = map (fn (nf,rows,c) => {path = nf@rstp,
1.543 rows = map (expnd c) rows})
1.544 (U.zip3 new_formals groups constraints)
1.545 val recursive_thms = map mk news
1.546 val build_exists = foldr
1.547 - (fn((x,t), th) =>
1.548 + (fn((x,t), th) =>
1.549 R.CHOOSE (tych x, R.ASSUME (tych t)) th)
1.550 val thms' = ListPair.map build_exists (vexl, recursive_thms)
1.551 val same_concls = R.EVEN_ORS thms'
1.552 in R.DISJ_CASESL thm' same_concls
1.553 - end
1.554 + end
1.555 end end
1.556 in mk
1.557 end;
1.558 @@ -687,11 +687,11 @@
1.559 val th0 = R.ASSUME (tych a_eq_v)
1.560 val rows = map (fn x => ([x], (th0,[]))) pats
1.561 in
1.562 - R.GEN (tych a)
1.563 + R.GEN (tych a)
1.564 (R.RIGHT_ASSOC
1.565 (R.CHOOSE(tych v, ex_th0)
1.566 (mk_case ty_info (vname::aname::names)
1.567 - thy {path=[v], rows=rows})))
1.568 + thy {path=[v], rows=rows})))
1.569 end end;
1.570
1.571
1.572 @@ -708,16 +708,16 @@
1.573 local infix 5 ==>
1.574 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
1.575 in
1.576 -fun build_ih f P (pat,TCs) =
1.577 +fun build_ih f P (pat,TCs) =
1.578 let val globals = S.free_vars_lr pat
1.579 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
1.580 - fun dest_TC tm =
1.581 + fun dest_TC tm =
1.582 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
1.583 val (R,y,_) = S.dest_relation R_y_pat
1.584 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
1.585 - in case cntxt
1.586 + in case cntxt
1.587 of [] => (P_y, (tm,[]))
1.588 - | _ => let
1.589 + | _ => let
1.590 val imp = S.list_mk_conj cntxt ==> P_y
1.591 val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
1.592 val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
1.593 @@ -736,17 +736,17 @@
1.594 local infix 5 ==>
1.595 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
1.596 in
1.597 -fun build_ih f (P,SV) (pat,TCs) =
1.598 +fun build_ih f (P,SV) (pat,TCs) =
1.599 let val pat_vars = S.free_vars_lr pat
1.600 val globals = pat_vars@SV
1.601 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
1.602 - fun dest_TC tm =
1.603 + fun dest_TC tm =
1.604 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
1.605 val (R,y,_) = S.dest_relation R_y_pat
1.606 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
1.607 - in case cntxt
1.608 + in case cntxt
1.609 of [] => (P_y, (tm,[]))
1.610 - | _ => let
1.611 + | _ => let
1.612 val imp = S.list_mk_conj cntxt ==> P_y
1.613 val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
1.614 val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
1.615 @@ -762,9 +762,9 @@
1.616 end;
1.617
1.618 (*---------------------------------------------------------------------------
1.619 - * This function makes good on the promise made in "build_ih".
1.620 + * This function makes good on the promise made in "build_ih".
1.621 *
1.622 - * Input is tm = "(!y. R y pat ==> P y) ==> P pat",
1.623 + * Input is tm = "(!y. R y pat ==> P y) ==> P pat",
1.624 * TCs = TC_1[pat] ... TC_n[pat]
1.625 * thm = ih1 /\ ... /\ ih_n |- ih[pat]
1.626 *---------------------------------------------------------------------------*)
1.627 @@ -776,17 +776,17 @@
1.628 fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
1.629 fun mk_ih ((TC,locals),th2,nested) =
1.630 R.GENL (map tych locals)
1.631 - (if nested
1.632 + (if nested
1.633 then R.DISCH (get_cntxt TC) th2 handle _ => th2
1.634 - else if S.is_imp(concl TC)
1.635 - then R.IMP_TRANS TC th2
1.636 + else if S.is_imp(concl TC)
1.637 + then R.IMP_TRANS TC th2
1.638 else R.MP th2 TC)
1.639 - in
1.640 + in
1.641 R.DISCH antc
1.642 (if S.is_imp(concl thm') (* recursive calls in this clause *)
1.643 then let val th1 = R.ASSUME antc
1.644 val TCs = map #1 TCs_locals
1.645 - val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
1.646 + val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
1.647 #2 o S.strip_forall) TCs
1.648 val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
1.649 TCs_locals
1.650 @@ -806,8 +806,8 @@
1.651 * ?v1 ... vn. x = (v1,...,vn) |- M[x]
1.652 *
1.653 *---------------------------------------------------------------------------*)
1.654 -fun LEFT_ABS_VSTRUCT tych thm =
1.655 - let fun CHOOSER v (tm,thm) =
1.656 +fun LEFT_ABS_VSTRUCT tych thm =
1.657 + let fun CHOOSER v (tm,thm) =
1.658 let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
1.659 in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
1.660 end
1.661 @@ -821,7 +821,7 @@
1.662 * Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)]
1.663 *
1.664 * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
1.665 - * recursion induction (Rinduct) by proving the antecedent of Sinduct from
1.666 + * recursion induction (Rinduct) by proving the antecedent of Sinduct from
1.667 * the antecedent of Rinduct.
1.668 *---------------------------------------------------------------------------*)
1.669 fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
1.670 @@ -830,8 +830,8 @@
1.671 val (pats,TCsl) = ListPair.unzip pat_TCs_list
1.672 val case_thm = complete_cases thy pats
1.673 val domain = (type_of o hd) pats
1.674 - val Pname = Term.variant (foldr (foldr add_term_names)
1.675 - (pats::TCsl, [])) "P"
1.676 + val Pname = Term.variant (foldr (foldr add_term_names)
1.677 + (pats::TCsl, [])) "P"
1.678 val P = Free(Pname, domain --> HOLogic.boolT)
1.679 val Sinduct = R.SPEC (tych P) Sinduction
1.680 val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
1.681 @@ -842,11 +842,11 @@
1.682 val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
1.683 val proved_cases = map (prove_case fconst thy) tasks
1.684 val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
1.685 - "v",
1.686 - domain)
1.687 + "v",
1.688 + domain)
1.689 val vtyped = tych v
1.690 val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
1.691 - val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')
1.692 + val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')
1.693 (substs, proved_cases)
1.694 val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
1.695 val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
1.696 @@ -855,7 +855,7 @@
1.697 val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
1.698 val dc' = U.itlist (R.GEN o tych) vars
1.699 (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
1.700 -in
1.701 +in
1.702 R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
1.703 end
1.704 handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"};
1.705 @@ -864,23 +864,23 @@
1.706
1.707
1.708 (*---------------------------------------------------------------------------
1.709 - *
1.710 + *
1.711 * POST PROCESSING
1.712 *
1.713 *---------------------------------------------------------------------------*)
1.714
1.715
1.716 -fun simplify_induction thy hth ind =
1.717 +fun simplify_induction thy hth ind =
1.718 let val tych = Thry.typecheck thy
1.719 val (asl,_) = R.dest_thm ind
1.720 val (_,tc_eq_tc') = R.dest_thm hth
1.721 val tc = S.lhs tc_eq_tc'
1.722 fun loop [] = ind
1.723 - | loop (asm::rst) =
1.724 + | loop (asm::rst) =
1.725 if (U.can (Thry.match_term thy asm) tc)
1.726 then R.UNDISCH
1.727 (R.MATCH_MP
1.728 - (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
1.729 + (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
1.730 hth)
1.731 else loop rst
1.732 in loop asl
1.733 @@ -888,10 +888,10 @@
1.734
1.735
1.736 (*---------------------------------------------------------------------------
1.737 - * The termination condition is an antecedent to the rule, and an
1.738 + * The termination condition is an antecedent to the rule, and an
1.739 * assumption to the theorem.
1.740 *---------------------------------------------------------------------------*)
1.741 -fun elim_tc tcthm (rule,induction) =
1.742 +fun elim_tc tcthm (rule,induction) =
1.743 (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
1.744
1.745
1.746 @@ -901,10 +901,10 @@
1.747 (*---------------------------------------------------------------------
1.748 * Attempt to eliminate WF condition. It's the only assumption of rules
1.749 *---------------------------------------------------------------------*)
1.750 - val (rules1,induction1) =
1.751 - let val thm = R.prove(tych(HOLogic.mk_Trueprop
1.752 - (hd(#1(R.dest_thm rules)))),
1.753 - WFtac)
1.754 + val (rules1,induction1) =
1.755 + let val thm = R.prove(tych(HOLogic.mk_Trueprop
1.756 + (hd(#1(R.dest_thm rules)))),
1.757 + WFtac)
1.758 in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction)
1.759 end handle _ => (rules,induction)
1.760
1.761 @@ -917,11 +917,11 @@
1.762 * 3. replace tc by tc' in both the rules and the induction theorem.
1.763 *---------------------------------------------------------------------*)
1.764
1.765 - fun print_thms s L =
1.766 + fun print_thms s L =
1.767 if !trace then writeln (cat_lines (s :: map string_of_thm L))
1.768 else ();
1.769
1.770 - fun print_cterms s L =
1.771 + fun print_cterms s L =
1.772 if !trace then writeln (cat_lines (s :: map string_of_cterm L))
1.773 else ();;
1.774
1.775 @@ -930,25 +930,25 @@
1.776 val _ = print_cterms "TC before simplification: " [tc1]
1.777 val tc_eq = simplifier tc1
1.778 val _ = print_thms "result: " [tc_eq]
1.779 - in
1.780 + in
1.781 elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
1.782 - handle _ =>
1.783 + handle _ =>
1.784 (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
1.785 - (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
1.786 - terminator)))
1.787 + (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
1.788 + terminator)))
1.789 (r,ind)
1.790 - handle _ =>
1.791 - (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
1.792 + handle _ =>
1.793 + (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
1.794 simplify_induction theory tc_eq ind))
1.795 end
1.796
1.797 (*----------------------------------------------------------------------
1.798 * Nested termination conditions are harder to get at, since they are
1.799 - * left embedded in the body of the function (and in induction
1.800 - * theorem hypotheses). Our "solution" is to simplify them, and try to
1.801 - * prove termination, but leave the application of the resulting theorem
1.802 - * to a higher level. So things go much as in "simplify_tc": the
1.803 - * termination condition (tc) is simplified to |- tc = tc' (there might
1.804 + * left embedded in the body of the function (and in induction
1.805 + * theorem hypotheses). Our "solution" is to simplify them, and try to
1.806 + * prove termination, but leave the application of the resulting theorem
1.807 + * to a higher level. So things go much as in "simplify_tc": the
1.808 + * termination condition (tc) is simplified to |- tc = tc' (there might
1.809 * not be a change) and then 2 attempts are made:
1.810 *
1.811 * 1. if |- tc = T, then return |- tc; otherwise,
1.812 @@ -963,12 +963,12 @@
1.813 handle _
1.814 => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
1.815 (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
1.816 - terminator))
1.817 + terminator))
1.818 handle _ => tc_eq))
1.819 end
1.820
1.821 (*-------------------------------------------------------------------
1.822 - * Attempt to simplify the termination conditions in each rule and
1.823 + * Attempt to simplify the termination conditions in each rule and
1.824 * in the induction theorem.
1.825 *-------------------------------------------------------------------*)
1.826 fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm