src/Pure/drule.ML
changeset 10767 8fa4aafa7314
parent 10667 75a1c9575edb
child 10815 dd5fb02ff872
equal deleted inserted replaced
10766:ace2ba2d4fd1 10767:8fa4aafa7314
   121 
   121 
   122 (*dest_implies for cterms. Note T=prop below*)
   122 (*dest_implies for cterms. Note T=prop below*)
   123 fun dest_implies ct =
   123 fun dest_implies ct =
   124     case term_of ct of
   124     case term_of ct of
   125         (Const("==>", _) $ _ $ _) =>
   125         (Const("==>", _) $ _ $ _) =>
   126             let val (ct1,ct2) = dest_comb ct
   126             let val (ct1,ct2) = Thm.dest_comb ct
   127             in  (#2 (dest_comb ct1), ct2)  end
   127             in  (#2 (Thm.dest_comb ct1), ct2)  end
   128       | _ => raise TERM ("dest_implies", [term_of ct]) ;
   128       | _ => raise TERM ("dest_implies", [term_of ct]) ;
   129 
   129 
   130 fun dest_equals ct =
   130 fun dest_equals ct =
   131     case term_of ct of
   131     case term_of ct of
   132         (Const("==", _) $ _ $ _) =>
   132         (Const("==", _) $ _ $ _) =>
   133             let val (ct1,ct2) = dest_comb ct
   133             let val (ct1,ct2) = Thm.dest_comb ct
   134             in  (#2 (dest_comb ct1), ct2)  end
   134             in  (#2 (Thm.dest_comb ct1), ct2)  end
   135       | _ => raise TERM ("dest_equals", [term_of ct]) ;
   135       | _ => raise TERM ("dest_equals", [term_of ct]) ;
   136 
   136 
   137 
   137 
   138 (*Discard flexflex pairs; return a cterm*)
   138 (*Discard flexflex pairs; return a cterm*)
   139 fun skip_flexpairs ct =
   139 fun skip_flexpairs ct =
   149     handle TERM _ => [];
   149     handle TERM _ => [];
   150 
   150 
   151 (* A1==>...An==>B  goes to B, where B is not an implication *)
   151 (* A1==>...An==>B  goes to B, where B is not an implication *)
   152 fun strip_imp_concl ct =
   152 fun strip_imp_concl ct =
   153     case term_of ct of (Const("==>", _) $ _ $ _) =>
   153     case term_of ct of (Const("==>", _) $ _ $ _) =>
   154         strip_imp_concl (#2 (dest_comb ct))
   154         strip_imp_concl (#2 (Thm.dest_comb ct))
   155   | _ => ct;
   155   | _ => ct;
   156 
   156 
   157 (*The premises of a theorem, as a cterm list*)
   157 (*The premises of a theorem, as a cterm list*)
   158 val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
   158 val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
   159 
   159 
   160 val proto_sign = Theory.sign_of ProtoPure.thy;
   160 val proto_sign = Theory.sign_of ProtoPure.thy;
   161 
   161 
   162 val implies = cterm_of proto_sign Term.implies;
   162 val implies = cterm_of proto_sign Term.implies;
   163 
   163 
   164 (*cterm version of mk_implies*)
   164 (*cterm version of mk_implies*)
   165 fun mk_implies(A,B) = capply (capply implies A) B;
   165 fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B;
   166 
   166 
   167 (*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
   167 (*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
   168 fun list_implies([], B) = B
   168 fun list_implies([], B) = B
   169   | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
   169   | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
   170 
   170