equal
deleted
inserted
replaced
65 (* the lucas-interpreter LI requires programs in this specific format *) |
65 (* the lucas-interpreter LI requires programs in this specific format *) |
66 fun prep_program thm = (thm |
66 fun prep_program thm = (thm |
67 |> Thm.prop_of |
67 |> Thm.prop_of |
68 |> HOLogic.dest_Trueprop |
68 |> HOLogic.dest_Trueprop |
69 |> Logic.unvarify_global |
69 |> Logic.unvarify_global |
70 |> TermC.inst_abs |
70 |> TermC.inst_abs) |
71 |> ThmC_Def.num_to_Free (*for numbers in the program*)) |
|
72 handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm]) |
71 handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm]) |
73 |
72 |
74 (* get identifier of partial_function *) |
73 (* get identifier of partial_function *) |
75 fun get_fun_id (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ fun_and_args $ _) = |
74 fun get_fun_id (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ fun_and_args $ _) = |
76 fun_and_args |> strip_comb |> fst |> dest_Const |
75 fun_and_args |> strip_comb |> fst |> dest_Const |