From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2003 14:44:51 +0000 (+0000) Subject: First commit of the NuPRL stylesheets. X-Git-Tag: before_refactoring~28 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=734a6fc5d8da4896c646d1dd7a17afaf0dd33224;p=helm.git First commit of the NuPRL stylesheets. --- diff --git a/helm/nuprl_stylesheets/nuprl_abstract.xsl b/helm/nuprl_stylesheets/nuprl_abstract.xsl new file mode 100644 index 000000000..fa6d8154d --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_abstract.xsl @@ -0,0 +1,170 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + forall + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + so_lambda + + + + so_variable + + + + + + + + + + + + + + + + + + so_apply + + + + + + + + gcd_p + + + + + + + decidable + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_annotatedpres.xsl b/helm/nuprl_stylesheets/nuprl_annotatedpres.xsl new file mode 100644 index 000000000..f97a08be6 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_annotatedpres.xsl @@ -0,0 +1,61 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html.xsl new file mode 100644 index 000000000..a2dbe9c03 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_content_to_html.xsl @@ -0,0 +1,2807 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Ax + + + + + Void + + + + + + + + " + ∀ + ??? + + + + + + l + λ + ??? + + + + + + Õ + Π + ??? + + + + + + ® + → + ??? + + + + + + Þ + ⇒ + ??? + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + <xsl:value-of select="$CICURI"/> + + + + + + if(document.getElementById) + for(var i=0;i<document.to_be_deleted.length;i++) + Hide(document.getElementById(document.to_be_deleted[i])); + + + + + + + + + + + + + + + + + + + + + + + + +   + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + "" + + + : + + + ( + + + + ) + + + + + + + + + + + + + + + + + + : + + ( + + + + ) + + . + + + ) + + + + + + + + : + + + x + + + + + + + + + x + + + + + + + + < + + + , + + + > + + + + + + + + + + + + + + + + + inl ( + + + + ) + + + + + + + inr ( + + + + ) + + + + + + + + = + + + + + + + + + + + + + + + + + + + + :: + + + + + + + + + rectype + + + + = + + + + + + + + + + { + + + + + + : + + + + + + + + + | + + + + + + + + + + + + + + + : + + + + . + + + + + + + + + , + + + : + + + + // + + + + + + + ( + + + + + + + + ) + + + + + ( + + +   + + + ) + + + + ( + + :> + + ) + + + Prop + + + Set + + + Type + + + + + < + + > + CASE + + OF + + + + + | + + + + + + + + + + + + + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + +  proves  + + + + letin1 (inline error) + + + + + Contradiction. + + + + From  + +  we get + ( + + )  + +  and  + ( + + )  + + ; +  hence  + + + + + + + + + + + + + + + + + : + + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + : + + ( + + + + +
+ + + + + + + + + + + + + ( + + + + + + + + + + + + : + + + + ( + + + + ) + + +
+ + + + + + + + + + + + + + + + + : + + + +
+ + + + . + + + + + + + + + + + + + + + + + + + + + : + + +
+ + + + . + + + + + + + + + + + + + + + + + + + + + +
+ + + + . + + + + + + + + + + + + + + + + < + + + + + , +
+ + + + + + > + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + + + + inl ( + + + + +
+ + + + + ) + + + + + + + + + + + + + + inr ( + + + + +
+ + + + + ) + + + + + + + + + + + + P + + + + + + + + + + U + + + + + + + + + + + + + = + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + + " + + + + " + + + + + + + + [] + + + + + + + + +
+ + + + + :: + + + + + + + + + + rectype + + + + +
+ + + + + = + + + + + + + + + { + + + + + + : + + + + +
+ + + + + + + + + +
+ + + + + + + | + + + + + + + + + + + + + + + : + + + + +
+ + + + + . + + + + + + + + + , + + + : + + + + +
+ + + + + // + + + + + + + + + + + atom_eq ( + + + + + int_eq ( + + + + + less ( + + + + + ; + + ; + + ; + + + ) + + + + + + + + + + + spread ( + + + ; + + , + + . + + + ) + + + + + + decide ( + + + ; + + . + + ; + + . + + + ) + + + + + any ( + + + + ) + + + + + + + + + so_ + + + + + + + + + + ( + + + , + + + ) + + + + . + + + + + + + + + + so_apply + ( + + + + + + ) + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + ) + + + + + + + + + + + + ( + + + + +
+ + + + + + + + ) + + + + + + + + + + + + + ( + + +
+ + + :> + + + + ) + + + + + + + + + + + + + + + Prop + + + Set + + + Type + + + + + < + + + + > +
+ + + CASE + + + + OF + + +
+ + + + + +    + + + | + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + FIX + + { + +
+ + + + + : + + + +
+ + + + := + + + + +
+ + + + } + + + + + + + + + + + COFIX + + { +
+ + + + + + : + + + +
+ + + + := + + + + + +
+ + + + } + + + + + + + + let  + +  :=  + + + +
+ + + + in  + + + + + + + + + + + + + + + + + + +   + + + +
+ + + + we proved  + + + + + + + + + + + + + + + + + + + + +   + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + +  = + + + =  + + + + + + +
+ + + + + + + + + + + + We have the following chain of disequalities: + + +
+ + + + + + + + +   + + + + +   + + + + + + +
+ + + + + + + + + + + + + + +
+ + + + + + + + + + + + + +
+ + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + Consider  + + + + + + + + + + + + + + + + + + +
+ + + + Rewrite  + +   + +
+ + + + + with  + +   + +
+ + + + + by  + + + + + + + + + +
+ + + + Then apply it to  + + + + + We prove  + + + +
+ + + + by induction on  + + + + + + + + + + + +
+ + + + Case  + + + + +
+ + + + By induction hypothesis, we have: + +
+ + + + ( + + )  + + + + + +
+ + + + + + + + + + + + + + + + ( + + +   + + : + + + ) + + + + + + + + +
+ + + + Contradiction. + + + + + + + + + + + Consider  + + + +
+ + + + In particular, we have +
+ + + + ( + + )  + + + +
+ + + + ( + + )  + + + +
+ + + + + + + + + + + + + + + + + Consider  + + + +
+ + + + We proceed by cases to prove  + +
+ + + + Left: suppose  + ( + + )  + +
+ + + + + + +
+ + + + Right: suppose  + ( + + )  + +
+ + + + + + + + + + + + + + + + + Consider  + + + +
+ + + + We prove  + +  by cases: +
+ + + + Left:  + + + +
+ + + + Right:  + + + + + + + + + + + + + + Consider  + + + + + +
+ + + + Let  + + : + +  such that +
+ + + + ( + + ) + + + +
+ + + + + + + + + + + + + [ + + + + + + + + + + + + + + + + + + + + + ] + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + + + + + + + + + | + + + | + + + + + + | + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + ] + + + + + + + + + + + + + + + + + + + + + + + + + : + + +
+ + + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+Rule: +
+ + + + + + + + + + ( + + + + + level-exp( + + ) + + + + + + + + + + , + + + + ) + + + +

+ + + + + + +

+Sequent () : +
+ + + + + ) + + ( + + + + + + + + + + + ) + + + +
+ +===================================== +
+ + + + +

+ + + + + + + +

+Node:
+ + + + + +

+ + + + + + + +

+DEFINITION ()
+TYPE =
+ + + + + +
+BODY =
+ + + + + + +

+ + + + + + +

+AXIOM ()
+TYPE =
+ + + + + + +

+ + + + + + +

+UNFINISHED PROOF ()
+THESIS: + +
+CONJECTURES: + +
+ + + + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ :? _ + + + + |- : + + + + +
+PROOF: + + + +

+ + + + + + +

+ + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + () + [ + + + + : + + + + ]
+ OF ARITY + + +
+ BUILT FROM: + +
+ + + + + +    + + + | + + + + : + + + + + +

+ + + + + + +

+VARIABLE
+TYPE = + + + +
+BODY = + + + +

+ + + + + + + + + + +

BEGIN OF SECTION

+ +

END OF SECTION

+ + + diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl new file mode 100644 index 000000000..d45eb8b00 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl @@ -0,0 +1,3042 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + " + ∀ + ??? + + + + + + l + λ + ??? + + + + + + Õ + Π + ??? + + + + + + ® + → + ??? + + + + + + Þ + ⇒ + ??? + + + + + + S + Σ + ??? + + + + + + Î + ∈ + ??? + + + + + + Ç + ∩ + ??? + + + + + + I + Ι + ??? + + + + + + N + Ν + ??? + + + + + + î + ⇒ + ??? + + + + + + $ + ∃ + ??? + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + <xsl:value-of select="$CICURI"/> + + + + + + if(document.getElementById) + for(var i=0;i<document.to_be_deleted.length;i++) + Hide(document.getElementById(document.to_be_deleted[i])); + + + + + + + + + + + + + + + + + + + + + + + + +   + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + "" + + : + + + + . + + + + + + ( + + + + + + + + ) + + + + + + + + + + + + : + + + + . + + + + + + + + + + + + + : + + . + + + + + + + ( + + + + x + + + + ) + + + + + + + + < + + + , + + + > + + + + + + + + + + + + + + + + + inl ( + + + + ) + + + + + + + inr ( + + + + ) + + + + + + + + = + + + + + + + + + + + + + + + + + + + :: + + + + + + + + + rectype + + + + = + + + + + + + + + + { + + + + + + : + + + + + + + + + | + + + + } + + + + + + + + + + + + + + + : + + + + . + + + + + + + + + , + + + : + + + + // + + + + + + + + + + + + + . + + + + + + + + ( + + +   + + + ) + + + + + + + ( + + + + , + + + ) + + + + + + ( + + :> + + ) + + + Prop + + + Set + + + Type + + + + + < + + > + CASE + + OF + + + + + | + + + + + + + + + + + + + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + +  proves  + + + + letin1 (inline error) + + + + + Contradiction. + + + + From  + +  we get + ( + + )  + +  and  + ( + + )  + + ; +  hence  + + + + + + + + + + + + + + + + : + + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + "" + + : + + + + + +
+ + + + . + + + + + + + + + + + + + + + arrow + ( + + + +
+ + + + + + + + + + + + + + ) + + + + + + + + + + + : + + ( + + + + ) + + + + + + + Ax + + + + + + + Void + + + + + + + Atom + + + + + + + + + + + + + + + + + + + : + + + +
+ + + + . + + + + + + + + + + + + + + + + + + + + + + + : + + +
+ + + + . + + + + + + + + + + + + + + + + ( + + + + +
+ + + + + x + + + + + + ) + + + + + + + + + + + + + + < + + + + + , +
+ + + + + + + + > + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + inl ( + + + + + + ) + + + + + + + + + + + + + + inr ( + + + + + + ) + + + + + + + + + + + + P + + + + + + + + + + + + U + + + + + + + + + + + + + +
+ + + + + = + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + + " + + + + " + + + + + + + + [] + + + + + + + + +
+ + + + + :: + + + + + + + + + + + + + + rectype + + + + +
+ + + + + = + + + + + + + + + + + + + + + + + + { + + + + + + : + + + + +
+ + + + + + + + +
+ + + + + + + | + + + + + + + } + + + + + + + + + + + + + + + + + + + + : + + + + +
+ + + + + . + + + + + + + + + + + + , + + + : + + + + +
+ + + + + // + + + + + + + + + + + + + atom_eq ( + + + + + int_eq ( + + + + + less ( + + + + + ; + + ; + + ; + + + ) + + + + + + + + + + + + + + +
+ + + + . + + + + + + + + + + + + + + + + + ( + + + + +
+ + + + + + + + ) + + + + + + + + + + + + + + + +
+ + + + + ( + +
+ + + + + + , + + + ) + + + + + + + + + + + + + + + ( + + +
+ + + + : + + + + ) + + + + + + + + + + + + + + + Prop + + + Set + + + Type + + + + + < + + + + > +
+ + + CASE + + + + OF + + +
+ + + + + +    + + + | + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + FIX + + { + +
+ + + + + : + + + +
+ + + + := + + + + +
+ + + + } + + + + + + + + + + + COFIX + + { +
+ + + + + + : + + + +
+ + + + := + + + + + +
+ + + + } + + + + + + + + let  + +  :=  + + + +
+ + + + in  + + + + + + + + + + + + + + + + + + +   + + + +
+ + + + we proved  + + + + + + + + + + + + + + + + + + + + +   + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + +  = + + + =  + + + + + + +
+ + + + + + + + + + + + We have the following chain of disequalities: + + +
+ + + + + + + + +   + + + + +   + + + + + + +
+ + + + + + + + + + + + + + +
+ + + + + + + + + + + + + +
+ + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + Consider  + + + + + + + + + + + + + + + + + + +
+ + + + Rewrite  + +   + +
+ + + + + with  + +   + +
+ + + + + by  + + + + + + + + + +
+ + + + Then apply it to  + + + + + We prove  + + + +
+ + + + by induction on  + + + + + + + + + + + +
+ + + + Case  + + + + +
+ + + + By induction hypothesis, we have: + +
+ + + + ( + + )  + + + + + +
+ + + + + + + + + + + + + + + + ( + + +   + + : + + + ) + + + + + + + + +
+ + + + Contradiction. + + + + + + + + + + + Consider  + + + +
+ + + + In particular, we have +
+ + + + ( + + )  + + + +
+ + + + ( + + )  + + + +
+ + + + + + + + + + + + + + + + + Consider  + + + +
+ + + + We proceed by cases to prove  + +
+ + + + Left: suppose  + ( + + )  + +
+ + + + + + +
+ + + + Right: suppose  + ( + + )  + +
+ + + + + + + + + + + + + + + + + Consider  + + + +
+ + + + We prove  + +  by cases: +
+ + + + Left:  + + + +
+ + + + Right:  + + + + + + + + + + + + + + Consider  + + + + + +
+ + + + Let  + + : + +  such that +
+ + + + ( + + ) + + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + : + + +
+ + + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + + , + + + ] + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + + + + ) + + + + + + + + + + : + + + . + + + + + + + + + + [ + + + , + + + ] + + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + implies + ( + + + +
+ + + + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + : + + + + + +
+ + + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ + + +Rule: + + + + + + + + + + + +
+ + + + + + + + + + + + +
+ + + + + + ( + + + + + + + + + + + level-exp( + + + + ) + + + + + + + + + + + + + + , +
+ + + + ) + + + + + + + + + + + ( + + + + + + level-exp( + + + + ) + + + + + + + + + + + + + + + , + + + + ) + + + + + +

+ + + + + + + + + +Sequent +
+
+ + + + + + + ) + + + + : + + + + + + + +
+ + + + + + |- +
+ + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + +
+
+ + + + + By + + + + + + + + Details + + + + +
+ + + + Hide details +
+ + + +
+ +

+ + + + + + + + + + Subgoal +
+ + + + + + + + Subgoals +
+ + + +
+ + + + Back +
+ + + +
+ + + + + + + + +

+DEFINITION ()
+TYPE =
+ + + + + +
+BODY =
+ + + + + + +

+ + + + + + +

+AXIOM ()
+TYPE =
+ + + + + + +

+ + + + + + +

+UNFINISHED PROOF ()
+THESIS: + +
+CONJECTURES: + +
+ + + + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ :? _ + + + + |- : + + + + +
+PROOF: + + + +

+ + + + + + +

+ + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + () + [ + + + + : + + + + ]
+ OF ARITY + + +
+ BUILT FROM: + +
+ + + + + +    + + + | + + + + : + + + + + +

+ + + + + + +

+VARIABLE
+TYPE = + + + +
+BODY = + + + +

+ + + + + + + + + + +

BEGIN OF SECTION

+ +

END OF SECTION

+ + + diff --git a/helm/nuprl_stylesheets/nuprl_expand.xsl b/helm/nuprl_stylesheets/nuprl_expand.xsl new file mode 100644 index 000000000..c31b47993 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_expand.xsl @@ -0,0 +1,108 @@ + + + + + + + + + + + + + + + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ERROR + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_html_arith.xsl b/helm/nuprl_stylesheets/nuprl_html_arith.xsl new file mode 100644 index 000000000..995a23c75 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_html_arith.xsl @@ -0,0 +1,650 @@ + + + + + + + + + + + + + + + + + + + + + + + + + £ + ≤ + ??? + + + + + + < + < + ??? + + + + + + ³ + ≥ + ??? + + + + + + > + > + ??? + + + + + + + + + + ??? + + + + + + - + - + ??? + + + + + + * + ∗ + ??? + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + leq + + + + + + ) + + + + + + ( + + + + + + + + + leq + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + lt + + + + + + ) + + + + + + ( + + + + + + + + + lt + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + geq + + + + + + ) + + + + + + ( + + + + + + + + + geq + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + gt + + + + + + ) + + + + + + ( + + + + + + + + + gt + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + plus + + + + + + ) + + + + + + ( + + + + + + + + + plus + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + minus + + + + + + ) + + + + + + ( + + + + + + + + + minus + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + times + + + + + + ) + + + + + + ( + + + + + + + + + times + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + min + + + { + + + + , +
+ + + + + + + } + + + + + + + + + + + + + min + + + { + + , + + } + + + + + + + + + + + + + + + + + + minus + + + + + + + + + + + + + + + + minus + + + + + + + + + + + + + + + + + + + + + abs + + + + + + + + + + + + + abs + + + + + + + + + + + + + abs + + + + + + + + + + + abs + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_html_basic.xsl b/helm/nuprl_stylesheets/nuprl_html_basic.xsl new file mode 100644 index 000000000..dfe3a011f --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_html_basic.xsl @@ -0,0 +1,532 @@ + + + + + + + + + + + + + + + + + + + + + + + + + Ù + ∧ + ??? + + + + + + Ú + ∨ + ??? + + + + + + Û + ⇔ + ??? + + + + + + Ø + ¬ + ??? + + + + + + = + = + ??? + + + + + + ¹ + ≠ + ??? + + + + + + $ + ∃ + ??? + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + and + + + + + + ) + + + + + + ( + + + + + + + + + and + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + or + + + + + + ) + + + + + + ( + + + + + + + + + or + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + iff + + + + + + ) + + + + + + ( + + + + + + + + + iff + + + + ) + + + + + + + + + + + + + + + + + + not + + + + + + + + + + + + + + + + not + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + eq + + + + + + ) + + + + + + ( + + + + + + + + + eq + + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + neq + + + + + + ) + + + + + + ( + + + + + + + + + neq + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + exists + + + + : + + + +
+ + + + . + + + + + + + + + + + + + + + + exists + + + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + exists + + + + : + + + +
+ + + + . + + + + + + + + + + + + + + + + exists + + + + : + + . + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_link.xsl b/helm/nuprl_stylesheets/nuprl_link.xsl new file mode 100644 index 000000000..849e06c3e --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_link.xsl @@ -0,0 +1,127 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + other + + + + + + + + + + + + + + + + + + + + + + + + cic + + + + + + + + theory + + + + + + + + + + _blank + + + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_links_library.xsl b/helm/nuprl_stylesheets/nuprl_links_library.xsl new file mode 100644 index 000000000..d023d774f --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_links_library.xsl @@ -0,0 +1,369 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + getxml?uri= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +?url= +?url= +apply?keys= +&param.naturalLanguage=&param.proofcheckerURL=&param.draw_graphURL=&param.uri_set_queueURL=&param.UNICODEvsSYMBOL=&param.annotations=&prop.doctype-public=&param.doctype-public=&param.encoding=&param.media-type=&param.keys=&param.getterURL=&param.processorURL=&param.interfaceURL=&param.topurl=&xmluri= +&prop.media-type=&prop.encoding= +&prop.media-type=&param.thmedia-type=&param.thkeys=&param.embedkeys=&param.thinterfaceURL=&param.thencoding=&prop.encoding= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + %23 + + + + + + http://mowgli.cs.unibo.it:58080/apply?keys=NT,NC2,NL&prop.doctype-public=&prop.media-type=text/html&param.doctype-public=&param.encoding=&param.media-type=text/html&param.CICURI=cic:/CICURI.con&param.naturalLanguage=yes&param.annotations=no&param.topurl=http://helm.cs.unibo.it/helm&param.UNICODEvsSYMBOL=SYMBOL&xmluri= + + + + + + + + + + + + + + + + + + + + + + + + %23 + + + + + %26param.CICURI%3D + + + + + + + + + + + + + + + + + + + + + + + %23 + + + + + + + + &param.CICURI=&param.type= + + + + + + + + + + + + + + + + + + + + + %23 + + + + d_c&param.getterURL=&param.CICURI=&xmluri= + + + + diff --git a/helm/nuprl_stylesheets/nuprl_mmlextension.xsl b/helm/nuprl_stylesheets/nuprl_mmlextension.xsl new file mode 100644 index 000000000..028579230 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_mmlextension.xsl @@ -0,0 +1,3034 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Sequent + + + + + + + + + + + + + + ) + + __ + + + : + + + + + + + + + + + + |- + + + + + + + + + + + Rule: + + + + + + NESSUNA REGOLA + + + + + + + + + + + + + + + + + + + + Sequent + + + + + + + + + + + + + + ) + + __ + + + : + + + + + + + + + + + + |- + + + + + + + + + + + Rule: + + + + + + NESSUNA REGOLA + + + + + + + + + + + + + + + Subgoal + + + Subgoals + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + DEFINITION () OF TYPE + + + + + + + __ + + + + + + + + AS + + + + + + + __ + + + + + + + + + + + + + + + + + AXIOM () OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + + + UNFINISHED PROOF () + + + + + + + THESIS: + + + + + + + __ + + + + + + + + CONJECTURES: + + + + + + + + __ + + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ + :? + _ + + + + + ; + + + |- + ? + : + + + + + + + + + PROOF: + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + _ + () + + + + + + + __ + [ + + + + + + + + + : + + + + + + + + + ] + + + + + + + ] + + + + + + + + + OF ARITY + + + + + + + __ + + + + + + + + BUILT FROM + + + + + + + + + + __ + + + | + _ + + + OF + _ + + + + + + + + + + + + + + + + + + + VARIABLE OF TYPE + + + + + + + __ + + + + + + + + + AS + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + : + + + + + + + + + + + + + + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + ⇒ + + + + + + + + + ⇒ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∀ + + + + + + + + . + + + + + + + + ∀ + + : + + . + + + + + + + + + + + + + LET + _ + + + + + + + + = + + + + + + + + IN + _ + + + + + + + + LET + _ + + = + + _ + IN + _ + + + + + + + + + + + + + Π + + + + + + + + . + + + + + + + + Π + + : + + . + + + + + + + + + + + + + + ( + + + + + + + + + → + + + + + + + + + + + + + + + + + + + + + + + + ) + + + + + + + + + ( + + + → + + + + + + + + + + + + + + + + + + ) + + + + + + + + + + + + + + : + + + + + + + + + + + + + + + + : + + + + + + + + + + + + + + Σ + + : + + + + + + + + . + + + + + + + + + Σ + + : + + . + + + + + + + + + + + + + + ( + + + + + + + + x + + ) + + + + + + + + ( + + x + + ) + + + + + + + + + + + + + < + + , + + + + + + + + > + + + + + + + + < + + , + + > + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + inl( + + ) + + + + + + inr( + + ) + + + + + Ax + + + + Void + + + + Atom + + + + + U + + + + + + + P + + + + + + + + + + + + + + + + + = + + + + + + + + ∈ + + + + + + + + + + = + + ∈ + + + + + + + + + " + + " + + + + + [] + + + + + + + + + + + + + + + :: + + + + + + + + + + :: + + + + + + + + + + + + + + + rectype + + + + + + + + = + + + + + + + + + rectype + + = + + + + + + + + + + + + + + + { + + + + : + + + + + + + + + + + + + | + + } + + + + + + + + { + + + + : + + + + + + + | + + } + + + + + + + + + + + + + + Ç + + : + + + + + + + + . + + + + + + + + + Ç + + : + + . + + + + + + + + + + + + + + + , + + : + + + + + + + + // + + + + + + + + + + , + + : + + // + + + + + + + + + + + + + + + + atom_eq ( + + + int_eq ( + + + less ( + + + + ; + + + + + + + + ; + + + + + + + + ; + + + + + + + + ) + + + + + + + + + + atom_eq ( + + + int_eq ( + + + less ( + + + + ; + + ; + + ; + + ) + + + + + + + + + + + + + λ + + + + + + + + . + + + + + + + + + λ + + . + + + + + + + + + + + + + + ( + + + + + + + + + + + ( + + + + + + + + + + + ) + + + + + + +( + + + + + _ + + + + +) + + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + + + + + + + + ( + + + + + + + + + + + + ( + + + + + + + + + + + + ) + + + + + + + ( + + + + + + _ + + + + + + ) + + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + + + + + + + + + + + + + + + < + + + > + CASES + _ + + + + + + + + + + > + CASES + _ + + + + + + + + + OF + + + + + + + + + + + | + + + | + + + _ + + + ⇒ + + + + + + + + + + |_ + ⇒ + + + + + + + + + + END + + + + + + + <> + CASES + _ + + _ + OF + + + + | + + + + ⇒ + + + _ + END + + + + + + + + + + + + FIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + FIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + + COFIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + COFIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + _ + + + (hide details) + + + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + _ + + + (hide details) + + + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We prove + _ + + + + + + + + by induction on + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Case + _ + + + + + + + + _ + + + + + + By induction hypothesis, we have: + + + + + + + _ + + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + _ + + : + + + ) + + + + + + + + + + + + + + + + + + Contradiction. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + Rewrite + _ + + _ + with + _ + + _ + by + _ + + + + + + + + + + + + + + + + + + + + + Then apply it to + _ + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + In particular, we have + + + + + + + ( + + ) + _ + + + + + + + + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + We proceed by cases to prove + _ + + + + + + + + Left: suppose + _ + ( + + ) + _ + + + + + + + + _ + + + + + + + + Right: suppose + _ + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + We prove + _ + + _ + by cases: + + + + + + + Left + + + + + + + + Right + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + We have the following equality chain: + + + + + + + + + + + + _ + = + + + = + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + We have the following disequality chain: + + + + + + + + + + + + _ + + + + + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + + [ + + + + + ← + + ] + + + + + + + + ↑ + + + + ( + + ) + + + + + + + + + ↑ + + + + + ( + + ) + + + + + + + + + + → + β + + + + + + + + + + + → + β + * + + + + + + + + + + + ⇒ + β + + + + + + + + + + + ⇒ + β + * + + + + + + + + + + + + + + + + + + + ≅ + + + + + + + + + + + + + + + ERROR + + + + + + + + + + + + + + + + + + + + + + + + λ + + + + + + + + + . + + + + + + + + λ + + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl new file mode 100644 index 000000000..343cafd63 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_proof.xsl @@ -0,0 +1,74 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_rules.xsl b/helm/nuprl_stylesheets/nuprl_rules.xsl new file mode 100644 index 000000000..6926ddeab --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_rules.xsl @@ -0,0 +1,876 @@ + + + + + level-exp + + + + + + + + + parameter-substitution-list + + + + + + + + + + tag : + + + + + + + dependent_functionFormation + + + + + + independent_functionFormation + + + + + functionEquality + + + + + + independent_functionEquality + + + + + lambdaEquality + + + + + + + lambdaFormation + + + + + + + applyEquality + + + + + + + independent_functionElimination + + + + + + + + + + dependent_functionElimination + + + + + + + + + functionEquality + + + + + functionExtensionality + + + + + + + dependent_productFormation + + + + + + independent_productFormation + + + + + productEquality + + + + + + independent_productEquality + + + + + dependent_pairEquality + + + + + + + dependent_pairFormation + + + + + + independent_pairEquality + + + + independent_pairFormation + + + + + spreadEquality + + + + + + + + + + productElimination + + + + + + spreadReduce + + + + unionFormation + + + + unionEquality + + + + + inlEquality + + + + + + + inlFormation + + + + + + + inrEquality + + + + + + + inrFormation + + + + + + + decideEquality + + + + + + + unionElimination + + + + + + + + + decideReduceLeft + + + + decideReduceRight + + + + + universeFormation + + + + + + universeEquality + + + + + cumulativity + + + + + + + equalityFormation + + + + + + equalityEquality + + + + axiomEquality + + + + + equalityElimination + + + + + + + + + hypothesisEquality + + + + + + + + + substitution + + + + + + equality + + + + voidFormation + + + + voidEquality + + + + anyEquality + + + + + voidElimination + + + + + + + + atomFormation + + + + atomEquality + + + + tokenEquality + + + + + tokenFormation + + + + + + + atom_eqEquality + + + + + + + atom_eqReduceTrue + + + + + + atom_eqReduceFalse + + + + intFormation + + + + intEquality + + + + natural_numberEquality + + + + minusEquality + + + + addEquality + + + + subtractEquality + + + + multiplyEquality + + + + divideFormation + + + + addEquality + + + + subtractEquality + + + + multiplyEquality + + + + divideEquality + + + + remainderBounds1 + + + + remainderBounds2 + + + + remainderBounds3 + + + + remainderBounds4 + + + + divideRemainderSum + + + + + arith + + + + + + + indEquality + + + + + + + intElimination + + + + + + + + + indReduceDown + + + + indReduceUp + + + + indReduceBase + + + + ind_eqEquality + + + + ind_eqReduceTrue + + + + ind_eqReduceFalse + + + + lessEquality + + + + lessReduceTrue + + + + lessReduceFalse + + + + less_thanEquality + + + + less_thanFormation + + + + less_thanMember + + + + listFormation + + + + listEquality + + + + + nilEquality + + + + + + + nilFormation + + + + + + consFormation + + + + consEquality + + + + + list_indEquality + + + + + + + listElimination + + + + + + + + + list_indReduceUp + + + + list_indReduceBase + + + + + recEquality + + + + + + + rec_memberEquality + + + + + + + rec_memberFormation + + + + + + + rec_indEquality + + + + + + + recElimination + + + + + + + + + + recUnrollElimination + + + + + + + + + + dependent_setFormation + + + + + + independent_setFormation + + + + + setEquality + + + + + + + dependent_set_memberEquality + + + + + + + dependent_set_memberFormation + + + + + + independent_set_memberEquality + + + + + independent_set_memberFormation + + + + + + + setElimination + + + + + + + + + + isectFormation + + + + + + + isectEquality + + + + + + + isect_memberEquality + + + + + + + isect_memberFormation + + + + + + + isect_member_caseEquality + + + + + + + isectElimination + + + + + + + + + + quotientFormation + + + + + + + quotientWeakEquality + + + + + + quotientEquality + + + + + quotient_memberWeakEquality + + + + + + + quotient_memberFormation + + + + + + + quotient_memberEquality + + + + + + + quotient_equalityElimination + + + + + + + + + + quotientElimination + + + + + + + + + + quotientElimination_2 + + + + + + + + + + direct_computation + + + + + + + reverse_direct_computation + + + + + + + direct_computation_hypothesis + + + + + + + + + + reverse_direct_computation_hypothesis + + + + + + + + + + hypothesis + + + + + + + + + thin + + + + + + + + + cut + + + + + + + + + + hyp_replacement + + + + + + + + + + lemma + + + + + + + + + extract + + + + + + + + + instantiate + + + + + + because + + + + + rename + + + + + + + introducition + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_term.xsl b/helm/nuprl_stylesheets/nuprl_term.xsl new file mode 100644 index 000000000..1bd02c93e --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_term.xsl @@ -0,0 +1,598 @@ + + + + + + + + + + + + + + + + + + + + + arrow + + + + + + + prod + + + + + + + + + + + + + + + + arrow + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + product_ind + + + + + + product + + + + + + + + + + + + + product_ind + + + + + + + + + + + + + pair + + + + + + + + + mutcase + NONE + + + + + + pair + + + + + + + + + + + + union + + + + + + + + + inl + + + + + + + + inr + + + + + + + + mutcase + NONE + + + + + + inl + + + + + + + inr + + + + + + + + + + + universe + + + + + + + + + + equal + + + + + + + + + + Ax + + + + + + + void + + + + + + + mutcase + NONE + + + + + + + + atom + + + + + + + token + + + + + + + + + + if_then_else + atom_eq + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + if_then_else + int_eq + + + + + + + + + + + if_then_else + less + + + + + + + + + + + by_induction + ind + NONE + + inductive_case + + case_lhs + 0 + + + induction_hypothesis + + + + + + inductive_case + + case_lhs + succ + + + int + + + + induction_hypothesis + + + + + + + inductive_case + + case_lhs + pred + + + int + + + + induction_hypothesis + + + + + + extra_args + + + + + + + + + + + + + + + + + list + + + + + + nil + + + + + + + cons + + + + + + + + + by_induction + list_ind + NONE + + inductive_case + + case_lhs + nil + + + induction_hypothesis + + + + + inductive_case + + case_lhs + cons + + + ? + + + + ? + + + + induction_hypothesis + + + + + + extra_args + + + + + + + + + rec + + + + + + + + + app + + fix + + + + + + + + ? + + + + + + + + + + + + + + + + t_set + + + + + + + + + + + + + + + + + + + + + + + + + isect + + + + + + + + + + + + + + + + quotient + + + + + + + + + + + + + + + type_of + + + + + + + + + + prop + + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/nuprl_tree.xsl b/helm/nuprl_stylesheets/nuprl_tree.xsl new file mode 100644 index 000000000..03daa4726 --- /dev/null +++ b/helm/nuprl_stylesheets/nuprl_tree.xsl @@ -0,0 +1,25 @@ + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/nuprl_stylesheets/xslt_index.txt b/helm/nuprl_stylesheets/xslt_index.txt new file mode 100644 index 000000000..11e49a8ea --- /dev/null +++ b/helm/nuprl_stylesheets/xslt_index.txt @@ -0,0 +1,14 @@ +nuprl_abstract.xsl +nuprl_proof.xsl +nuprl_rules.xsl +nuprl_term.xsl +nuprl_content_to_html.xsl +nuprl_content_to_html2.xsl +nuprl_annotatedpres.xsl +nuprl_mmlextension.xsl +nuprl_expand.xsl +nuprl_tree.xsl +nuprl_link.xsl +nuprl_links_library.xsl +nuprl_html_arith.xsl +nuprl_html_basic.xsl