From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 2 Mar 2009 23:34:30 +0000 (+0000)
Subject: First version.
X-Git-Tag: make_still_working~4182
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eb0dee396c1a88059cae089aed3184b5d4cf9a72;p=helm.git

First version.
---

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
new file mode 100755
index 000000000..d388acd89
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -0,0 +1,142 @@
+type t = M | I | C
+type w = t list
+type eqclass = w list
+
+let rules =
+ [ [I;I],   [I];
+   [C;C],   [C];
+   [M;M],   [];
+   [M;C],   [I;M];
+   [C;M],   [M;I];
+(*
+axiom leq_refl: ∀A. A ⊆ A.
+axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
+axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
+
+axiom i_contrattivita: ∀A. i A ⊆ A.
+axiom i_idempotenza: ∀A. i (i A) = i A.
+axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
+axiom c_espansivita: ∀A. A ⊆ c A.
+axiom c_idempotenza: ∀A. c (c A) = c A.
+axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
+axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
+axiom m_saturazione: ∀A. A ⊆ m (m A).
+axiom m_puntofisso: ∀A. m A = m (m (m A)).
+axiom th1: ∀A. c (m A) ⊆ m (i A).
+axiom th2: ∀A. i (m A) ⊆ m (c A).
+lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
+lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
+*)
+ ]
+;;
+
+let print_w w =
+ String.concat ""
+  (List.map (function I -> "i" | C -> "c" | M -> "-") w)
+;;
+
+let print_eqclass eqc =
+ let eqc = List.sort compare eqc in
+  prerr_endline (String.concat "=" (List.map print_w eqc))
+;;
+
+let print = List.iter print_eqclass;;
+
+exception NoMatch;;
+
+let apply_rule_at_beginning (lhs,rhs) l =
+ let rec aux =
+  function
+     [],l -> l
+   | x::lhs,x'::l when x = x' -> aux (lhs,l)
+   | _,_ -> raise NoMatch
+ in
+  rhs @ aux (lhs,l)
+;;
+
+let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2
+;;
+
+let rec apply_rule rule w =
+ (try
+   [apply_rule_at_beginning rule w]
+  with
+   NoMatch -> []) @
+ match w with
+    [] -> []
+  | he::tl -> [he] @@ apply_rule rule tl
+;;
+
+let uniq =
+ let rec aux l =
+  function
+     [] -> l
+   | he::tl -> aux (if List.mem he l then l else he::l) tl
+ in
+  aux []
+;;
+
+let apply_rules w =
+ let rec aux =
+  function
+     [] -> [w]
+   | rule::rules -> apply_rule rule w @ aux rules
+ in
+  uniq (aux rules)
+;;
+
+let subseteq l1 l2 =
+ List.for_all (fun x -> List.mem x l2) l1
+;;
+
+let (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;;
+
+let simplify eqc =
+ let rec aux l =
+  let l' = uniq (List.flatten (List.map apply_rules l)) in
+  if l === l' then l else aux l'
+ in
+  aux eqc
+;;
+
+let combine_class_with_classes l1 =
+ let rec aux =
+  function
+     [] -> [l1]
+   | l2::tl ->
+      if List.exists (fun x -> List.mem x l2) l1 then
+       uniq (l1 @ l2) :: tl
+      else
+       l2:: aux tl
+ in
+  aux
+;;
+
+let combine_classes l =
+ let rec aux acc =
+  function
+     [] -> acc
+   | he::tl -> aux (combine_class_with_classes he acc) tl
+ in
+  aux [] l
+;;
+
+let step (s : eqclass list) =
+ let ns = ref [] in
+  List.iter (function eqc -> ns := eqc::!ns) s;
+  List.iter
+   (function eqc ->
+     List.iter
+      (function x ->
+        let eqc = simplify ([x] @@ eqc) in
+         if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
+          ns := eqc::!ns
+      ) [I;C;M]
+   ) s;
+  combine_classes !ns
+;;
+
+let classes = step (step (step (step [[[]]]))) in
+ prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
+ print classes
+;;