# HG changeset patch # User wenzelm # Date 1331327115 -3600 # Node ID 940dbfd43dc4720fcf3a7b6538a0c1aae663215b # Parent 998ec26044c49a90e09cbc834fcc119610aa48fd# Parent 36f392239b6a5686bdacfdf02b3c06983841d89e merged diff -r 36f392239b6a -r 940dbfd43dc4 src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Mar 09 20:04:19 2012 +0100 +++ b/src/HOL/Set.thy Fri Mar 09 22:05:15 2012 +0100 @@ -97,28 +97,28 @@ begin definition less_eq_set where - "less_eq_set A B = less_eq (\x. member x A) (\x. member x B)" + "A \ B \ (\x. member x A) \ (\x. member x B)" definition less_set where - "less_set A B = less (\x. member x A) (\x. member x B)" + "A < B \ (\x. member x A) < (\x. member x B)" definition inf_set where - "inf_set A B = Collect (inf (\x. member x A) (\x. member x B))" + "A \ B = Collect ((\x. member x A) \ (\x. member x B))" definition sup_set where - "sup_set A B = Collect (sup (\x. member x A) (\x. member x B))" + "A \ B = Collect ((\x. member x A) \ (\x. member x B))" definition bot_set where - "bot = Collect bot" + "\ = Collect \" definition top_set where - "top = Collect top" + "\ = Collect \" definition uminus_set where - "uminus A = Collect (uminus (\x. member x A))" + "- A = Collect (- (\x. member x A))" definition minus_set where - "minus_set A B = Collect (minus (\x. member x A) (\x. member x B))" + "A - B = Collect ((\x. member x A) - (\x. member x B))" instance proof qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def @@ -1907,3 +1907,4 @@ *} end + diff -r 36f392239b6a -r 940dbfd43dc4 src/HOL/Tools/enriched_type.ML --- a/src/HOL/Tools/enriched_type.ML Fri Mar 09 20:04:19 2012 +0100 +++ b/src/HOL/Tools/enriched_type.ML Fri Mar 09 22:05:15 2012 +0100 @@ -170,6 +170,33 @@ val (Ts'', T'') = split_last Ts'; in (Ts'', T'', T') end; +fun analyze_mapper ctxt input_mapper = + let + val T = fastype_of input_mapper; + val _ = Type.no_tvars T; + val _ = + if null (subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper [])) + then () + else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper); + val _ = + if null (Term.add_vars (singleton + (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) []) + then () + else error ("Illegal locally free variable(s) in term: " + ^ Syntax.string_of_term ctxt input_mapper);; + val mapper = singleton (Variable.polymorphic ctxt) input_mapper; + val _ = + if null (Term.add_tfreesT (fastype_of mapper) []) then () + else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T); + fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts + | add_tycos _ = I; + val tycos = add_tycos T []; + val tyco = if tycos = ["fun"] then "fun" + else case remove (op =) "fun" tycos + of [tyco] => tyco + | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T); + in (mapper, T, tyco) end; + fun analyze_variances ctxt tyco T = let fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T); @@ -198,19 +225,7 @@ fun gen_enriched_type prep_term some_prfx raw_mapper lthy = let - val input_mapper = prep_term lthy raw_mapper; - val T = fastype_of input_mapper; - val _ = Type.no_tvars T; - val mapper = singleton (Variable.polymorphic lthy) input_mapper; - val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then () - else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T); - fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts - | add_tycos _ = I; - val tycos = add_tycos T []; - val tyco = if tycos = ["fun"] then "fun" - else case remove (op =) "fun" tycos - of [tyco] => tyco - | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ lthy T); + val (mapper, T, tyco) = analyze_mapper lthy (prep_term lthy raw_mapper); val prfx = the_default (Long_Name.base_name tyco) some_prfx; val variances = analyze_variances lthy tyco T; val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper); @@ -221,8 +236,9 @@ val typ_instance = Sign.typ_instance (Context.theory_of context); val mapper' = Morphism.term phi mapper; val T_T' = pairself fastype_of (mapper, mapper'); + val vars = Term.add_vars mapper' []; in - if typ_instance T_T' andalso typ_instance (swap T_T') + if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T') then (Data.map o Symtab.cons_list) (tyco, { mapper = mapper', variances = variances, comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context diff -r 36f392239b6a -r 940dbfd43dc4 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Fri Mar 09 20:04:19 2012 +0100 +++ b/src/Tools/Code/code_scala.ML Fri Mar 09 22:05:15 2012 +0100 @@ -130,10 +130,11 @@ val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars; val p_body = print_term tyvars false some_thm vars' NOBR body in concat [str "case", p_pat, str "=>", p_body] end; - in brackify_block fxy - (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"]) - (map print_select clauses) - (str "}") + in + map print_select clauses + |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}") + |> single + |> enclose "(" ")" end | print_case tyvars some_thm vars fxy ((_, []), _) = (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];