Hi Haitao,
I’m glad you figured out sg and metis_tac as a solution to this, but of course,
you’re right that this can be tedious. One of the most precise way of attacking
this is to use a tactic like drule, and to select assumptions with the various
_assum combinators (first_assum, last_assum,
Call for Extended Abstracts & Demonstrations
**
ThEdu'19
Theorem proving components for Educational software
25 or 26 August 2019
Hi,
I just started HOL and am really enjoying it quite a bit. One difficulty I
find during interactive tactic proof sessions is to get hold of and
manipulate assumptions. Right now I find myself using sg to write new
subgoals and then metis_tac[] to prove the baby steps that could be easily
VerifyThis Verification Competition 2019
CALL FOR PARTICIPATION -- TRAVEL GRANTS
Competition to be held at ETAPS 2019
http://verifythis.ethz.ch
First Call for Papers
SYNASC 2019
21th International Symposium on
Symbolic and Numeric Algorithms for Scientific Computing
September 4-7, 2019, Timisoara, Romania
I think that the set type here is irrelevant. You have a relation for sorting
elements in the range of f. Construct the list of applications of f to
0..(n-1), sort that using the sort operation from sortingTheory, and make g
from the list index operator applied to that.
Cheers,
Thomas.
Hi,
suppose I have a finite sequence of n disjoint sets, given by a function (f
:num -> ‘a -> bool), and their union is BIGUNION (IMAGE f (count n)), and an
order R (antisymmetric
, transitive) on these sets.
Is it possible to assert the existence of another function (g :num -> ‘a ->
bool)
Hi Michael,
thanks for the explanation in details! Now I finally understand why the
two versions of `sup` can be proved equivalent, while the two "inf"
cannot. Any way, I'll follow your idea and submit a fix of the
duplicated definitions of `inf` soon.
--Chun
Il 23/02/19 07:00,
