equal
deleted
inserted
replaced
42 (**) |
42 (**) |
43 structure LTool(**): LANGUAGE_TOOLS(**) = |
43 structure LTool(**): LANGUAGE_TOOLS(**) = |
44 struct |
44 struct |
45 (**) |
45 (**) |
46 |
46 |
47 (* prepare program for Lucas-Interpretation *) |
|
48 (* version introduced BEFORE switch to partial_function *) |
|
49 fun prep_program thy str = (TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) str |
|
50 (* version for later switch to partial_function *) |
|
51 fun prep_program thm = (thm |
47 fun prep_program thm = (thm |
52 |> Thm.prop_of |
48 |> Thm.prop_of |
53 |> HOLogic.dest_Trueprop |
49 |> HOLogic.dest_Trueprop |
54 |> Logic.unvarify_global |
50 |> Logic.unvarify_global |
55 |> TermC.inst_abs |
51 |> TermC.inst_abs |
306 | contain_bdv (Rule.Rls_ rls :: rs) = |
302 | contain_bdv (Rule.Rls_ rls :: rs) = |
307 contain_bdv (Rule.get_rules rls) orelse contain_bdv rs |
303 contain_bdv (Rule.get_rules rls) orelse contain_bdv rs |
308 | contain_bdv (r :: _) = |
304 | contain_bdv (r :: _) = |
309 error ("contain_bdv called with [" ^ Rule.id_rule r ^ ",...]"); |
305 error ("contain_bdv called with [" ^ Rule.id_rule r ^ ",...]"); |
310 |
306 |
311 fun rules2scr_Rls thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*) |
307 fun rules2scr_Rls thy rules = |
312 if contain_bdv rules |
308 if contain_bdv rules |
313 then FunID_Term_Bdv $ (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term)) |
309 then FunID_Term_Bdv $ (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term)) |
314 else FunID_Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term)); |
310 else FunID_Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term)); |
315 fun rules2scr_Seq thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*) |
311 fun rules2scr_Seq thy rules = |
316 if contain_bdv rules |
312 if contain_bdv rules |
317 then FunID_Term_Bdv $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term) |
313 then FunID_Term_Bdv $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term) |
318 else FunID_Term $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term); |
314 else FunID_Term $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term); |
319 |
315 |
320 (* prepare the input for an rls for use: |
316 (* prepare the input for an rls for use: |