From: Andrea Asperti Date: Tue, 3 Apr 2001 07:56:41 +0000 (+0000) Subject: Complete management of inductive types. X-Git-Tag: v0_1_2~45 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d4b90e232867dd3cda85b7707ac456b547539a06;p=helm.git Complete management of inductive types. or_ind revisited (full_or_in). (only for html: mml_extension must be upadated!!!). -- andrea --- diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 9de7d4896..028f65504 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -55,7 +55,7 @@ media-type="text/html" doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" /> - + @@ -261,6 +261,11 @@  proves  + + + + Contradiction. + From  @@ -628,16 +633,47 @@ + + + + + + + + + + + + +
Rewrite  - -  with  - -  by  - + +   + +
+ + + +
+ with  + +   + +
+ + + +
+ by  + + +
@@ -651,6 +687,156 @@ Then apply it to  + + + We prove  + + + +
+ + + + by induction on  + + + + + + + + +
+ + +
+ + + + Case  + + + + +
+ + + + By induction hypothesis, we have: + +
+ + + + ( + + + + + +
+
+
+ + + + + + + +
+ + + + + + + + ( + + +   + + : + + + ) + + + + + + By induction on  + : +
+ + + + + Þ + + + +
+ + + + S( + + + Þ + Assume by induction +
+ + + + ( + + ) + + + +
+ + + + + + +
+ + + + + +
+ + + + Contradiction. +
@@ -697,6 +883,62 @@
+ + + + + + + + + + Consider  + + + +
+ + + + We proceed by cases to prove  + +
+ + + + Left: suppose  + ( + + + +
+ + + + + + +
+ + + + Right: suppose  + ( + + + +
+ + + + + + +
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index c40a42ce8..306b48fbc 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -55,6 +55,7 @@ proof + @@ -72,6 +73,7 @@ proof + @@ -88,6 +90,46 @@
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -100,19 +142,30 @@ - + + rw_step @@ -125,7 +178,9 @@ @@ -209,6 +264,16 @@ + + + + false_ind + cic:/Coq/Init/Logic/False_ind.con + + + - - or_ind - - - - - + + + + + full_or_ind + + + + left_case + + + + + + + + + + + + right_case + + + + + + + + + + + + + + + or_ind + + + + + + + + + + @@ -351,6 +459,21 @@ + + + + + + + + + + + + + + +