36 expected (i.e.~on the left-hand side of a code equation) must be |
36 expected (i.e.~on the left-hand side of a code equation) must be |
37 eliminated. This can be accomplished -- as far as possible -- by |
37 eliminated. This can be accomplished -- as far as possible -- by |
38 applying the following transformation rule: |
38 applying the following transformation rule: |
39 *} |
39 *} |
40 |
40 |
41 lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow> |
41 lemma Suc_if_eq: |
42 f n \<equiv> if n = 0 then g else h (n - 1)" |
42 assumes "\<And>n. f (Suc n) \<equiv> h n" |
43 by (rule eq_reflection) (cases n, simp_all) |
43 assumes "f 0 \<equiv> g" |
|
44 shows "f n \<equiv> if n = 0 then g else h (n - 1)" |
|
45 by (rule eq_reflection) (cases n, insert assms, simp_all) |
44 |
46 |
45 text {* |
47 text {* |
46 The rule above is built into a preprocessor that is plugged into |
48 The rule above is built into a preprocessor that is plugged into |
47 the code generator. |
49 the code generator. |
48 *} |
50 *} |
54 let |
56 let |
55 val thy = Proof_Context.theory_of ctxt; |
57 val thy = Proof_Context.theory_of ctxt; |
56 val vname = singleton (Name.variant_list (map fst |
58 val vname = singleton (Name.variant_list (map fst |
57 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
59 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
58 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
60 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
59 fun lhs_of th = snd (Thm.dest_comb |
61 val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o cprop_of; |
60 (fst (Thm.dest_comb (cprop_of th)))); |
62 val rhs_of = snd o Thm.dest_comb o cprop_of; |
61 fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); |
|
62 fun find_vars ct = (case term_of ct of |
63 fun find_vars ct = (case term_of ct of |
63 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
64 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
64 | _ $ _ => |
65 | _ $ _ => |
65 let val (ct1, ct2) = Thm.dest_comb ct |
66 let val (ct1, ct2) = Thm.dest_comb ct |
66 in |
67 in |
67 map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @ |
68 map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @ |
68 map (apfst (Thm.apply ct1)) (find_vars ct2) |
69 map (apfst (Thm.apply ct1)) (find_vars ct2) |
69 end |
70 end |
70 | _ => []); |
71 | _ => []); |
71 val eqs = maps |
72 val eqs = maps |
72 (fn th => map (pair th) (find_vars (lhs_of th))) thms; |
73 (fn thm => map (pair thm) (find_vars (lhs_of thm))) thms; |
73 fun mk_thms (th, (ct, cv')) = |
74 fun mk_thms (thm, (ct, cv')) = |
74 let |
75 let |
75 val th' = |
76 val thm' = |
76 Thm.implies_elim |
77 Thm.implies_elim |
77 (Conv.fconv_rule (Thm.beta_conversion true) |
78 (Conv.fconv_rule (Thm.beta_conversion true) |
78 (Drule.instantiate' |
79 (Drule.instantiate' |
79 [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct), |
80 [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct), |
80 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv'] |
81 SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv'] |
81 @{thm Suc_if_eq})) (Thm.forall_intr cv' th) |
82 @{thm Suc_if_eq})) (Thm.forall_intr cv' thm) |
82 in |
83 in |
83 case map_filter (fn th'' => |
84 case map_filter (fn thm'' => |
84 SOME (th'', singleton |
85 SOME (thm'', singleton |
85 (Variable.trade (K (fn [th'''] => [th''' RS th'])) |
86 (Variable.trade (K (fn [thm'''] => [thm''' RS thm'])) |
86 (Variable.global_thm_context th'')) th'') |
87 (Variable.global_thm_context thm'')) thm'') |
87 handle THM _ => NONE) thms of |
88 handle THM _ => NONE) thms of |
88 [] => NONE |
89 [] => NONE |
89 | thps => |
90 | thmps => |
90 let val (ths1, ths2) = split_list thps |
91 let val (thms1, thms2) = split_list thmps |
91 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end |
92 in SOME (subtract Thm.eq_thm (thm :: thms1) thms @ thms2) end |
92 end |
93 end |
93 in get_first mk_thms eqs end; |
94 in get_first mk_thms eqs end; |
94 |
95 |
95 fun eqn_suc_base_preproc thy thms = |
96 fun eqn_suc_base_preproc thy thms = |
96 let |
97 let |