author  wenzelm 
Wed, 05 Jan 2000 11:45:01 +0100  
changeset 8094  62b45a2e6ecb 
parent 7923  895d31b54da5 
child 8109  aca11f954993 
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 

8094  5 
The 'obtain' language element  eliminated existential quantification 
6 
at the level of proof texts. 

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 
8094  35 
def thesis == C x 
7674
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 

8094  42 
TODO: 
43 
 bind terms for goal as well (done?); 

44 
 improve block structure (admit subsequent occurences of 'next') (no?); 

45 
 handle general case (easy??); 

46 
*) 

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

47 

8094  48 
signature OBTAIN_DATA = 
49 
sig 

50 
val that_atts: Proof.context attribute list 

51 
end; 

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

52 

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

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

54 
sig 
8094  55 
val obtain: ((string list * string option) * Comment.text) list 
56 
* ((string * Args.src list * (string * (string list * string list)) list) 

57 
* Comment.text) list > ProofHistory.T > ProofHistory.T 

58 
val obtain_i: ((string list * typ option) * Comment.text) list 

59 
* ((string * Proof.context attribute list * (term * (term list * term list)) list) 

60 
* Comment.text) list > ProofHistory.T > ProofHistory.T 

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

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

62 

8094  63 
functor ObtainFun(Data: OBTAIN_DATA): OBTAIN = 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

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

65 

8094  66 

67 
(** obtain(_i) **) 

68 

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

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

70 

8094  71 
fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state = 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

72 
let 
8094  73 
(*thesis*) 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

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

75 

8094  76 
val parms = Logic.strip_params prop; (* FIXME unused *) 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

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

78 
if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state); 
8094  79 
val hyps = Logic.strip_assums_hyp prop; (* FIXME unused *) 
80 
val concl = Logic.strip_assums_concl prop; 

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

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

82 

8094  83 
(*vars*) 
84 
val (vars_ctxt, vars) = 

85 
foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars); 

86 
val xs = flat (map fst vars); 

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

87 

8094  88 
(*asms*) 
89 
fun prep_asm (ctxt, (name, src, raw_propps)) = 

90 
let 

91 
val atts = map (prep_att (ProofContext.theory_of ctxt)) src; 

92 
val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps); 

93 
in (ctxt', (name, atts, propps)) end; 

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

94 

8094  95 
val (asms_ctxt, asms) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms); 
96 
val asm_props = flat (map (map fst o #3) asms); 

97 
val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt; 

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

98 

8094  99 
(*that_prop*) 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

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

101 
(case Proof.find_free t x of Some (Free a) => Some a  _ => None); 
8094  102 
fun occs_var x = Library.get_first (find_free x) asm_props; 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

103 
val that_prop = 
8094  104 
Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis)); 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

105 

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

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

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

108 
> Proof.next_block 
8094  109 
> Proof.fix_i vars 
110 
> Proof.assume_i asms 

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

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

112 
in 
8094  113 
state 
114 
> Method.proof (Some (Method.Basic (K Method.succeed))) 

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

115 
> Seq.map (fn st => st 
8094  116 
> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, [])) 
117 
> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])] 

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

118 
> Proof.from_facts goal_facts 
8094  119 
> Proof.show_i after_qed "" [] (atomic_thesis, ([], []))) 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

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

121 

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

122 

8094  123 
val obtain = ProofHistory.applys o 
124 
(gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute); 

125 

126 
val obtain_i = ProofHistory.applys o 

127 
(gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I)); 

128 

129 

130 

131 
(** outer syntax **) 

132 

133 
local structure P = OuterParse and K = OuterSyntax.Keyword in 

134 

135 
val obtainP = 

136 
OuterSyntax.command "obtain" "proof textlevel existential quantifier" 

137 
K.prf_asm_goal 

138 
(Scan.optional 

139 
(P.and_list1 (Scan.repeat1 P.name  Scan.option (P.$$$ "::"  P.typ)  P.marg_comment) 

140 
 P.$$$ "in") []  

141 
P.and_list1 ((P.opt_thm_name ":"  Scan.repeat1 P.propp >> P.triple1)  P.marg_comment) 

142 
>> (Toplevel.print oo (Toplevel.proof o obtain))); 

143 

144 
val _ = OuterSyntax.add_parsers [obtainP]; 

145 

146 
end; 

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

147 

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

148 

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

149 
end; 