synchronize with compiler/core/Floor2_examp.thy

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14176 3260e6d1-4efc-4170-b0a7-36055960796d

Citadelle/src/compiler_generic/toy_example/embedding/Core.thy

@@ -115,6 +115,7 @@ local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_examp_d
 local_setup \<open>embedding_fun_info_f1 @{const_name Floor1_examp.print_transition}\<close>
 local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_transition_locale}\<close>
 local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_transition_interp}\<close>
+local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_transition_def_state'}\<close>
 local_setup \<open>embedding_fun_info_f1 @{const_name Floor1_ctxt.print_ctxt}\<close>
 local_setup \<open>embedding_fun_info @{const_name print_meta_setup_def_state}\<close>
 local_setup \<open>embedding_fun_info @{const_name print_meta_setup_def_transition}\<close>
@@ -189,7 +190,8 @@ definition "thy_def_transition = (\<lambda> Floor1 \<Rightarrow> Embed_theories
                                 | Floor2 \<Rightarrow> Embed_locale
                                               [ section' \<open>Transition (Floor 2)\<close> ]
                                               Floor2_examp.print_transition_locale
-                                              [ Floor2_examp.print_transition_interp ])"
+                                              [ Floor2_examp.print_transition_interp
+                                              , Floor2_examp.print_transition_def_state' ])"
 definition "thy_ctxt = (\<lambda> Floor1 \<Rightarrow> Embed_theories
                                       [ section' \<open>Context (Floor 1)\<close>
                                       , floor1_PRINT_ctxt ]

Citadelle/src/compiler_generic/toy_example/embedding/core/Floor2_examp.thy

@@ -236,4 +236,16 @@ definition "print_transition_interp = get_state (\<lambda> _ _.
     Interpretation n n (print_transition_locale_aux l)
                        (C.by [M.rule (T.thm s)])))"
 
+definition "print_transition_def_state' = get_state (\<lambda> pre post _.
+ (Pair o L.map O'.definition)
+ (L.map
+  (let a = \<lambda>f x. Term_app f [x]
+     ; b = \<lambda>s. Term_basic [s]
+     ; heap = \<open>heap\<close> in
+   (\<lambda>(s, _).
+    Definition (Term_rewrite (b (heap @@ \<open>_\<close> @@ s))
+                \<open>=\<close>
+                (a heap (b (print_examp_def_st_locale_name s @@ \<open>.\<close> @@ s))))))
+  [ pre, post ]))"
+
 end