wenzelm@22905: (* Title: Pure/conv.ML wenzelm@32843: Author: Amine Chaieb, TU Muenchen wenzelm@32843: Author: Makarius wenzelm@22905: wenzelm@22905: Conversions: primitive equality reasoning. wenzelm@22905: *) wenzelm@22905: wenzelm@22937: infix 1 then_conv; wenzelm@22937: infix 0 else_conv; wenzelm@23169: boehmes@30136: signature BASIC_CONV = boehmes@30136: sig boehmes@30136: val then_conv: conv * conv -> conv boehmes@30136: val else_conv: conv * conv -> conv boehmes@30136: end; boehmes@30136: wenzelm@22905: signature CONV = wenzelm@22905: sig boehmes@30136: include BASIC_CONV wenzelm@22905: val no_conv: conv wenzelm@22905: val all_conv: conv wenzelm@22926: val first_conv: conv list -> conv wenzelm@22926: val every_conv: conv list -> conv wenzelm@22937: val try_conv: conv -> conv wenzelm@22937: val repeat_conv: conv -> conv wenzelm@32843: val cache_conv: conv -> conv wenzelm@26571: val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv wenzelm@22926: val combination_conv: conv -> conv -> conv wenzelm@22926: val comb_conv: conv -> conv wenzelm@22926: val arg_conv: conv -> conv wenzelm@22926: val fun_conv: conv -> conv wenzelm@22926: val arg1_conv: conv -> conv wenzelm@22926: val fun2_conv: conv -> conv chaieb@23034: val binop_conv: conv -> conv wenzelm@26571: val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv wenzelm@26571: val implies_conv: conv -> conv -> conv wenzelm@26571: val implies_concl_conv: conv -> conv wenzelm@26571: val rewr_conv: thm -> conv wenzelm@26571: val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv wenzelm@26571: val prems_conv: int -> conv -> conv wenzelm@22905: val concl_conv: int -> conv -> conv wenzelm@22905: val fconv_rule: conv -> thm -> thm wenzelm@23583: val gconv_rule: conv -> int -> thm -> thm wenzelm@22905: end; wenzelm@22905: wenzelm@22905: structure Conv: CONV = wenzelm@22905: struct wenzelm@22905: wenzelm@32843: (* basic conversionals *) wenzelm@22905: wenzelm@22905: fun no_conv _ = raise CTERM ("no conversion", []); wenzelm@22905: val all_conv = Thm.reflexive; wenzelm@22905: wenzelm@22937: fun (cv1 then_conv cv2) ct = wenzelm@22905: let wenzelm@22926: val eq1 = cv1 ct; wenzelm@22926: val eq2 = cv2 (Thm.rhs_of eq1); wenzelm@22905: in wenzelm@23596: if Thm.is_reflexive eq1 then eq2 wenzelm@23596: else if Thm.is_reflexive eq2 then eq1 wenzelm@22905: else Thm.transitive eq1 eq2 wenzelm@22905: end; wenzelm@22905: wenzelm@22937: fun (cv1 else_conv cv2) ct = wenzelm@23583: (cv1 ct wenzelm@23583: handle THM _ => cv2 ct wenzelm@23583: | CTERM _ => cv2 ct wenzelm@23583: | TERM _ => cv2 ct wenzelm@23583: | TYPE _ => cv2 ct); wenzelm@22926: wenzelm@22937: fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv; wenzelm@22937: fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; wenzelm@22926: wenzelm@22937: fun try_conv cv = cv else_conv all_conv; wenzelm@22937: fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; wenzelm@22926: wenzelm@32843: fun cache_conv (cv: conv) = Thm.cterm_cache cv; wenzelm@32843: wenzelm@22905: wenzelm@22905: wenzelm@22926: (** Pure conversions **) wenzelm@22926: wenzelm@22926: (* lambda terms *) wenzelm@22926: wenzelm@24834: fun abs_conv cv ctxt ct = wenzelm@23587: (case Thm.term_of ct of wenzelm@22926: Abs (x, _, _) => wenzelm@23596: let wenzelm@24834: val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt; wenzelm@24834: val (v, ct') = Thm.dest_abs (SOME u) ct; wenzelm@26571: val eq = cv (v, ctxt') ct'; wenzelm@23596: in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end wenzelm@22926: | _ => raise CTERM ("abs_conv", [ct])); wenzelm@22926: wenzelm@22926: fun combination_conv cv1 cv2 ct = wenzelm@22926: let val (ct1, ct2) = Thm.dest_comb ct wenzelm@22926: in Thm.combination (cv1 ct1) (cv2 ct2) end; wenzelm@22926: wenzelm@22926: fun comb_conv cv = combination_conv cv cv; wenzelm@22926: fun arg_conv cv = combination_conv all_conv cv; wenzelm@22926: fun fun_conv cv = combination_conv cv all_conv; wenzelm@22926: wenzelm@22926: val arg1_conv = fun_conv o arg_conv; wenzelm@22926: val fun2_conv = fun_conv o fun_conv; wenzelm@22926: chaieb@23034: fun binop_conv cv = combination_conv (arg_conv cv) cv; wenzelm@22926: wenzelm@23169: wenzelm@26571: (* primitive logic *) wenzelm@26571: wenzelm@26571: fun forall_conv cv ctxt ct = wenzelm@26571: (case Thm.term_of ct of wenzelm@26571: Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct wenzelm@26571: | _ => raise CTERM ("forall_conv", [ct])); wenzelm@26571: wenzelm@26571: fun implies_conv cv1 cv2 ct = wenzelm@26571: (case Thm.term_of ct of wenzelm@26571: Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct wenzelm@26571: | _ => raise CTERM ("implies_conv", [ct])); wenzelm@26571: wenzelm@26571: fun implies_concl_conv cv ct = wenzelm@26571: (case Thm.term_of ct of wenzelm@26571: Const ("==>", _) $ _ $ _ => arg_conv cv ct wenzelm@26571: | _ => raise CTERM ("implies_concl_conv", [ct])); wenzelm@26571: wenzelm@26571: wenzelm@26571: (* single rewrite step, cf. REWR_CONV in HOL *) wenzelm@26571: wenzelm@26571: fun rewr_conv rule ct = wenzelm@26571: let wenzelm@26571: val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule; wenzelm@26571: val lhs = Thm.lhs_of rule1; wenzelm@26571: val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1; wenzelm@26571: in wenzelm@26571: Drule.instantiate (Thm.match (lhs, ct)) rule2 wenzelm@26571: handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct]) wenzelm@26571: end; wenzelm@26571: wenzelm@26571: wenzelm@26571: (* conversions on HHF rules *) wenzelm@22905: wenzelm@22905: (*rewrite B in !!x1 ... xn. B*) wenzelm@26571: fun params_conv n cv ctxt ct = wenzelm@27332: if n <> 0 andalso Logic.is_all (Thm.term_of ct) wenzelm@26571: then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct wenzelm@24834: else cv ctxt ct; wenzelm@22905: wenzelm@26571: (*rewrite the A's in A1 ==> ... ==> An ==> B*) wenzelm@26571: fun prems_conv 0 _ ct = all_conv ct wenzelm@26571: | prems_conv n cv ct = wenzelm@26571: (case try Thm.dest_implies ct of wenzelm@26571: NONE => all_conv ct wenzelm@26571: | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B)); wenzelm@26571: wenzelm@22905: (*rewrite B in A1 ==> ... ==> An ==> B*) wenzelm@22905: fun concl_conv 0 cv ct = cv ct wenzelm@22905: | concl_conv n cv ct = wenzelm@22905: (case try Thm.dest_implies ct of wenzelm@22905: NONE => cv ct wenzelm@22926: | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B)); wenzelm@22905: wenzelm@23596: wenzelm@26571: (* conversions as inference rules *) wenzelm@22905: wenzelm@23596: (*forward conversion, cf. FCONV_RULE in LCF*) wenzelm@23596: fun fconv_rule cv th = wenzelm@23596: let val eq = cv (Thm.cprop_of th) in wenzelm@23596: if Thm.is_reflexive eq then th wenzelm@23596: else Thm.equal_elim eq th wenzelm@23596: end; wenzelm@22905: wenzelm@23596: (*goal conversion*) wenzelm@23596: fun gconv_rule cv i th = wenzelm@23596: (case try (Thm.cprem_of th) i of wenzelm@23596: SOME ct => wenzelm@23596: let val eq = cv ct in wenzelm@23596: if Thm.is_reflexive eq then th wenzelm@23596: else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th wenzelm@23596: end wenzelm@23596: | NONE => raise THM ("gconv_rule", i, [th])); chaieb@23411: wenzelm@22905: end; boehmes@30136: wenzelm@32843: structure Basic_Conv: BASIC_CONV = Conv; wenzelm@32843: open Basic_Conv;