On Wed, Jun 6, 2012 at 6:33 PM, Ramana Kumar <[email protected]> wrote:
> > Cv1_Axiom;
> val it =
> |- ∀f0 f1 f2 f3 f4 f5 f6 f7.
> ∃fn0 fn1 fn2.
> (∀l. fn0 (CLitv l) = f0 l) ∧
> (∀m vs. fn0 (CConv m vs) = f1 m vs (fn1 vs)) ∧
> (∀env xs b. fn0 (CClosure env xs b) = f2 env xs b (fn2 env)) ∧
> (∀env ns defs d.
> fn0 (CRecClos env ns defs d) = f3 env ns defs d (fn2 env)) ∧
> (fn1 [] = f4) ∧ (∀v vs. fn1 (v::vs) = f5 v vs (fn0 v) (fn1 vs)) ∧
> ∀env. fn2 env = f6 env (f7 o_f env):
> thm
>
Sorry. That axiom is wrong. It should look like this:
|- ∀f0 f1 f2 f3 f4 f5 f6.
∃fn0 fn1 fn2.
(∀l. fn0 (CLitv l) = f0 l) ∧
(∀m vs. fn0 (CConv m vs) = f1 m vs (fn1 vs)) ∧
(∀env xs b. fn0 (CClosure env xs b) = f2 env xs b (fn2 env)) ∧
(∀env ns defs d.
fn0 (CRecClos env ns defs d) =
f3 env ns defs d (fn2 env)) ∧ (fn1 [] = f4) ∧
(∀v vs. fn1 (v::vs) = f5 v vs (fn0 v) (fn1 vs)) ∧
∀env. fn2 env = f6 env (fn0 o_f env)
build_tyinfos still can't deal with it though.
Probably because to define the size constant manually I also had to define
a size constant for finite maps, which I don't think exists in the standard
library yet.
(Amongst other things.)
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
