author  wenzelm 
Sun, 30 Jul 2000 12:54:07 +0200  
changeset 9468  9adbcf6375c1 
parent 9293  3da2533e0a61 
child 9481  b16624f1ea38 
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 
8807  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

5 

8543  6 
The 'obtain' language element  generalized existence at the level of 
7 
proof texts. 

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

8 

9468  9 
<chain_facts> 
10 
obtain x where "P x" <proof> == 

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

11 

9468  12 
{ 
13 
fix thesis 

14 
assume that: "!!x. P x ==> thesis" 

15 
<chain_facts> have thesis <proof> 

16 
} 

17 
fix x assm(obtained) "P x" 

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

18 

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

20 

8094  21 
signature OBTAIN_DATA = 
22 
sig 

9468  23 
val atomic_thesis: string > term 
8094  24 
val that_atts: Proof.context attribute list 
25 
end; 

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

26 

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

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

28 
sig 
8094  29 
val obtain: ((string list * string option) * Comment.text) list 
30 
* ((string * Args.src list * (string * (string list * string list)) list) 

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

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

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

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

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

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

36 

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

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

39 

8094  40 

9468  41 
(** export_obtained **) 
42 

43 
fun disch_obtained state parms rule cprops thm = 

44 
let 

45 
val {sign, prop, maxidx, ...} = Thm.rep_thm thm; 

46 
val cparms = map (Thm.cterm_of sign) parms; 

47 

48 
val thm' = thm 

49 
> Drule.implies_intr_list cprops 

50 
> Drule.forall_intr_list cparms 

51 
> Drule.forall_elim_vars (maxidx + 1); 

52 
val elim_tacs = replicate (length cprops) Proof.hard_asm_tac; 

53 

54 
val concl = Logic.strip_assums_concl prop; 

55 
val bads = parms inter (Term.term_frees concl); 

56 
in 

57 
if not (null bads) then 

58 
raise Proof.STATE ("Result contains illegal parameters: " ^ 

59 
space_implode " " (map (Sign.string_of_term sign) bads), state) 

60 
else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then 

61 
raise Proof.STATE ("Conclusion of result is not an objectlogic judgment", state) 

62 
else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule 

63 
end; 

64 

65 
fun export_obtained state parms rule = 

66 
(disch_obtained state parms rule, fn _ => fn _ => []); 

67 

68 

69 

8094  70 
(** obtain(_i) **) 
71 

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

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

73 

8094  74 
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

75 
let 
9468  76 
val _ = Proof.assert_forward_or_chain state; 
77 
val chain_facts = if Proof.is_chain state then Proof.the_facts state else []; 

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

78 

8543  79 
(*obtain vars*) 
8094  80 
val (vars_ctxt, vars) = 
81 
foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars); 

82 
val xs = flat (map fst vars); 

9468  83 
val thesisN = Term.variant xs AutoBind.thesisN; 
9293  84 

9468  85 
val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]); 
9293  86 
fun bind_propp (prop, (pats1, pats2)) = 
87 
(bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2)); 

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

88 

8543  89 
(*obtain asms*) 
8094  90 
fun prep_asm (ctxt, (name, src, raw_propps)) = 
91 
let 

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

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

9293  94 
in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end; 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

95 

9293  96 
val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms); 
97 
val (asms, asm_propss) = Library.split_list asms_result; 

98 
val asm_props = flat asm_propss; 

8094  99 
val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt; 
7674
99305245f6bd
The 'obtain' language element  achieves (eliminated) existential
wenzelm
parents:
diff
changeset

100 

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

102 
fun find_free x t = 
8614  103 
(case ProofContext.find_free t x of Some (Free a) => Some a  _ => None); 
8094  104 
fun occs_var x = Library.get_first (find_free x) asm_props; 
9468  105 
val xs' = mapfilter occs_var xs; 
106 
val parms = map (bind_skolem o Free) xs'; 

107 

108 
val bound_thesis = bind_skolem (Data.atomic_thesis thesisN); 

109 
val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis)); 

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

110 

9468  111 
fun after_qed st = st 
112 
> Proof.end_block 

113 
> Seq.map (fn st' => st' 

114 
> Proof.fix_i vars 

115 
> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms); 

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

116 
in 
8094  117 
state 
9468  118 
> Proof.enter_forward 
119 
> Proof.begin_block 

120 
> Proof.fix_i [([thesisN], None)] 

121 
> Proof.assume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])] 

122 
> Proof.from_facts chain_facts 

123 
> Proof.have_i after_qed "" [] (bound_thesis, ([], [])) 

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

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

125 

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

126 

9468  127 
val obtain = ProofHistory.apply o 
8094  128 
(gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute); 
129 

9468  130 
val obtain_i = ProofHistory.apply o 
8094  131 
(gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I)); 
132 

133 

134 

135 
(** outer syntax **) 

136 

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

138 

139 
val obtainP = 

8543  140 
OuterSyntax.command "obtain" "generalized existence" 
8094  141 
K.prf_asm_goal 
142 
(Scan.optional 

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

8109  144 
 P.$$$ "where") []  
8094  145 
P.and_list1 ((P.opt_thm_name ":"  Scan.repeat1 P.propp >> P.triple1)  P.marg_comment) 
146 
>> (Toplevel.print oo (Toplevel.proof o obtain))); 

147 

8109  148 
val _ = OuterSyntax.add_keywords ["where"]; 
8094  149 
val _ = OuterSyntax.add_parsers [obtainP]; 
150 

151 
end; 

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

152 

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

153 
end; 