author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 54742  7a86358a3c0b 
child 58826  2ed2eaabe3df 
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 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

4 
Combine two case rules into a single one. 
41826
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 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

16 
end 
41826
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 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

21 
(*instantiate the conclusion of thm2 to the one of thm1*) 
41826
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 
(* 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

35 
Return list of prems, where loose bounds have been replaced by frees. 
41826
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) 
48902
44a6967240b7
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents:
45375
diff
changeset

51 
val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1) 
44a6967240b7
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents:
45375
diff
changeset

52 
val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2) 
41826
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) 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

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

62 

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

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

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

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

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

67 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

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

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

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

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

72 
in 
52732  73 
rtac (thm1 OF p_cons1) 
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

74 
THEN' EVERY' (map (fn p => 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

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

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

77 

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

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

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

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

81 
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

82 
in 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

83 
Goal.prove ctxt' [] (flat prems_rich) concl 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

84 
(fn {context = ctxt'', prems} => 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

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

86 
> singleton (Variable.export ctxt' ctxt) 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

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

88 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

89 
fun annotation_rule thm1 thm2 = 
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

90 
let 
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42361
diff
changeset

91 
val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1) 
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
42361
diff
changeset

92 
val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2) 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

93 
val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2 
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

94 
in 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

95 
Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2)) 
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

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

97 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

98 
fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2)) 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

99 

41826
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 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

102 
> annotation_rule thm1 thm2 
41826
18d4d2b60016
introduce attribute case_prod for combining case rules
noschinl
parents:
diff
changeset

103 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

104 

7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

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

106 

41883  107 
val case_prod_attr = 
108 
let 

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

109 
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

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

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

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

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

114 

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

115 
val setup = 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

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

117 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44045
diff
changeset

118 
end 