author  wenzelm 
Fri, 22 Oct 1999 21:48:50 +0200  
changeset 7923  895d31b54da5 
parent 7677  de2e468a42c8 
child 8094  62b45a2e6ecb 
permissions  rwrr 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Isar/obtain.ML 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

4 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

5 
The 'obtain' language element  achieves (eliminated) existential 
7677  6 
quantification at proof command level. 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

7 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

8 
The common case: 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

9 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

10 
<goal_facts> 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

11 
have/show C 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

12 
obtain a in P[a] <proof> == 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

13 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

14 
<goal_facts> 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

15 
have/show C 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

16 
proof succeed 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

17 
def thesis == C 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

18 
presume that: !!a. P a ==> thesis 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

19 
from goal_facts show thesis <proof> 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

20 
next 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

21 
fix a 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

22 
assume P a 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

23 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

24 
The general case: 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

25 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

26 
<goal_facts> 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

27 
have/show !!x. G x ==> C x 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

28 
obtain a in P[a] <proof> == 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

29 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

30 
<goal_facts> 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

31 
have/show !!x. G x ==> C x 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

32 
proof succeed 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

33 
fix x 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

34 
assume antecedent: G x 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

35 
def thesis == ?thesis_prop x 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

36 
presume that: !!a. P a ==> thesis 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

37 
from goal_facts show thesis <proof> 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

38 
next 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

39 
fix a 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

40 
assume P a 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

41 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

42 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

43 
TODO: 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

44 
 handle general case; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

45 
*) 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

46 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

47 
signature OBTAIN = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

48 
sig 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

49 
val obtain: (string list * string option) list 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

50 
> (string * Proof.context attribute list * (string * (string list * string list)) list) list 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

51 
> Proof.state > Proof.state Seq.seq 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

52 
val obtain_i: (string list * typ option) list 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

53 
> (string * Proof.context attribute list * (term * (term list * term list)) list) list 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

54 
> Proof.state > Proof.state Seq.seq 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

55 
end; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

56 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

57 
structure Obtain: OBTAIN = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

58 
struct 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

59 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

60 
val thatN = "that"; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

61 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

62 
fun gen_obtain prep_typ prep_prop fix assume raw_vars raw_asms state = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

63 
let 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

64 
val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state); 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

65 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

66 
val parms = Logic.strip_params prop; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

67 
val hyps = Logic.strip_assums_hyp prop; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

68 
val concl = Logic.strip_assums_concl prop; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

69 
val _ = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

70 
if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state); 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

71 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

72 
val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

73 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

74 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

75 
fun fix_vars (ctxt, (xs, raw_T)) = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

76 
let 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

77 
val T = apsome (prep_typ ctxt) raw_T; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

78 
val ctxt' = ProofContext.fix_i [(xs, T)] ctxt; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

79 
in (ctxt', map (ProofContext.cert_skolem ctxt') xs) end; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

80 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

81 
fun prep_asm (ctxt, (_, _, raw_propps)) = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

82 
let val ts = map (prep_prop ctxt) (map fst raw_propps); 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

83 
in (ctxt > ProofContext.declare_terms ts, ts) end; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

84 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

85 
val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars)); 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

86 
val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms)); 
7923  87 
val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt; 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

88 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

89 
fun find_free x t = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

90 
(case Proof.find_free t x of Some (Free a) => Some a  _ => None); 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

91 
fun find_skolem x = Library.get_first (find_free x) asms; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

92 
val skolemTs = mapfilter find_skolem skolems; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

93 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

94 
val that_prop = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

95 
Logic.list_rename_params (map (Syntax.dest_skolem o #1) skolemTs, 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

96 
Term.list_all_free (skolemTs, Logic.list_implies (asms, atomic_thesis))); 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

97 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

98 
val presume_stateq = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

99 
state 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

100 
> Method.proof (Some (Method.Basic (K Method.succeed))) 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

101 
> Seq.map (fn st => st 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

102 
> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, [])) 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

103 
> Proof.presume_i [(thatN, [], [(that_prop, ([], []))])]); 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

104 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

105 
fun after_qed st = 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

106 
st 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

107 
> Proof.next_block 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

108 
> fix raw_vars (*prepared twice!*) 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

109 
> assume raw_asms (*prepared twice!*) 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

110 
> Seq.single; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

111 
in 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

112 
presume_stateq 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

113 
> Seq.map (fn st => st 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

114 
> Proof.from_facts goal_facts 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

115 
> Proof.show_i after_qed "" [] (atomic_thesis, ([], [])) 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

116 
> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts st))))) 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

117 
> Seq.flat 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

118 
end; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

119 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

120 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

121 
val obtain = gen_obtain ProofContext.read_typ ProofContext.read_prop Proof.fix Proof.assume; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

122 
val obtain_i = gen_obtain ProofContext.cert_typ ProofContext.cert_prop Proof.fix_i Proof.assume_i; 
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

123 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

124 

99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

125 
end; 