TFL/tfl.sml
changeset 3379 7091ffa99c93
parent 3353 9112a2efb9a3
child 3387 6f2eaa0ce04b
equal deleted inserted replaced
3378:11f4884a071a 3379:7091ffa99c93
   424      val corollary' = R.UNDISCH corollary  (* put WF R on assums *)
   424      val corollary' = R.UNDISCH corollary  (* put WF R on assums *)
   425      val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
   425      val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
   426      val (case_rewrites,context_congs) = extraction_thms theory
   426      val (case_rewrites,context_congs) = extraction_thms theory
   427      val corollaries' = map(R.simplify case_rewrites) corollaries
   427      val corollaries' = map(R.simplify case_rewrites) corollaries
   428      fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
   428      fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
   429                          {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
   429                          {cut_lemma = R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
   430                          congs = context_congs,
   430 			  congs = context_congs,
   431                             th = th}
   431 			  th = th}
   432      val (rules, TCs) = ListPair.unzip (map xtract corollaries')
   432      val (rules, TCs) = ListPair.unzip (map xtract corollaries')
   433      val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
   433      val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
   434      val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
   434      val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
   435      val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   435      val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   436  in
   436  in
   462      val R1 = S.rand WFR
   462      val R1 = S.rand WFR
   463      val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   463      val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   464      val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
   464      val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
   465      val corollaries' = map (R.simplify case_rewrites) corollaries
   465      val corollaries' = map (R.simplify case_rewrites) corollaries
   466      fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
   466      fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
   467                         {thms = [(R.ISPECL o map tych)[f,R1] Thms.CUT_LEMMA], 
   467                         {cut_lemma = R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
   468                         congs = context_congs,
   468 			 congs = context_congs,
   469                           th  = th}
   469 			 th  = th}
   470  in {proto_def=proto_def, 
   470  in {proto_def=proto_def, 
   471      WFR=WFR, 
   471      WFR=WFR, 
   472      pats=pats,
   472      pats=pats,
   473      extracta = map extract corollaries'}
   473      extracta = map extract corollaries'}
   474  end;
   474  end;