94 val t_rhs = lambda t_k proto_t_rhs; |
94 val t_rhs = lambda t_k proto_t_rhs; |
95 val eqs0 = [subst_v @{term "0::natural"} eq, |
95 val eqs0 = [subst_v @{term "0::natural"} eq, |
96 subst_v (@{const Code_Numeral.Suc} $ t_k) eq]; |
96 subst_v (@{const Code_Numeral.Suc} $ t_k) eq]; |
97 val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0; |
97 val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0; |
98 val ((_, (_, eqs2)), lthy') = lthy |
98 val ((_, (_, eqs2)), lthy') = lthy |
99 |> BNF_LFP_Compat.add_primrec_simple |
99 |> BNF_LFP_Compat.primrec_simple |
100 [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1; |
100 [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1; |
101 val cT_random_aux = inst pt_random_aux; |
101 val cT_random_aux = inst pt_random_aux; |
102 val cT_rhs = inst pt_rhs; |
102 val cT_rhs = inst pt_rhs; |
103 val rule = @{thm random_aux_rec} |
103 val rule = @{thm random_aux_rec} |
104 |> Drule.instantiate_normalize |
104 |> Drule.instantiate_normalize |