132 lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" .. |
132 lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" .. |
133 |
133 |
134 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. |
134 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. |
135 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
135 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
136 lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. |
136 lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. |
|
137 lemma [code, code del]: |
|
138 "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" .. |
|
139 lemma [code, code del]: |
|
140 "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" .. |
137 |
141 |
138 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c = |
142 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c = |
139 (let (n, m) = nibble_pair_of_char c |
143 (let (n, m) = nibble_pair_of_char c |
140 in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
144 in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
141 (Code_Eval.term_of n)) (Code_Eval.term_of m))" |
145 (Code_Eval.term_of n)) (Code_Eval.term_of m))" |