src/HOL/Tools/datatype_realizer.ML
changeset 13708 a3a410782c95
parent 13656 58bb243dbafb
child 13725 12404b452034
equal deleted inserted replaced
13707:55670a70a5f9 13708:a3a410782c95
    24      else [[]];
    24      else [[]];
    25 
    25 
    26 fun forall_intr_prf (t, prf) =
    26 fun forall_intr_prf (t, prf) =
    27   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    27   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    28   in Abst (a, Some T, Proofterm.prf_abstract_over t prf) end;
    28   in Abst (a, Some T, Proofterm.prf_abstract_over t prf) end;
    29 
       
    30 fun prove_goal' sg p f =
       
    31   let
       
    32     val (As, B) = Logic.strip_horn p;
       
    33     val cAs = map (cterm_of sg) As;
       
    34     val asms = map (norm_hhf_rule o assume) cAs;
       
    35     fun check thm = if nprems_of thm > 0 then
       
    36       error "prove_goal': unsolved goals" else thm
       
    37   in
       
    38     standard (implies_intr_list cAs
       
    39       (check (Seq.hd (EVERY (f asms) (trivial (cterm_of sg B))))))
       
    40   end;
       
    41 
    29 
    42 fun prf_of thm =
    30 fun prf_of thm =
    43   let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    31   let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    44   in Reconstruct.reconstruct_proof sign prop prf end;
    32   in Reconstruct.reconstruct_proof sign prop prf end;
    45 
    33 
   127           (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
   115           (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
   128     val cert = cterm_of sg;
   116     val cert = cterm_of sg;
   129     val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
   117     val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
   130       (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
   118       (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
   131 
   119 
   132     val thm = prove_goal' sg (Logic.list_implies (prems, concl))
   120     val thm = simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
   133       (fn prems =>
   121       (fn prems =>
   134          [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
   122          [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
   135           rtac (cterm_instantiate inst induction) 1,
   123           rtac (cterm_instantiate inst induction) 1,
   136           ALLGOALS ObjectLogic.atomize_tac,
   124           ALLGOALS ObjectLogic.atomize_tac,
   137           rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
   125           rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),