diff -r a6f3e1b08494 -r b6873d123f9b Attic/Quot/Examples/FSet3.thy
--- a/Attic/Quot/Examples/FSet3.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-theory FSet3
-imports "../../../Nominal/FSet"
-begin
-
-(* TBD *)
-
-text {* syntax for fset comprehensions (adapted from lists) *}
-
-nonterminals fsc_qual fsc_quals
-
-syntax
-"_fsetcompr" :: "'a \<Rightarrow> fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> 'a fset"  ("{|_ . __")
-"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ <- _")
-"_fsc_test" :: "bool \<Rightarrow> fsc_qual" ("_")
-"_fsc_end" :: "fsc_quals" ("|}")
-"_fsc_quals" :: "fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> fsc_quals" (", __")
-"_fsc_abs" :: "'a => 'b fset => 'b fset"
-
-syntax (xsymbols)
-"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
-syntax (HTML output)
-"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
-
-parse_translation (advanced) {*
-let
-  val femptyC = Syntax.const @{const_name fempty};
-  val finsertC = Syntax.const @{const_name finsert};
-  val fmapC = Syntax.const @{const_name fmap};
-  val fconcatC = Syntax.const @{const_name fconcat};
-  val IfC = Syntax.const @{const_name If};
-  fun fsingl x = finsertC $ x $ femptyC;
-
-  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
-    let
-      val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
-      val e = if opti then fsingl e else e;
-      val case1 = Syntax.const "_case1" $ p $ e;
-      val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
-                                        $ femptyC;
-      val cs = Syntax.const "_case2" $ case1 $ case2
-      val ft = Datatype_Case.case_tr false Datatype.info_of_constr
-                 ctxt [x, cs]
-    in lambda x ft end;
-
-  fun abs_tr ctxt (p as Free(s,T)) e opti =
-        let val thy = ProofContext.theory_of ctxt;
-            val s' = Sign.intern_const thy s
-        in if Sign.declared_const thy s'
-           then (pat_tr ctxt p e opti, false)
-           else (lambda p e, true)
-        end
-    | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
-
-  fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] =
-        let 
-          val res = case qs of 
-                      Const("_fsc_end",_) => fsingl e
-                    | Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs];
-        in 
-          IfC $ b $ res $ femptyC 
-        end
-
-    | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] =
-         (case abs_tr ctxt p e true of
-            (f,true) => fmapC $ f $ es
-          | (f, false) => fconcatC $ (fmapC $ f $ es))
-       
-    | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] =
-        let
-          val e' = fsc_tr ctxt [e, q, qs];
-        in 
-          fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es) 
-        end
-
-in [("_fsetcompr", fsc_tr)] end
-*}
-
-
-(* NEEDS FIXING *)
-(* examles *)
-(*
-term "{|(x,y,z). b|}"
-term "{|x. x \<leftarrow> xs|}"
-term "{|(x,y,z). x\<leftarrow>xs|}"
-term "{|e x y. x\<leftarrow>xs, y\<leftarrow>ys|}"
-term "{|(x,y,z). x<a, x>b|}"
-term "{|(x,y,z). x\<leftarrow>xs, x>b|}"
-term "{|(x,y,z). x<a, x\<leftarrow>xs|}"
-term "{|(x,y). Cons True x \<leftarrow> xs|}"
-term "{|(x,y,z). Cons x [] \<leftarrow> xs|}"
-term "{|(x,y,z). x<a, x>b, x=d|}"
-term "{|(x,y,z). x<a, x>b, y\<leftarrow>ys|}"
-term "{|(x,y,z). x<a, x\<leftarrow>xs,y>b|}"
-term "{|(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys|}"
-term "{|(x,y,z). x\<leftarrow>xs, x>b, y<a|}"
-term "{|(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys|}"
-term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x|}"
-term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs|}"
-*)
-
-(* BELOW CONSTRUCTION SITE *)
-
-
-end