X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fparamodulation%2Fparamodulation.ma;h=17cd3199a7448a6078e0149213313a2b6a148bd2;hb=ff5659b6ee47292a33c84b0889b5d66d729397f6;hp=aaaf36312a8582d51d4dc15451520f9a26746a35;hpb=7245ccc4076a799ac50546e70327320a8625b5e8;p=helm.git

diff --git a/helm/software/matita/library/paramodulation/paramodulation.ma b/helm/software/matita/library/paramodulation/paramodulation.ma
index aaaf36312..17cd3199a 100644
--- a/helm/software/matita/library/paramodulation/paramodulation.ma
+++ b/helm/software/matita/library/paramodulation/paramodulation.ma
@@ -15,8 +15,156 @@
 set "baseuri" "cic:/matita/paramodulation/".
 
 include "nat/nat.ma".
+include "datatypes/bool.ma".
 
-definition make_eqs_smart \def 
+inductive List (U:Type) : nat \to Type \def
+  | Nil : List U O
+  | Cons : \forall n.U \to List U n \to List U (S n).
+
+(*  
+definition mk_T \def \lambda U:Type.\lambda n:nat.List U n \to Prop.
+
+definition app_T' \def 
+  \lambda n:nat.
+  \lambda U:Type.
+  \lambda a:U.
+  \lambda t:mk_T U (S n).
+  \lambda l:List U n.t (Cons U n a l).
+    
+let rec mk_Arrow' (n:nat) (U:Type) on n \def
+  match n return \lambda x.\forall t:mk_T U x.Prop with 
+  [ O ⇒ 
+     \lambda t:mk_T U O.t (Nil U)
+  | (S m) ⇒ 
+     \lambda t:mk_T U (S m).\forall a.mk_Arrow' m U (app_T' m U a t)].
+
+theorem leaf':
+  \forall U:Type.
+  \forall n:nat.
+  \forall actual_params:List U n.
+  \forall pred:mk_T U n.
+  \forall H:mk_Arrow' n U pred.
+  pred actual_params.
+  intros 3.
+  elim actual_params; 
+    [ exact H.
+    | simplify in H1.
+      unfold app_T' in H1.
+      lapply (H1 t).
+      apply H.
+      assumption
+    ]   
+qed.
+*)
+  
+definition mk_Tside \def \lambda U:Type.\lambda n:nat.List U n \to U.
+
+definition app_T \def 
+  \lambda n:nat.
+  \lambda U:Type.
+  \lambda a:U.
+  \lambda side:mk_Tside U (S n).
+  \lambda args:List U n.side (Cons U n a args).
+     
+let rec mk_Arrow (n:nat) (U:Type) (eq:\forall T:Type.T\to T\to Prop) on n \def
+  match n return \lambda x.\forall l:mk_Tside U x.\forall r:mk_Tside U x.Prop with 
+  [ O ⇒ 
+     \lambda l:mk_Tside U O.\lambda r:mk_Tside U O.eq U (l (Nil U)) (r (Nil U))
+  | (S m) ⇒ 
+     \lambda l:mk_Tside U (S m).\lambda r:mk_Tside U (S m).\forall a.
+       mk_Arrow m U eq (app_T m U a l) (app_T m U a r)].    
+
+definition sym \def
+  \lambda eq:\forall T:Type.T\to T\to Prop.
+  \lambda U:Type.
+  \lambda l,r:U.
+  \lambda b:bool.
+  match b with 
+  [ true ⇒ eq U r l
+  | false ⇒ eq U l r].
+
+let rec mk_TsideArr (n:nat) (U:Type) on n \def
+  match n with 
+  [ O ⇒ U
+  | (S m) ⇒  U \to mk_TsideArr m U].
+
+let rec mk_Statement 
+  (n:nat) (U:Type) (eq:\forall T:Type.T\to T\to Prop) (b:bool) 
+  (context:U \to U) on n  
+\def
+  match n return \lambda x.\forall l:mk_TsideArr x U.\forall r:mk_TsideArr x U.Prop with 
+  [ O ⇒ 
+     \lambda predl:mk_TsideArr O U.
+     \lambda predr:mk_TsideArr O U.
+       sym eq U (context predl) (context predr) b
+  | (S m) ⇒ 
+     \lambda predl:mk_TsideArr (S m) U.\lambda predr:mk_TsideArr (S m) U.
+     \forall a:U.
+       mk_Statement m U eq b context (predl a) (predr a)].    
+
+theorem eq_f_to_mk_Statement:
+  \forall eq:\forall T:Type.T\to T\to Prop.
+  \forall sym_eq: \forall T:Type.\forall l,r:T.eq T l r \to eq T r l.
+  \forall eq_f :
+    \forall U,U1:Type.
+    \forall f:U \to U1.\forall x,y:U. eq U x y \to eq U1 (f x) (f y).
+  \forall b:bool.
+  \forall U:Type.
+  \forall context: U \to U.
+  \forall n:nat.
+  \forall predl:mk_TsideArr n U.
+  \forall predr:mk_TsideArr n U.
+  \forall H:mk_Statement n U eq false (\lambda x.x) predl predr.
+  mk_Statement n U eq b context predl predr.
+  intros 7.
+  elim n;
+  [ simplify in H2.
+    elim b;
+    [ simplify.
+      apply H1.
+      apply H.
+      assumption.
+    | simplify.
+      apply H1.
+      assumption.
+    ]  
+  | generalize in match H2.
+    clear H2.
+    elim b;
+    [ simplify.
+      intro.
+      apply H2.
+      simplify in H3.
+      apply H3.
+    | simplify.
+      intro.
+      apply H2.
+      simplify in H3.
+      apply H3.
+    ]
+  ]
+qed.
+
+variant rewrite : 
+  \forall eq:\forall T:Type.T\to T\to Prop.
+  \forall sym_eq: \forall T:Type.\forall l,r:T.eq T l r \to eq T r l.
+  \forall eq_f :
+    \forall U,U1:Type.
+    \forall f:U \to U1.\forall x,y:U. eq U x y \to eq U1 (f x) (f y).
+  \forall b:bool.
+  \forall U:Type.
+  \forall context: U \to U.
+  \forall n:nat.
+  \forall predl:mk_TsideArr n U.
+  \forall predr:mk_TsideArr n U.
+  \forall H:mk_Statement n U eq false (\lambda x.x) predl predr.
+  mk_Statement n U eq b context predl predr
+\def 
+  eq_f_to_mk_Statement.
+
+(*
+
+definition make_eqs_smart' \def 
   \lambda Univ:Type.
   \lambda length:nat.
   \lambda initial:Univ.
@@ -28,18 +176,18 @@ definition make_eqs_smart \def
   in 
     aux initial length.
   
-theorem transl_smart : 
+theorem transl_smart' : 
   \forall Univ:Type.\forall n:nat.\forall initial:Univ.
-    make_eqs_smart Univ n initial.
+    make_eqs_smart' Univ n initial.
   intros.
-  unfold make_eqs_smart.
+  unfold make_eqs_smart'.
   elim n
   [ simplify.intros.assumption
   | simplify.intros.rewrite < H1.assumption
   ]
 qed.  
 
-theorem prova:
+theorem prova':
   \forall Univ:Type.
   \forall a,b:Univ.
   \forall plus: Univ \to Univ \to Univ.
@@ -47,6 +195,7 @@ theorem prova:
   \forall H1:plus b a = plus b b.
   plus a b = plus b b.
   intros.
-  apply (transl_smart ? (S O) ? ? (H a b) ? H1).
+  apply (transl_smart' ? (S O) ? ? (H a b) ? H1).
 qed. 
   
+*)
\ No newline at end of file