author | dixon |
Mon, 18 Oct 2004 13:40:45 +0200 | |
changeset 15250 | 217bececa2bd |
parent 15150 | c7af682b9ee5 |
permissions | -rw-r--r-- |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
2 |
(* Title: sys/isand.ML |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
3 |
Author: Lucas Dixon, University of Edinburgh |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
4 |
lucas.dixon@ed.ac.uk |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
5 |
Date: 6 Aug 2004 |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
6 |
*) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
7 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
8 |
(* DESCRIPTION: |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
9 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
10 |
Natural Deduction tools |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
11 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
12 |
For working with Isbaelle theorem in a natural detuction style, |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
13 |
ie, not having to deal with meta level quantified varaibles, |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
14 |
instead, we work with newly introduced frees, and hide the |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
15 |
"all"'s, exporting results from theorems proved with the frees, to |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
16 |
solve the all cases of the previous goal. |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
17 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
18 |
Note: A nice idea: allow esxporting to solve any subgoal, thus |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
19 |
allowing the interleaving of proof, or provide a structure for the |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
20 |
ordering of proof, thus allowing proof attempts in parrelle, but |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
21 |
recording the order to apply things in. |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
22 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
23 |
debugging tools: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
24 |
fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
25 |
fun asm_read s = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
26 |
(assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
27 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
28 |
THINK: are we really ok with our varify name w.r.t the prop - do |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
29 |
we alos need to avoid named in the hidden hyps? |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
30 |
|
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
31 |
*) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
32 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
33 |
structure IsaND = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
34 |
struct |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
35 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
36 |
(* Solve *some* subgoal of "th" directly by "sol" *) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
37 |
(* Note: this is probably what Markus ment to do upon export of a |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
38 |
"show" but maybe he used RS/rtac instead, which would wrongly lead to |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
39 |
failing if there are premices to the shown goal. *) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
40 |
fun solve_with sol th = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
41 |
let fun solvei 0 = Seq.empty |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
42 |
| solvei i = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
43 |
Seq.append (bicompose false (false,sol,0) i th, |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
44 |
solvei (i - 1)) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
45 |
in |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
46 |
solvei (Thm.nprems_of th) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
47 |
end; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
48 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
49 |
|
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
50 |
(* Given ctertmify function, (string,type) pairs capturing the free |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
51 |
vars that need to be allified in the assumption, and a theorem with |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
52 |
assumptions possibly containing the free vars, then we give back the |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
53 |
assumptions allified as hidden hyps. *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
54 |
(* |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
55 |
Given: vs |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
56 |
th: A vs ==> B vs |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
57 |
Results in: "B vs" [!!x. A x] |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
58 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
59 |
fun allify_conditions ctermify Ts th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
60 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
61 |
val premts = Thm.prems_of th |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
62 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
63 |
fun allify_prem_var (vt as (n,ty),t) = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
64 |
(Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
65 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
66 |
fun allify_prem Ts p = foldr allify_prem_var (Ts, p) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
67 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
68 |
val cTs = map (ctermify o Free) Ts |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
69 |
val cterm_asms = map (ctermify o allify_prem Ts) premts |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
70 |
val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
71 |
in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
72 |
(foldl (fn (x,y) => y RS x) (th, allifyied_asm_thms), cterm_asms) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
73 |
end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
74 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
75 |
fun allify_conditions' Ts th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
76 |
allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
77 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
78 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
79 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
80 |
(* change schematic vars to fresh free vars *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
81 |
fun fix_vars_to_frees th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
82 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
83 |
val ctermify = Thm.cterm_of (Thm.sign_of_thm th) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
84 |
val prop = Thm.prop_of th |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
85 |
val vars = map Term.dest_Var (Term.term_vars prop) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
86 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
87 |
val names = Term.add_term_names (prop, []) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
88 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
89 |
val (insts,names2) = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
90 |
foldl (fn ((insts,names),v as ((n,i),ty)) => |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
91 |
let val n2 = Term.variant names n in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
92 |
((ctermify (Var v), ctermify (Free(n2,ty))) :: insts, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
93 |
n2 :: names) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
94 |
end) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
95 |
(([],names), vars) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
96 |
in (insts, Thm.instantiate ([], insts) th) end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
97 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
98 |
(* *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
99 |
(* |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
100 |
val th = Thm.freezeT (topthm()); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
101 |
val (insts, th') = fix_vars_to_frees th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
102 |
val Ts = map (Term.dest_Free o Thm.term_of o snd) insts; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
103 |
allify_conditions' Ts th'; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
104 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
105 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
106 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
107 |
(* datatype to capture an exported result, ie a fix or assume. *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
108 |
datatype export = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
109 |
export of {fixes : Thm.cterm list, (* fixed vars *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
110 |
assumes : Thm.cterm list, (* hidden hyps/assumed prems *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
111 |
sgid : int, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
112 |
gth : Thm.thm}; (* subgoal/goalthm *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
113 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
114 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
115 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
116 |
(* export the result of the new goal thm, ie if we reduced teh |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
117 |
subgoal, then we get a new reduced subtgoal with the old |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
118 |
all-quantified variables *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
119 |
local |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
120 |
fun allify_term (v, t) = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
121 |
let val vt = #t (Thm.rep_cterm v) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
122 |
val (n,ty) = Term.dest_Free vt |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
123 |
in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
124 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
125 |
fun allify_for_sg_term ctermify vs t = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
126 |
let val t_alls = foldr allify_term (vs,t); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
127 |
val ct_alls = ctermify t_alls; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
128 |
in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
129 |
(ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
130 |
end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
131 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
132 |
fun lookupfree vs vn = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
133 |
case Library.find_first (fn (n,ty) => n = vn) vs of |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
134 |
None => raise ERROR_MESSAGE ("prepare_goal_export:lookupfree: " |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
135 |
^ vn ^ " does not occur in the term") |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
136 |
| Some x => x; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
137 |
in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
138 |
fun export_back (export {fixes = vs, assumes = hprems, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
139 |
sgid = i, gth = gth}) newth = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
140 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
141 |
val sgn = Thm.sign_of_thm newth; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
142 |
val ctermify = Thm.cterm_of sgn; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
143 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
144 |
val sgs = prems_of newth; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
145 |
val (sgallcts, sgthms) = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
146 |
Library.split_list (map (allify_for_sg_term ctermify vs) sgs); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
147 |
val minimal_newth = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
148 |
(foldl (fn ( newth', sgthm) => |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
149 |
Drule.compose_single (sgthm, 1, newth')) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
150 |
(newth, sgthms)); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
151 |
val allified_newth = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
152 |
minimal_newth |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
153 |
|> Drule.implies_intr_list hprems |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
154 |
|> Drule.forall_intr_list vs |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
155 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
156 |
val newth' = Drule.implies_intr_list sgallcts allified_newth |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
157 |
in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
158 |
bicompose false (false, newth', (length sgallcts)) i gth |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
159 |
end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
160 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
161 |
(* given a thm of the form: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
162 |
P1 vs; ...; Pn vs ==> Goal(C vs) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
163 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
164 |
Gives back: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
165 |
n, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
166 |
[| !! vs. P1 vs; !! vs. Pn vs |] |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
167 |
==> !! C vs |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
168 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
169 |
(* note: C may contain further premices etc |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
170 |
Note that cterms is the assumed facts, ie prems of "P1" that are |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
171 |
reintroduced. |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
172 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
173 |
fun prepare_goal_export (vs, cterms) th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
174 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
175 |
val sgn = Thm.sign_of_thm th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
176 |
val ctermify = Thm.cterm_of sgn; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
177 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
178 |
val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th)) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
179 |
val cfrees = map (ctermify o Free o lookupfree allfrees) vs |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
180 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
181 |
val sgs = prems_of th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
182 |
val (sgallcts, sgthms) = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
183 |
Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
184 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
185 |
val minimal_th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
186 |
(foldl (fn ( th', sgthm) => |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
187 |
Drule.compose_single (sgthm, 1, th')) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
188 |
(th, sgthms)) RS Drule.rev_triv_goal; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
189 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
190 |
val allified_th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
191 |
minimal_th |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
192 |
|> Drule.implies_intr_list cterms |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
193 |
|> Drule.forall_intr_list cfrees |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
194 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
195 |
val th' = Drule.implies_intr_list sgallcts allified_th |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
196 |
in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
197 |
((length sgallcts), th') |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
198 |
end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
199 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
200 |
end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
201 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
202 |
(* val exports_back = foldr (uncurry export_to_sg); *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
203 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
204 |
(* test with: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
205 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
206 |
fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
207 |
fun asm_read s = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
208 |
(assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
209 |
use_thy "theories/dbg2"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
210 |
Goal "!! x :: nat. [| A x; B x; C x; D x |] ==> ((P1 x & P2 x) & P3 x)"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
211 |
by (rtac conjI 1); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
212 |
by (rtac conjI 1); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
213 |
val th = topthm(); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
214 |
val i = 1; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
215 |
val (gthi, exp) = IsaND.fix_alls i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
216 |
val [th'] = Seq.list_of (rtac (thm "p321") 1 gthi); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
217 |
val oldthewth = Seq.list_of (IsaND.export_back exp th'); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
218 |
or |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
219 |
val [th'] = Seq.list_of (RWStepTac.rwstep_tac (thms "aa2") 1 gthi); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
220 |
val oldthewth = Seq.list_of (IsaND.export_back exp th'); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
221 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
222 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
223 |
val th = topthm(); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
224 |
val i = 1; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
225 |
val (goalth, exp1) = IsaND.fix_alls' i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
226 |
val (newth, exp2) = IsaND.hide_other_goals 2 goalth; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
227 |
val oldthewth = Seq.list_of (IsaND.export_back exp2 newth); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
228 |
val (export {fixes = vs, assumes = hprems, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
229 |
sgid = i, gth = gth}) = exp2; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
230 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
231 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
232 |
Goal "!! x y. P (x + (Suc y)) ==> Z x y ==> Q ((Suc x) + y)"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
233 |
val th = topthm(); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
234 |
val i = 1; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
235 |
val (gthi, exp) = IsaND.fix_alls i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
236 |
val newth = Seq.hd (Asm_full_simp_tac 1 gthi); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
237 |
Seq.list_of (IsaND.export_back exp newth); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
238 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
239 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
240 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
241 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
242 |
(* exporting function that takes a solution to the fixed/assumed goal, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
243 |
and uses this to solve the subgoal in the main theorem *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
244 |
fun export_solution (export {fixes = cfvs, assumes = hcprems, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
245 |
sgid = i, gth = gth}) solth = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
246 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
247 |
val solth' = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
248 |
solth |> Drule.implies_intr_list hcprems |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
249 |
|> Drule.forall_intr_list cfvs |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
250 |
in Drule.compose_single (solth', i, gth) end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
251 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
252 |
val exports_solution = foldr (uncurry export_solution); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
253 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
254 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
255 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
256 |
|
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
257 |
(* fix parameters of a subgoal "i", as free variables, and create an |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
258 |
exporting function that will use the result of this proved goal to |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
259 |
show the goal in the original theorem. |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
260 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
261 |
Note, an advantage of this over Isar is that it supports instantiation |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
262 |
of unkowns in the earlier theorem, ie we can do instantiation of meta |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
263 |
vars! *) |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
264 |
(* loosely corresponds to: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
265 |
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
266 |
Result: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
267 |
("(As ==> SGi x') ==> (As ==> SGi x')" : thm, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
268 |
expf : |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
269 |
("As ==> SGi x'" : thm) -> |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
270 |
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
271 |
*) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
272 |
fun fix_alls' i th = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
273 |
let |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
274 |
val t = (prop_of th); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
275 |
val names = Term.add_term_names (t,[]); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
276 |
val gt = Logic.get_goal t i; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
277 |
val body = Term.strip_all_body gt; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
278 |
val alls = rev (Term.strip_all_vars gt); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
279 |
val fvs = map Free |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
280 |
((Term.variantlist (map fst alls, names)) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
281 |
~~ (map snd alls)); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
282 |
val sgn = Thm.sign_of_thm th; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
283 |
val ctermify = Thm.cterm_of sgn; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
284 |
val cfvs = rev (map ctermify fvs); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
285 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
286 |
val body' = (subst_bounds (fvs,body)); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
287 |
val gthi0 = Thm.trivial (ctermify body'); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
288 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
289 |
(* Given a thm justifying subgoal i, solve subgoal i *) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
290 |
(* Note: fails if there are choices! *) |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
291 |
(* fun exportf thi = |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
292 |
Drule.compose_single (Drule.forall_intr_list cfvs thi, |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
293 |
i, th) *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
294 |
in (gthi0, cfvs) end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
295 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
296 |
(* small example: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
297 |
Goal "!! x. [| False; C x |] ==> P x"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
298 |
val th = topthm(); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
299 |
val i = 1; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
300 |
val (goalth, fixes) = fix_alls' i (topthm()); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
301 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
302 |
Goal "!! x. P (x + (Suc y)) ==> Q ((Suc x) + y)"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
303 |
Goal "!! x. P x y = Q y x ==> P x y"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
304 |
val th = topthm(); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
305 |
val i = 1; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
306 |
val (prems, gthi, expf) = IsaND.fixes_and_assumes i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
307 |
val gth2 = Seq.hd (RWStepTac.rwstep_tac prems 1 gthi); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
308 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
309 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
310 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
311 |
(* hide other goals *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
312 |
(* note the export goal is rotated by (i - 1) and will have to be |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
313 |
unrotated to get backto the originial position(s) *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
314 |
fun hide_other_goals th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
315 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
316 |
(* tl beacuse fst sg is the goal we are interested in *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
317 |
val cprems = tl (Drule.cprems_of th) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
318 |
val aprems = map Thm.assume cprems |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
319 |
in |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
320 |
(Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
321 |
cprems) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
322 |
end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
323 |
(* test with: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
324 |
Goal "!! x. [| False; C x |] ==> P x"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
325 |
val th = topthm(); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
326 |
val i = 1; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
327 |
val (goalth, fixedvars) = IsaND.fix_alls' i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
328 |
val (newth, hiddenprems) = IsaND.hide_other_goals goalth; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
329 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
330 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
331 |
(* a nicer version of the above that leaves only a single subgoal (the |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
332 |
other subgoals are hidden hyps, that the exporter suffles about) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
333 |
namely the subgoal that we were trying to solve. *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
334 |
(* loosely corresponds to: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
335 |
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
336 |
Result: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
337 |
("(As ==> SGi x') ==> SGi x'" : thm, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
338 |
expf : |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
339 |
("SGi x'" : thm) -> |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
340 |
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
341 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
342 |
fun fix_alls i th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
343 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
344 |
val (fixed_gth, fixedvars) = fix_alls' i th |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
345 |
val (sml_gth, othergoals) = hide_other_goals fixed_gth |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
346 |
in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
347 |
(sml_gth, export {fixes = fixedvars, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
348 |
assumes = othergoals, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
349 |
sgid = i, gth = th}) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
350 |
end; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
351 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
352 |
(* small example: |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
353 |
Goal "!! x. [| False; C x |] ==> P x"; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
354 |
val th = topthm(); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
355 |
val i = 1; |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
356 |
val (goalth, exp) = IsaND.fix_alls i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
357 |
val oldthewth = Seq.list_of (IsaND.export_back exp goalth); |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
358 |
|
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
359 |
val (premths, goalth2, expf2) = IsaND.assume_prems 1 goalth; |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
360 |
val False_th = nth_elem (0,premths); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
361 |
val anything = False_th RS (thm "FalseE"); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
362 |
val th2 = anything RS goalth2; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
363 |
val th1 = expf2 th2; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
364 |
val final_th = flat (map expf th1); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
365 |
*) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
366 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
367 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
368 |
(* assume the premises of subgoal "i", this gives back a list of |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
369 |
assumed theorems that are the premices of subgoal i, it also gives |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
370 |
back a new goal thm and an exporter, the new goalthm is as the old |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
371 |
one, but without the premices, and the exporter will use a proof of |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
372 |
the new goalthm, possibly using the assumed premices, to shoe the |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
373 |
orginial goal. *) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
374 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
375 |
(* Note: Dealing with meta vars, need to meta-level-all them in the |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
376 |
shyps, which we can later instantiate with a specific value.... ? |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
377 |
think about this... maybe need to introduce some new fixed vars and |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
378 |
then remove them again at the end... like I do with rw_inst. *) |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
379 |
(* loosely corresponds to: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
380 |
Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
381 |
Result: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
382 |
(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
383 |
"SGi ==> SGi" : thm, -- new goal |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
384 |
"SGi" ["A0" ... "An"] : thm -> -- export function |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
385 |
("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
386 |
*) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
387 |
fun assume_prems i th = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
388 |
let |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
389 |
val t = (prop_of th); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
390 |
val gt = Logic.get_goal t i; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
391 |
val _ = case Term.strip_all_vars gt of [] => () |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
392 |
| _ => raise ERROR_MESSAGE "assume_prems: goal has params" |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
393 |
val body = gt; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
394 |
val prems = Logic.strip_imp_prems body; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
395 |
val concl = Logic.strip_imp_concl body; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
396 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
397 |
val sgn = Thm.sign_of_thm th; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
398 |
val ctermify = Thm.cterm_of sgn; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
399 |
val cprems = map ctermify prems; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
400 |
val aprems = map Thm.assume cprems; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
401 |
val gthi = Thm.trivial (ctermify concl); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
402 |
|
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
403 |
(* fun explortf thi = |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
404 |
Drule.compose (Drule.implies_intr_list cprems thi, |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
405 |
i, th) *) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
406 |
in |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
407 |
(aprems, gthi, cprems) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
408 |
end; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
409 |
(* small example: |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
410 |
Goal "False ==> b"; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
411 |
val th = topthm(); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
412 |
val i = 1; |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
413 |
val (prems, goalth, cprems) = IsaND.assume_prems i (topthm()); |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
414 |
val F = hd prems; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
415 |
val FalseE = thm "FalseE"; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
416 |
val anything = F RS FalseE; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
417 |
val thi = anything RS goalth; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
418 |
val res' = expf thi; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
419 |
*) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
420 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
421 |
|
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
422 |
(* first fix the variables, then assume the assumptions *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
423 |
(* loosely corresponds to: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
424 |
Given |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
425 |
"[| SG0; ... |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
426 |
!! xs. [| A0 xs; ... An xs |] ==> SGi xs; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
427 |
... SGm |] ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
428 |
Result: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
429 |
(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
430 |
"SGi xs' ==> SGi xs'" : thm, -- new goal |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
431 |
"SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
432 |
("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
433 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
434 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
435 |
(* Note: the fix_alls actually pulls through all the assumptions which |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
436 |
means that the second export is not needed. *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
437 |
fun fixes_and_assumes i th = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
438 |
let |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
439 |
val (fixgth, exp1) = fix_alls i th |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
440 |
val (assumps, goalth, _) = assume_prems 1 fixgth |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
441 |
in |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
442 |
(assumps, goalth, exp1) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
443 |
end; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
444 |
(* test with: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
445 |
Goal "!! x. [| False; C x |] ==> P x"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
446 |
val th = topthm(); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
447 |
val i = 1; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
448 |
val (fixgth, exp) = IsaND.fix_alls i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
449 |
val (assumps, goalth, _) = assume_prems 1 fixgth; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
450 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
451 |
val oldthewth = Seq.list_of (IsaND.export_back exp fixgth); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
452 |
val oldthewth = Seq.list_of (IsaND.export_back exp goalth); |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
453 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
454 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
455 |
val (prems, goalth, expf) = IsaND.fixes_and_assumes i th; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
456 |
val F = hd prems; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
457 |
val FalseE = thm "FalseE"; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
458 |
val anything = F RS FalseE; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
459 |
val thi = anything RS goalth; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
460 |
val res' = expf thi; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
461 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
462 |
|
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
463 |
(* Fixme: allow different order of subgoals given to expf *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
464 |
(* make each subgoal into a separate thm that needs to be proved *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
465 |
(* loosely corresponds to: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
466 |
Given |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
467 |
"[| SG0; ... SGm |] ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
468 |
Result: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
469 |
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
470 |
["SG0", ..., "SGm"] : thm list -> -- export function |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
471 |
"G" : thm) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
472 |
*) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
473 |
fun subgoal_thms th = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
474 |
let |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
475 |
val t = (prop_of th); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
476 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
477 |
val prems = Logic.strip_imp_prems t; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
478 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
479 |
val sgn = Thm.sign_of_thm th; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
480 |
val ctermify = Thm.cterm_of sgn; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
481 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
482 |
val aprems = map (Thm.trivial o ctermify) prems; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
483 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
484 |
fun explortf premths = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
485 |
Drule.implies_elim_list th premths |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
486 |
in |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
487 |
(aprems, explortf) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
488 |
end; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
489 |
(* small example: |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
490 |
Goal "A & B"; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
491 |
by (rtac conjI 1); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
492 |
val th = topthm(); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
493 |
val (subgoals, expf) = subgoal_thms (topthm()); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
494 |
*) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
495 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
496 |
(* make all the premices of a theorem hidden, and provide an unhide |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
497 |
function, that will bring them back out at a later point. This is |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
498 |
useful if you want to get back these premices, after having used the |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
499 |
theorem with the premices hidden *) |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
500 |
(* loosely corresponds to: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
501 |
Given "As ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
502 |
Result: ("G [As]" : thm, |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
503 |
"G [As]" : thm -> "As ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
504 |
*) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
505 |
fun hide_prems th = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
506 |
let |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
507 |
val sgn = Thm.sign_of_thm th; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
508 |
val ctermify = Thm.cterm_of sgn; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
509 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
510 |
val t = (prop_of th); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
511 |
val prems = Logic.strip_imp_prems t; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
512 |
val cprems = map ctermify prems; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
513 |
val aprems = map Thm.trivial cprems; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
514 |
|
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
515 |
(* val unhidef = Drule.implies_intr_list cprems; *) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
516 |
in |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
517 |
(Drule.implies_elim_list th aprems, cprems) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
518 |
end; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
519 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
520 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
521 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
522 |
|
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
523 |
(* Fixme: allow different order of subgoals in exportf *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
524 |
(* as above, but also fix all parameters in all subgoals, and uses |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
525 |
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
526 |
subgoals. *) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
527 |
(* loosely corresponds to: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
528 |
Given |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
529 |
"[| !! x0s. A0s x0s ==> SG0 x0s; |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
530 |
...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
531 |
Result: |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
532 |
(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
533 |
... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
534 |
["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
535 |
"G" : thm) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
536 |
*) |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
537 |
(* requires being given solutions! *) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
538 |
fun fixed_subgoal_thms th = |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
539 |
let |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
540 |
val (subgoals, expf) = subgoal_thms th; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
541 |
(* fun export_sg (th, exp) = exp th; *) |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
542 |
fun export_sgs expfs solthms = |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
543 |
expf (map2 (op |>) (solthms, expfs)); |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
544 |
(* expf (map export_sg (ths ~~ expfs)); *) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
545 |
in |
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
546 |
apsnd export_sgs (Library.split_list (map (apsnd export_solution o |
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
547 |
fix_alls 1) subgoals)) |
15150
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
548 |
end; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
549 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
550 |
|
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
551 |
(* small example: |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
552 |
Goal "(!! x. ((C x) ==> (A x)))"; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
553 |
val th = topthm(); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
554 |
val i = 1; |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
555 |
val (subgoals, expf) = fixed_subgoal_thms (topthm()); |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
556 |
*) |
c7af682b9ee5
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
paulson
parents:
diff
changeset
|
557 |
|
15250
217bececa2bd
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
dixon
parents:
15150
diff
changeset
|
558 |
end; |