src/HOL/List.thy
changeset 46138 85f8d8a8c711
parent 46133 d9fe85d3d2cd
child 46143 c932c80d3eae
equal deleted inserted replaced
46137:0477785525be 46138:85f8d8a8c711
   347 It is easy to write short list comprehensions which stand for complex
   347 It is easy to write short list comprehensions which stand for complex
   348 expressions. During proofs, they may become unreadable (and
   348 expressions. During proofs, they may become unreadable (and
   349 mangled). In such cases it can be advisable to introduce separate
   349 mangled). In such cases it can be advisable to introduce separate
   350 definitions for the list comprehensions in question.  *}
   350 definitions for the list comprehensions in question.  *}
   351 
   351 
   352 nonterminal lc_gen and lc_qual and lc_quals
   352 nonterminal lc_qual and lc_quals
   353 
   353 
   354 syntax
   354 syntax
   355 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
   355   "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
   356 "_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
   356   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
   357 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
   357   "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
   358 (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
   358   (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
   359 "_lc_end" :: "lc_quals" ("]")
   359   "_lc_end" :: "lc_quals" ("]")
   360 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
   360   "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")
   361 "_lc_abs" :: "'a => 'b list => 'b list"
   361   "_lc_abs" :: "'a => 'b list => 'b list"
   362 "_strip_positions" :: "'a \<Rightarrow> lc_gen"  ("_")
       
   363 
   362 
   364 (* These are easier than ML code but cannot express the optimized
   363 (* These are easier than ML code but cannot express the optimized
   365    translation of [e. p<-xs]
   364    translation of [e. p<-xs]
   366 translations
   365 translations
   367 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
   366   "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
   368 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
   367   "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
   369  => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
   368    => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
   370 "[e. P]" => "if P then [e] else []"
   369   "[e. P]" => "if P then [e] else []"
   371 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
   370   "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
   372  => "if P then (_listcompr e Q Qs) else []"
   371    => "if P then (_listcompr e Q Qs) else []"
   373 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
   372   "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
   374  => "_Let b (_listcompr e Q Qs)"
   373    => "_Let b (_listcompr e Q Qs)"
   375 *)
   374 *)
   376 
   375 
   377 syntax (xsymbols)
   376 syntax (xsymbols)
   378 "_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
   377   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
   379 syntax (HTML output)
   378 syntax (HTML output)
   380 "_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
   379   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
   381 
   380 
   382 parse_translation (advanced) {*
   381 parse_translation (advanced) {*
   383 let
   382   let
   384   val NilC = Syntax.const @{const_syntax Nil};
   383     val NilC = Syntax.const @{const_syntax Nil};
   385   val ConsC = Syntax.const @{const_syntax Cons};
   384     val ConsC = Syntax.const @{const_syntax Cons};
   386   val mapC = Syntax.const @{const_syntax map};
   385     val mapC = Syntax.const @{const_syntax map};
   387   val concatC = Syntax.const @{const_syntax concat};
   386     val concatC = Syntax.const @{const_syntax concat};
   388   val IfC = Syntax.const @{const_syntax If};
   387     val IfC = Syntax.const @{const_syntax If};
   389 
   388 
   390   fun singl x = ConsC $ x $ NilC;
   389     fun single x = ConsC $ x $ NilC;
   391 
   390 
   392   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
   391     fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
   393     let
   392       let
   394       (* FIXME proper name context!? *)
   393         (* FIXME proper name context!? *)
   395       val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
   394         val x =
   396       val e = if opti then singl e else e;
   395           Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
   397       val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
   396         val e = if opti then single e else e;
   398       val case2 =
   397         val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
   399         Syntax.const @{syntax_const "_case1"} $
   398         val case2 =
   400           Syntax.const @{const_syntax dummy_pattern} $ NilC;
   399           Syntax.const @{syntax_const "_case1"} $
   401       val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
   400             Syntax.const @{const_syntax dummy_pattern} $ NilC;
   402       val ft = Datatype_Case.case_tr false ctxt [x, cs];
   401         val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
   403     in lambda x ft end;
   402       in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr false ctxt [x, cs]] end;
   404 
   403 
   405   fun abs_tr ctxt (p as Free (s, T)) e opti =
   404     fun abs_tr ctxt p e opti =
   406         let
   405       (case Term_Position.strip_positions p of
   407           val thy = Proof_Context.theory_of ctxt;
   406         Free (s, T) =>
   408           val s' = Proof_Context.intern_const ctxt s;
   407           let
   409         in
   408             val thy = Proof_Context.theory_of ctxt;
   410           if Sign.declared_const thy s'
   409             val s' = Proof_Context.intern_const ctxt s;
   411           then (pat_tr ctxt p e opti, false)
   410           in
   412           else (lambda p e, true)
   411             if Sign.declared_const thy s'
   413         end
   412             then (pat_tr ctxt p e opti, false)
   414     | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
   413             else (Syntax_Trans.abs_tr [p, e], true)
   415 
   414           end
   416   fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
   415       | _ => (pat_tr ctxt p e opti, false));
   417         let
   416 
   418           val res =
   417     fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
   419             (case qs of
   418           let
   420               Const (@{syntax_const "_lc_end"}, _) => singl e
   419             val res =
   421             | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
   420               (case qs of
   422         in IfC $ b $ res $ NilC end
   421                 Const (@{syntax_const "_lc_end"}, _) => single e
   423     | lc_tr ctxt
   422               | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
   424           [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   423           in IfC $ b $ res $ NilC end
   425             Const(@{syntax_const "_lc_end"}, _)] =
   424       | lc_tr ctxt
   426         (case abs_tr ctxt p e true of
   425             [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   427           (f, true) => mapC $ f $ es
   426               Const(@{syntax_const "_lc_end"}, _)] =
   428         | (f, false) => concatC $ (mapC $ f $ es))
   427           (case abs_tr ctxt p e true of
   429     | lc_tr ctxt
   428             (f, true) => mapC $ f $ es
   430           [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   429           | (f, false) => concatC $ (mapC $ f $ es))
   431             Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
   430       | lc_tr ctxt
   432         let val e' = lc_tr ctxt [e, q, qs];
   431             [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   433         in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
   432               Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
   434 
   433           let val e' = lc_tr ctxt [e, q, qs];
   435 in [(@{syntax_const "_listcompr"}, lc_tr)] end
   434           in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
       
   435 
       
   436   in [(@{syntax_const "_listcompr"}, lc_tr)] end
   436 *}
   437 *}
   437 
   438 
   438 ML {*
   439 ML {*
   439   let
   440   let
   440     val read = Syntax.read_term @{context};
   441     val read = Syntax.read_term @{context};