author  wenzelm 
Sat, 09 Jul 2011 21:53:27 +0200  
changeset 43721  fad8634cee62 
parent 42361  23f352990944 
child 44045  2814ff2a6e3e 
permissions  rwrr 
41883  1 
(* Title: Tools/case_product.ML 
2 
Author: Lars Noschinski, TU Muenchen 

41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

3 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

4 
Combines two case rules into a single one. 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

5 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

6 
Assumes that the theorems are of the form 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

7 
"[ C1; ...; Cm; A1 ==> P; ...; An ==> P ] ==> P" 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

8 
where m is given by the "consumes" attribute of the theorem. 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

9 
*) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

10 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

11 
signature CASE_PRODUCT = 
41883  12 
sig 
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

13 
val combine: Proof.context > thm > thm > thm 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

14 
val combine_annotated: Proof.context > thm > thm > thm 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

15 
val setup: theory > theory 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

16 
end; 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

17 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

18 
structure Case_Product: CASE_PRODUCT = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

19 
struct 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

20 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

21 
(*Instantiates the conclusion of thm2 to the one of thm1.*) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

22 
fun inst_concl thm1 thm2 = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

23 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

24 
val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

25 
in Thm.instantiate (Thm.match (cconcl_of thm2, cconcl_of thm1)) thm2 end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

26 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

27 
fun inst_thms thm1 thm2 ctxt = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

28 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

29 
val import = yield_singleton (apfst snd oo Variable.import true) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

30 
val (i_thm1, ctxt') = import thm1 ctxt 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

31 
val (i_thm2, ctxt'') = import (inst_concl i_thm1 thm2) ctxt' 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

32 
in ((i_thm1, i_thm2), ctxt'') end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

33 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

34 
(* 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

35 
Returns list of prems, where loose bounds have been replaced by frees. 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

36 
FIXME: Focus 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

37 
*) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

38 
fun free_prems t ctxt = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

39 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

40 
val bs = Term.strip_all_vars t 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

41 
val (names, ctxt') = Variable.variant_fixes (map fst bs) ctxt 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

42 
val subst = map Free (names ~~ map snd bs) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

43 
val t' = map (Term.subst_bounds o pair (rev subst)) (Logic.strip_assums_hyp t) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

44 
in ((t', subst), ctxt') end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

45 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

46 
fun build_concl_prems thm1 thm2 ctxt = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

47 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

48 
val concl = Thm.concl_of thm1 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

49 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

50 
fun is_consumes t = not (Logic.strip_assums_concl t aconv concl) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

51 
val (p_cons1, p_cases1) = chop_while is_consumes (Thm.prems_of thm1) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

52 
val (p_cons2, p_cases2) = chop_while is_consumes (Thm.prems_of thm2) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

53 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

54 
val p_cases_prod = map (fn p1 => map (fn p2 => 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

55 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

56 
val (((t1, subst1), (t2, subst2)), _) = ctxt 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

57 
> free_prems p1 >> free_prems p2 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

58 
in 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

59 
Logic.list_implies (t1 @ t2, concl) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

60 
> fold_rev Logic.all (subst1 @ subst2) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

61 
end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

62 
) p_cases2) p_cases1 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

63 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

64 
val prems = p_cons1 :: p_cons2 :: p_cases_prod 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

65 
in 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

66 
(concl, prems) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

67 
end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

68 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

69 
fun case_product_tac prems struc thm1 thm2 = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

70 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

71 
val (p_cons1 :: p_cons2 :: premss) = unflat struc prems 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

72 
val thm2' = thm2 OF p_cons2 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

73 
in 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

74 
(Tactic.rtac (thm1 OF p_cons1) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

75 
THEN' EVERY' (map (fn p => 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

76 
Tactic.rtac thm2' 
42361  77 
THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss) 
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

78 
) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

79 
end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

80 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

81 
fun combine ctxt thm1 thm2 = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

82 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

83 
val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

84 
val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt' 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

85 
in 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

86 
Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} => 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

87 
case_product_tac prems prems_rich i_thm1 i_thm2 1) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

88 
> singleton (Variable.export ctxt' ctxt) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

89 
end; 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

90 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

91 
fun annotation thm1 thm2 = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

92 
let 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

93 
val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

94 
val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

95 
val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

96 
in 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

97 
Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

98 
end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

99 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

100 
fun combine_annotated ctxt thm1 thm2 = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

101 
combine ctxt thm1 thm2 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

102 
> snd o annotation thm1 thm2 o pair (Context.Proof ctxt) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

103 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

104 
(* Attribute setup *) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

105 

41883  106 
val case_prod_attr = 
107 
let 

41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

108 
fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

109 
in 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

110 
Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm => 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

111 
combine_list (Context.proof_of ctxt) thms thm)) 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

112 
end 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

113 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

114 
val setup = 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

115 
Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules" 
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

116 

18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

117 
end; 