update_name_tr: more precise handling of explicit constraints, including positions;
authorwenzelm
Tue Mar 22 16:15:50 2011 +0100 (2011-03-22)
changeset 42053006095137a81
parent 42052 34f1d2d81284
child 42054 8cd4783904d8
update_name_tr: more precise handling of explicit constraints, including positions;
src/HOL/Isar_Examples/Hoare.thy
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Tue Mar 22 15:32:47 2011 +0100
     1.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Mar 22 16:15:50 2011 +0100
     1.3 @@ -302,7 +302,7 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
     1.8 +lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
     1.9    by (rule basic)
    1.10  
    1.11  text {* Note that above formulation of assignment corresponds to our
     2.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Mar 22 15:32:47 2011 +0100
     2.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 22 16:15:50 2011 +0100
     2.3 @@ -42,6 +42,8 @@
     2.4      case_fixed: string -> 'a,
     2.5      case_default: string -> 'a} -> string -> 'a
     2.6    val is_marked: string -> bool
     2.7 +  val dummy_type: term
     2.8 +  val fun_type: term
     2.9    val pretty_position: Position.T -> Pretty.T
    2.10    val encode_position: Position.T -> string
    2.11    val decode_position: string -> Position.T option
    2.12 @@ -380,6 +382,9 @@
    2.13    unmark {case_class = K true, case_type = K true, case_const = K true,
    2.14      case_fixed = K true, case_default = K false};
    2.15  
    2.16 +val dummy_type = const (mark_type "dummy");
    2.17 +val fun_type = const (mark_type "fun");
    2.18 +
    2.19  
    2.20  (* read numbers *)
    2.21  
     3.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 15:32:47 2011 +0100
     3.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 16:15:50 2011 +0100
     3.3 @@ -188,8 +188,10 @@
     3.4  fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
     3.5    | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
     3.6    | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
     3.7 -      list_comb (c $ update_name_tr [t] $
     3.8 -        (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
     3.9 +      if Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
    3.10 +      else
    3.11 +        list_comb (c $ update_name_tr [t] $
    3.12 +          (Lexicon.fun_type $ (Lexicon.fun_type $ ty $ ty) $ Lexicon.dummy_type), ts)
    3.13    | update_name_tr ts = raise TERM ("update_name_tr", ts);
    3.14  
    3.15  
     4.1 --- a/src/Pure/Syntax/type_ext.ML	Tue Mar 22 15:32:47 2011 +0100
     4.2 +++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 22 16:15:50 2011 +0100
     4.3 @@ -9,6 +9,7 @@
     4.4    val sort_of_term: term -> sort
     4.5    val term_sorts: term -> (indexname * sort) list
     4.6    val typ_of_term: (indexname -> sort) -> term -> typ
     4.7 +  val is_position: term -> bool
     4.8    val strip_positions: term -> term
     4.9    val strip_positions_ast: Ast.ast -> Ast.ast
    4.10    val decode_term: (((string * int) * sort) list -> string * int -> sort) ->