#
5417af9d |
|
31-Mar-2020 |
Arve Gengelbach <arve.gengelbach@it.uu.se> |
remove lcsymtacs (github issue #666) The lcsymtacs structure is regarded superseded as it plainly is a shorthand for opening the following modules: Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib Rewrite bossLib Thm_cont
|
#
698d4c1b |
|
04-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/lambda/barendregt for tight equality
|
#
bc294d17 |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extract a usable half-way point from nominal_datatype branch. This replaces the is_perm predicate with a type embodying that predicate. It doesn't include the subsequent work on allowing multiple 'atom' types.
|
#
ba932e5d |
|
05-Jun-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rework lambda-theory scripts to use new varying parameter recursion theorem. Also make work for myself by having some of the script files use 'tight' equality. Later files get switched back to loose (prec = 100) equality, because it was all getting to be too much work.
|
#
89e4f0f9 |
|
13-Apr-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Prove some useful theorems about having weak-head normal forms.
|
#
edb14cee |
|
27-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Some additional rewrites of "general utility".
|
#
fcc09cc8 |
|
26-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Weak-head reduction (like all the others) can't create new free variables. Also add the substitutivity result for w.h. as a congruence rule.
|
#
d8319d52 |
|
26-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Prove some theorems about normal order reduction to weak-head normal forms (abstractions, or variables in the head position of a series of applications). Basically, if something can normal reduce to such a thing, then it can weak-head reduce to something that shares the key aspects of the shape. Either, it can weak-head reduce to an abstraction, or it can weak-head reduce to a series of applications, where the head is the variable that is in that position at the end of the normal order reduction. Along the way, invent a notation for FOLDL (@@) t ts where t is a term, and ts a list of terms. The notation is (t @* ts) in ASCII. This is a "series of applications" with t in the head position. Prove a bunch of theorems about these forms. All this stuff goes into basics/appFOLDLTheory.
|
#
1739d35f |
|
21-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove a redundant abbreviation tactic in the proof that weak head reduction is substitutive (i.e., if you have a w.h. reduction from M to N, then you will also have one from [P/v]M to [P/v]N).
|
#
e4599942 |
|
21-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More support for weak head reduction, including a simpset for rewriting with it.
|
#
5b53e531 |
|
17-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Introduce weak-head reduction very sketchily in order to show that there's a sort-of congruence rule with it and normal order reduction. Unfortunately, you don't have M1 -n->* M2 ==> M1 @@ N -n->* M2 @@ N because the reductions undergone by M1 might produce an abstraction, in which case the M1 reductions have to stop for the higher level redex to be reduced. But weak head reduction will never happen at all once an abstraction is produced so all is well.
|
#
4004ae0a |
|
24-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Eliminate the head_reduce1 constant from standardisation and replace it everywhere with head_reduction$hreduce1, written infix -h->. Also, prove a couple of easy lemmas in head_reduction: - that hreduce1 is deterministic/unique - that if M beta-reduces to N, and M is hnf, then so too is N (i.e., the reduction happened at an "internal" redex).
|
#
497555c3 |
|
24-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Start to move stuff relating to head-reduction into a separate theory. There's still a pile of stuff, mainly expressed in terms of reduction paths, in standardisationTheory that could probably be moved or re-expressed. In particular, there is a head_reduce1 constant there that is actually the same as -h-> from head_reductionTheory.
|