adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Isabelle2018: AutoCorres

This commit is contained in:
Gerwin Klein 2018-06-22 17:26:53 +02:00
parent bdb3c592b8
commit 1c82254a3c
4 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
tools/autocorres/TypHeapSimple.thy
View File

@ -106,7 +106,7 @@ lemma if_eqI:
by simp
lemma heap_type_tag_ptr_retyp:
"snd (s (ptr_val t)) = empty \<Longrightarrow>
"snd (s (ptr_val t)) = Map.empty \<Longrightarrow>
heap_type_tag (ptr_retyp (t :: 'a::mem_type ptr) s) (ptr_val t) = HeapType (typ_uinfo_t TYPE('a))"
apply (unfold ptr_retyp_def heap_type_tag_def)
apply (subst htd_update_list_index, fastforce, fastforce)+
@ -126,7 +126,7 @@ lemma not_snd_last_typ_slice_t:
by (case_tac z, clarsimp)
lemma heap_type_tag_ptr_retyp_rest:
"\<lbrakk> snd (s (ptr_val t + k)) = empty; 0 < k; unat k < size_td (typ_uinfo_t TYPE('a)) \<rbrakk> \<Longrightarrow>
"\<lbrakk> snd (s (ptr_val t + k)) = Map.empty; 0 < k; unat k < size_td (typ_uinfo_t TYPE('a)) \<rbrakk> \<Longrightarrow>
heap_type_tag (ptr_retyp (t :: 'a::mem_type ptr) s) (ptr_val t + k) = HeapFootprint"
apply (unfold ptr_retyp_def heap_type_tag_def)
apply (subst htd_update_list_index, simp, clarsimp,

2
tools/autocorres/autocorres_trace.ML
View File

@ -350,7 +350,7 @@ fun dropQuotes s = if String.isPrefix "\"" s andalso String.isSuffix "\"" s
then String.substring (s, 1, String.size s - 2) else s
fun cterm_to_string no_markup =
Proof_Display.pp_cterm Thy_Info.pure_theory
Proof_Display.pp_cterm (fn _ => @{theory Pure})
#> Pretty.string_of
#> YXML.parse_body
#> (if no_markup then XML.content_of else YXML.string_of_body)

2
tools/autocorres/heap_lift.ML
View File

@ -137,7 +137,7 @@ end
(* The opposite to "mk_first_order" *)
fun dest_first_order ctxt ct =
Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv
@{lemma "(op $) == (%a b. a b)" by (rule meta_ext, rule ext, simp)}))) ctxt ct
@{lemma "($) == (%a b. a b)" by (rule meta_ext, rule ext, simp)}))) ctxt ct
(*
* Resolve "base_thm" with "subgoal_thm" in all assumptions it is possible to

2
tools/autocorres/trace_antiquote.ML
View File

@ -23,7 +23,7 @@ struct
val tracing_str =
"(fn x => (Pretty.writeln (Pretty.enum \" \" \"\" \"\" ["
^ "Pretty.str \"Trace:\", (Pretty.from_ML (ML_Pretty.from_polyml ("
^ "ML_system_pretty (x, ML_Print_Depth.get_print_depth ()))))])))"
^ "ML_system_pretty (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ())))))])))"
val _ = Theory.setup (ML_Antiquotation.inline (Binding.name "trace") (Scan.succeed tracing_str))