minimal adaptions for abstract binding type;
authorwenzelm
Sat Mar 07 23:30:58 2009 +0100 (2009-03-07)
changeset 3034690efbb8a8cb2
parent 30345 76fd85bbf139
child 30351 46aa785d1e29
minimal adaptions for abstract binding type;
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Statespace/state_space.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Mar 07 22:17:25 2009 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 07 23:30:58 2009 +0100
     1.3 @@ -1926,7 +1926,8 @@
     1.4          val csyn = mk_syn thy constname
     1.5          val thy1 = case HOL4DefThy.get thy of
     1.6                         Replaying _ => thy
     1.7 -                     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
     1.8 +                     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
     1.9 +                              Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
    1.10          val eq = mk_defeq constname rhs' thy1
    1.11          val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
    1.12          val _ = ImportRecorder.add_defs thmname eq
    1.13 @@ -2017,7 +2018,7 @@
    1.14                                 val thy' = add_dump str thy
    1.15                                 val _ = ImportRecorder.add_consts consts
    1.16                             in
    1.17 -                               Sign.add_consts_i consts thy'
    1.18 +                               Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
    1.19                             end
    1.20  
    1.21              val thy1 = List.foldr (fn(name,thy)=>
    1.22 @@ -2093,7 +2094,9 @@
    1.23              val tnames = map fst tfrees
    1.24              val tsyn = mk_syn thy tycname
    1.25              val typ = (tycname,tnames,tsyn)
    1.26 -            val ((_, typedef_info), thy') = TypedefPackage.add_typedef false (SOME thmname) typ c NONE (rtac th2 1) thy
    1.27 +            val ((_, typedef_info), thy') =
    1.28 +              TypedefPackage.add_typedef false (SOME (Binding.name thmname))
    1.29 +                (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
    1.30              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
    1.31  
    1.32              val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
    1.33 @@ -2179,7 +2182,9 @@
    1.34              val tnames = sort string_ord (map fst tfrees)
    1.35              val tsyn = mk_syn thy tycname
    1.36              val typ = (tycname,tnames,tsyn)
    1.37 -            val ((_, typedef_info), thy') = TypedefPackage.add_typedef false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    1.38 +            val ((_, typedef_info), thy') =
    1.39 +              TypedefPackage.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c
    1.40 +                (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
    1.41              val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
    1.42              val fulltyname = Sign.intern_type thy' tycname
    1.43              val aty = Type (fulltyname, map mk_vartype tnames)
     2.1 --- a/src/HOL/Import/replay.ML	Sat Mar 07 22:17:25 2009 +0100
     2.2 +++ b/src/HOL/Import/replay.ML	Sat Mar 07 23:30:58 2009 +0100
     2.3 @@ -334,7 +334,7 @@
     2.4  	    add_hol4_mapping thyname thmname isaname thy
     2.5  	  | delta (Hol_pending (thyname, thmname, th)) thy = 
     2.6  	    add_hol4_pending thyname thmname ([], th_of thy th) thy
     2.7 -	  | delta (Consts cs) thy = Sign.add_consts_i cs thy
     2.8 +	  | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
     2.9  	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
    2.10  	    add_hol4_const_mapping thyname constname true fullcname thy
    2.11  	  | delta (Hol_move (fullname, moved_thmname)) thy = 
    2.12 @@ -343,8 +343,9 @@
    2.13  	    snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
    2.14  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    2.15  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    2.16 -	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
    2.17 -	    snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy)
    2.18 +	  | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
    2.19 +	    snd (TypedefPackage.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
    2.20 +        (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
    2.21  	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    2.22  	    add_hol4_type_mapping thyname tycname true fulltyname thy
    2.23  	  | delta (Indexed_theorem (i, th)) thy = 
     3.1 --- a/src/HOL/Statespace/state_space.ML	Sat Mar 07 22:17:25 2009 +0100
     3.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Mar 07 23:30:58 2009 +0100
     3.3 @@ -154,13 +154,13 @@
     3.4  
     3.5  fun add_locale name expr elems thy =
     3.6    thy 
     3.7 -  |> Expression.add_locale name name expr elems
     3.8 +  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
     3.9    |> snd
    3.10    |> LocalTheory.exit;
    3.11  
    3.12  fun add_locale_cmd name expr elems thy =
    3.13    thy 
    3.14 -  |> Expression.add_locale_cmd name "" expr elems
    3.15 +  |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
    3.16    |> snd
    3.17    |> LocalTheory.exit;
    3.18  
     4.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Mar 07 22:17:25 2009 +0100
     4.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Mar 07 23:30:58 2009 +0100
     4.3 @@ -324,6 +324,8 @@
     4.4  clist [a] = a |
     4.5  clist (a::r) = a ^ " || " ^ (clist r);
     4.6  
     4.7 +val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
     4.8 +
     4.9  
    4.10  (* add_ioa *)
    4.11  
    4.12 @@ -351,7 +353,7 @@
    4.13  (automaton_name ^ "_trans",
    4.14   "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
    4.15  (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
    4.16 -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
    4.17 +|> add_defs
    4.18  [(automaton_name ^ "_initial_def",
    4.19  automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
    4.20  (automaton_name ^ "_asig_def",
    4.21 @@ -392,7 +394,7 @@
    4.22    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    4.23     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
    4.24  ,NoSyn)]
    4.25 -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
    4.26 +|> add_defs
    4.27  [(automaton_name ^ "_def",
    4.28  automaton_name ^ " == " ^ comp_list)]
    4.29  end)
    4.30 @@ -407,7 +409,7 @@
    4.31  thy
    4.32  |> ContConsts.add_consts_i
    4.33  [(automaton_name, auttyp,NoSyn)]
    4.34 -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
    4.35 +|> add_defs
    4.36  [(automaton_name ^ "_def",
    4.37  automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
    4.38  end)
    4.39 @@ -421,7 +423,7 @@
    4.40  thy
    4.41  |> ContConsts.add_consts_i
    4.42  [(automaton_name, auttyp,NoSyn)]
    4.43 -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
    4.44 +|> add_defs
    4.45  [(automaton_name ^ "_def",
    4.46  automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
    4.47  end)
    4.48 @@ -447,7 +449,7 @@
    4.49    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    4.50     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
    4.51  ,NoSyn)]
    4.52 -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
    4.53 +|> add_defs
    4.54  [(automaton_name ^ "_def",
    4.55  automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
    4.56  end)