17 val istate2str : istate -> string |
17 val istate2str : istate -> string |
18 val e_istate : istate |
18 val e_istate : istate |
19 type subs |
19 type subs |
20 type sube |
20 type sube |
21 type subte |
21 type subte |
|
22 val subst'_to_sube : term -> Rule.cterm' list |
22 val sube2str : Rule.cterm' list -> string |
23 val sube2str : Rule.cterm' list -> string |
23 val sube2subst : theory -> Rule.cterm' list -> (term * term) list |
24 val sube2subst : theory -> Rule.cterm' list -> (term * term) list |
24 val sube2subte : Rule.cterm' list -> term list |
25 val sube2subte : Rule.cterm' list -> term list |
25 val subs2subst : theory -> Rule.cterm' list -> (term * term) list |
26 val subs2subst : theory -> Rule.cterm' list -> (term * term) list |
26 val subst2sube : (term * term) list -> Rule.cterm' list (* for datatypes.sml *) |
27 val subst2sube : (term * term) list -> Rule.cterm' list (* for datatypes.sml *) |
116 fun sube2str s = strs2str s; |
117 fun sube2str s = strs2str s; |
117 |
118 |
118 (* _sub_stitution as _t_erms of _e_qualities *) |
119 (* _sub_stitution as _t_erms of _e_qualities *) |
119 type subte = term list; |
120 type subte = term list; |
120 |
121 |
|
122 type subst' = term (* decomposes to "(char list * term) list", where term is Free ("xxx", _) |
|
123 e.g. @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"} *) |
|
124 fun subst'_to_sube sub = sub |
|
125 |> HOLogic.dest_list |
|
126 |> map HOLogic.dest_prod |
|
127 |> map (fn (e1, e2) => (HOLogic.dest_string e1, Rule.term2str e2)) |
|
128 |> map (fn (e1, e2) => "(" ^ e1 ^ ", " ^ e2 ^ ")"): Rule.cterm' list |
|
129 |
121 val subte2sube = map Rule.term2str; |
130 val subte2sube = map Rule.term2str; |
122 val subst2subs = map (pair2str o (apfst Rule.term2str) o (apsnd Rule.term2str)); |
131 val subst2subs = map (pair2str o (apfst Rule.term2str) o (apsnd Rule.term2str)); |
123 fun subst2sube subst = map Rule.term2str (map HOLogic.mk_eq subst) |
132 fun subst2sube subst = map Rule.term2str (map HOLogic.mk_eq subst) |
124 val subst2subs' = map ((apfst Rule.term2str) o (apsnd Rule.term2str)); |
133 val subst2subs' = map ((apfst Rule.term2str) o (apsnd Rule.term2str)); |
125 fun subs2subst thy s = map (TermC.isapair2pair o (TermC.parse_patt thy)) s; |
134 fun subs2subst thy s = map (TermC.isapair2pair o (TermC.parse_patt thy)) s; |