Theory Floor2_examp
section‹Main Translation for: Example (Floor 2)›
theory Floor2_examp
imports Floor1_examp
begin
definition "print_examp_def_st_locale_distinct = ‹distinct_oid›"
definition "print_examp_def_st_locale_metis = M.metis (L.map T.thm [print_examp_def_st_locale_distinct, ‹distinct_length_2_or_more›])"
definition "print_examp_def_st_locale_aux f_toyi l =
(let b = λs. Term_basic [s] in
map_prod
id
L.flatten
(L.split
(L.map
(λ name.
let (toyi, cpt) = f_toyi name
; n = inst_name toyi
; ty = inst_ty toyi
; f = λs. s @@ String.isub ty
; name_pers = print_examp_instance_name f n in
( Term_oid var_oid_uniq (oidGetInh cpt)
, [ ( [(b name_pers, Typ_base (f datatype_name))], None)
, ( [(b n, Typ_base (wrap_toyty ty))]
, Some (hol_definition n, Term_rewrite (b n) ‹=› (Term_lambda wildcard (Term_some (Term_some (b name_pers)))))) ]))
l)))"
definition "print_examp_def_st_locale_make f_name f_toyi f_spec l =
(let (oid, l_fix_assum) = print_examp_def_st_locale_aux f_toyi l
; ty_n = ‹nat› in
⦇ HolThyLocale_name = f_name
, HolThyLocale_header = L.flatten
[ [ ( L.map (λx. (x, Typ_base ty_n)) oid
, Some ( print_examp_def_st_locale_distinct
, Term_app ‹distinct› [let e = Term_list oid in
if oid = [] then Term_annot' e (ty_n @@ ‹ list›) else e])) ]
, l_fix_assum
, f_spec ] ⦈)"
definition "print_examp_def_st_locale_name n = ‹state_› @@ n"
definition "print_examp_def_st_locale = (λ ToyDefSt n l ⇒ λenv.
(λd. (d, env))
(print_examp_def_st_locale_make
(‹state_› @@ n)
(λ ToyDefCoreBinding name ⇒ case String.assoc name (D_input_instance env) of Some n ⇒ n)
[]
l))"
definition "print_examp_def_st_mapsto_gen f =
L.map
(λ(cpt, ocore).
let b = λs. Term_basic [s]
; (toyi, exp) = case ocore of
ToyDefCoreBinding (name, toyi) ⇒
(toyi, Some (b (print_examp_instance_name (λs. s @@ String.isub (inst_ty toyi)) name))) in
f (cpt, ocore) toyi exp)"
definition "print_examp_def_st_mapsto l = list_bind id id
(print_examp_def_st_mapsto_gen
(λ(cpt, _) toyi. map_option (λexp.
Term_binop (Term_oid var_oid_uniq (oidGetInh cpt)) ‹↦› (Term_app (datatype_in @@ String.isub (inst_ty toyi)) [exp])))
l)"
definition "print_examp_def_st2 = (λ ToyDefSt name l ⇒ λenv.
(λ(l, l_st). (L.map O'.definition l, env ⦇ D_input_state := (String.to_String⇩b⇩a⇩s⇩e name, l_st) # D_input_state env ⦈))
(let b = λs. Term_basic [s]
; l = L.map (λ ToyDefCoreBinding name ⇒ map_option (Pair name) (String.assoc name (D_input_instance env))) l
; (rbt, (map_self, map_username)) =
(init_map_class
(env ⦇ D_toy_oid_start := oidReinitInh (D_toy_oid_start env) ⦈)
(L.map (λ Some (_, toyi, _) ⇒ toyi | None ⇒ toy_instance_single_empty) l)
:: (_ ⇒ _ × _ × (_ ⇒ ((_ ⇒ nat ⇒ _ ⇒ _) ⇒ _
⇒ (toy_ty_class option × (toy_ty × toy_data_shallow) option) list) option)) × _ × _)
; (l_st, l_assoc) = L.mapM (λ o_n l_assoc.
case o_n of
Some (name, toyi, cpt) ⇒ ([(cpt, ToyDefCoreBinding (name, toyi))], (toyi, cpt) # l_assoc)
| None ⇒ ([], l_assoc)) l []
; l_st = L.unique oidGetInh (L.flatten l_st) in
( [ Definition (Term_rewrite (b name) ‹=› (Term_app ‹state.make›
( Term_app ‹Map.empty› (case print_examp_def_st_mapsto l_st of None ⇒ [] | Some l ⇒ l)
# [ print_examp_def_st_assoc (snd o rbt) map_self map_username l_assoc ]))) ]
, l_st)))"
definition "print_examp_def_st_perm_name name = S.flatten [‹perm_›, name]"
definition "print_examp_def_st_perm = (λ _ env.
(λ l. (L.map O'.lemma l, env))
(let (name, l_st) = map_prod String⇩b⇩a⇩s⇩e.to_String id (hd (D_input_state env))
; expr_app = print_examp_def_st_mapsto (rev l_st)
; b = λs. Term_basic [s]
; d = hol_definition
; (l_app, l_last) =
case l_st of [] ⇒ ([], C.by [M.simp_add [d name]])
| [_] ⇒ ([], C.by [M.simp_add [d name]])
| _ ⇒
( [ M.simp_add [d name]]
# L.flatten (L.map (λi_max. L.map (λi. [M.subst_l (L.map String.nat_to_digit10 [i_max - i]) (T.thm ‹fun_upd_twist›), print_examp_def_st_locale_metis]) (List.upt 0 i_max)) (List.upt 1 (List.length l_st)))
, C.by [M.simp]) in
case expr_app of None ⇒ [] | Some expr_app ⇒
[ Lemma
(print_examp_def_st_perm_name name)
[Term_rewrite (b name) ‹=› (Term_app ‹state.make›
(Term_app ‹Map.empty› expr_app # [Term_app var_assocs [b name]]))]
l_app
l_last ]))"
definition "merge_unique_gen f l = List.fold (List.fold (λx. case f x of Some (x, v) ⇒ RBT.insert x v | None ⇒ id)) l RBT.empty"
definition "merge_unique f l = RBT.entries (merge_unique_gen f l)"
definition "merge_unique' = L.map snd o merge_unique (λ (a, b). ((λx. Some (x, (a, b))) o oidGetInh) a)"
definition "get_state f = (λ ToyDefPP _ s_pre s_post ⇒ λ env.
let get_state = let l_st = D_input_state env in λToyDefPPCoreBinding s ⇒ (s, case String.assoc s l_st of None ⇒ [] | Some l ⇒ l)
; (s_pre, l_pre) = get_state s_pre
; (s_post, l_post) = case s_post of None ⇒ (s_pre, l_pre) | Some s_post ⇒ get_state s_post in
f (s_pre, l_pre)
(s_post, l_post)
((s_pre, l_pre) # (if s_pre ≜ s_post then
[]
else
[ (s_post, l_post) ]))
env)"
definition "print_pre_post_locale_aux f_toyi l =
(let (oid, l_fix_assum) = print_examp_def_st_locale_aux f_toyi l in
L.flatten [oid, L.flatten (L.map (L.map fst o fst) l_fix_assum) ])"
definition "print_pre_post_locale = get_state (λ (s_pre, l_pre) (s_post, l_post) l_pre_post. Pair
(let f_toyi = λ(cpt, ToyDefCoreBinding (_, toyi)) ⇒ (toyi, cpt) in
print_examp_def_st_locale_make
(‹pre_post_› @@ s_pre @@ ‹_› @@ s_post)
f_toyi
(L.map (λ(s, l). ([], Some (s, Term_app
(print_examp_def_st_locale_name s)
(print_pre_post_locale_aux f_toyi l))))
l_pre_post)
(merge_unique' [l_pre, l_post])))"
definition "print_pre_post_interp = get_state (λ _ _.
Pair o L.map O'.interpretation o L.map
(λ(s, l).
let n = print_examp_def_st_locale_name s in
Interpretation n n (print_pre_post_locale_aux (λ(cpt, ToyDefCoreBinding (_, toyi)) ⇒ (toyi, cpt)) l) (C.by [M.rule (T.thm s)])))"
definition "print_pre_post_def_state' = get_state (λ pre post _.
(Pair o L.map O'.definition)
(L.map
(let a = λf x. Term_app f [x]
; b = λs. Term_basic [s]
; heap = ‹heap› in
(λ(s, _).
Definition (Term_rewrite (b (heap @@ ‹_› @@ s))
‹=›
(a heap (b (print_examp_def_st_locale_name s @@ ‹.› @@ s))))))
[ pre, post ]))"
end