-
Notifications
You must be signed in to change notification settings - Fork 0
/
Proof_Checker.thy
5639 lines (5369 loc) · 306 KB
/
Proof_Checker.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
theory "Proof_Checker"
imports
Ordinary_Differential_Equations.ODE_Analysis
"./Ids"
"./Lib"
"./Syntax"
"./Denotational_Semantics"
"./Axioms"
"./Differential_Axioms"
"./Frechet_Correctness"
"./Static_Semantics"
"./Coincidence"
"./Bound_Effect"
"./Uniform_Renaming"
"./USubst_Lemma"
"./Pretty_Printer"
begin
section \<open>Proof Checker\<close>
text \<open>This proof checker defines a datatype for proof terms in dL and a function for checking proof
terms, with a soundness proof that any proof accepted by the checker is a proof of a sound rule or
valid formula.
A simple concrete hybrid system and a differential invariant rule for conjunctions are provided
as example proofs.
\<close>
lemma sound_weaken_gen:"\<And>A B C. sublist A B \<Longrightarrow> sound (A, C) \<Longrightarrow> sound (B,C)"
proof (rule soundI_mem)
fix A B::"sequent list"
and C::"sequent"
and I::"interp"
assume sub:"sublist A B"
assume good:"is_interp I"
assume "sound (A, C)"
then have soundC:"(\<And>\<phi>. List.member A \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV) \<Longrightarrow> seq_sem I C = UNIV"
apply simp
apply(drule soundD_mem)
by (auto simp add: good)
assume SG:"(\<And>\<phi>. List.member B \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV)"
show "seq_sem I C = UNIV"
using soundC SG sub unfolding sublist_def by auto
qed
lemma sound_weaken:"\<And>SG SGS C. sound (SGS, C) \<Longrightarrow> sound (SG # SGS, C)"
subgoal for SG SGS C
apply(induction SGS)
subgoal unfolding sound_def by auto
subgoal for SG2 SGS
unfolding sound_def
by (metis fst_conv le0 length_Cons not_less_eq nth_Cons_Suc snd_conv)
done
done
lemma member_filter:"\<And>P. List.member (filter P L) x \<Longrightarrow> List.member L x"
apply(induction L, auto)
by(metis (full_types) member_rec(1))
lemma mem_appL:"List.member A x \<Longrightarrow> List.member (A @ B) x"
by(induction A, auto simp add: member_rec)
lemma mem_appR:"List.member B x \<Longrightarrow> List.member (A @ B) x"
by(induction A, auto simp add: member_rec)
lemma sound_weaken_appR:"\<And>SG SGS C. sound (SG, C) \<Longrightarrow> sound (SG @ SGS, C)"
subgoal for SG SGS C
apply(rule sound_weaken_gen)
apply(auto)
unfolding sublist_def apply(rule allI)
subgoal for x
using mem_appL[of SG x SGS] by auto
done
done
fun start_proof::"sequent \<Rightarrow> rule"
where "start_proof S = ([S], S)"
lemma start_proof_sound:"sound (start_proof S)"
unfolding sound_def by auto
section \<open>Proof Checker Implementation\<close>
datatype rrule = ImplyR | AndR |CohideRR | TrueR | EquivR | Skolem | NotR
| HideR | CutRight "formula" | EquivifyR | CommuteEquivR | BRenameR ident ident
| ExchangeR nat | OrR
(* CohideR | *)
datatype lrule = ImplyL | AndL | HideL | FalseL
| NotL | CutLeft "formula" | EquivL | BRenameL ident ident
| OrL
(* EquivForwardL | EquivBackwardL | *)
datatype axRule =
(* CT
|*) CQ (* "('a, 'c) trm" "('a, 'c) trm" "('a, 'b, 'c) subst" "('a, 'b, 'c) pt" (*"('c \<Rightarrow> trm )" "('c \<Rightarrow> trm )" *)"'c"*)
| CE (* "('a, 'b, 'c) formula" "('a, 'b, 'c) formula" "('a, 'b, 'c) subst" "('a, 'b, 'c) derivation"*)
| G
| monb
datatype axiom =
AloopIter | AI | Atest | Abox | Achoice | AK | AV | Aassign | Adassign
| Advar | AdConst | AdPlus | AdMult
| ADW | ADE | ADC | ADS
|(* ADIGr | ADG |*) AEquivReflexive | ADiffEffectSys
| AAllElim | ADiffLinear | ABoxSplit | AImpSelf | Acompose | AconstFcong | AdMinus | AassignEq | AallInst
| AassignAny | AequalCommute
| ATrueImply | Adiamond | AdiamondModusPonens | AequalRefl | AlessEqualRefl
| Aassignd | Atestd | Achoiced | Acomposed | Arandomd
datatype ruleApp =
URename ident ident
(*| BRename 'c 'c*)
| RightRule "rrule" nat
| LeftRule "lrule" nat
| CloseId nat nat
| Cohide2 nat nat
| Cut "formula"
| DIGeqSchema "ODE" "trm" "trm"
| DIGrSchema "ODE" "trm" "trm"
| DIEqSchema "ODE" "trm" "trm"
(*| ARApp "('a,'b,'c) axRule"*)
datatype pt =
FOLRConstant "formula"
| RuleApplication "pt" "ruleApp" nat
| AxiomaticRule " axRule"
| PrUSubst " pt" "subst"
| Ax axiom
| FNC "pt" "sequent" "ruleApp"
| Pro "pt" "pt"
| Start "sequent"
| Sub "pt" "pt" nat
type_synonym pf = "sequent * pt"
fun get_axiom:: "axiom \<Rightarrow> formula"
where
"get_axiom AloopIter = loop_iterate_axiom"
| "get_axiom AI = Iaxiom"
| "get_axiom Atest = test_axiom"
| "get_axiom Abox = box_axiom"
| "get_axiom Achoice = choice_axiom"
| "get_axiom AK = Kaxiom"
| "get_axiom AV = Vaxiom"
| "get_axiom Aassign = assign_axiom"
| "get_axiom Adassign = diff_assign_axiom"
| "get_axiom AdConst = diff_const_axiom"
| "get_axiom AdPlus = diff_plus_axiom"
| "get_axiom AdMult = diff_times_axiom"
| "get_axiom Advar = diff_var_axiom"
| "get_axiom ADW = DWaxiom"
| "get_axiom ADE = DEaxiom"
| "get_axiom ADC = DCaxiom"
| "get_axiom ADS = DSaxiom"
(*| "get_axiom ADIGeq = DIGeqaxiom"
| "get_axiom ADIGr = DIGraxiom"*)
(*| "get_axiom ADG = DGaxiom"*)
| "get_axiom AEquivReflexive = EquivReflexiveAxiom"
| "get_axiom ADiffEffectSys = DiffEffectSysAxiom"
| "get_axiom AAllElim = AllElimAxiom"
| "get_axiom ADiffLinear = DiffLinearAxiom"
| "get_axiom ABoxSplit = BoxSplitAxiom"
| "get_axiom AImpSelf = ImpSelfAxiom"
| "get_axiom Acompose = compose_axiom"
| "get_axiom AconstFcong = constFcongAxiom"
| "get_axiom AdMinus = dMinusAxiom"
| "get_axiom AassignEq = assignEqAxiom"
| "get_axiom AallInst = allInstAxiom"
| "get_axiom AassignAny = assignAnyAxiom"
| "get_axiom AequalCommute = equalCommuteAxiom"
| "get_axiom ATrueImply = TrueImplyAxiom"
| "get_axiom Adiamond = diamondAxiom"
| "get_axiom AdiamondModusPonens = diamondModusPonensAxiom"
| "get_axiom AequalRefl = equalReflAxiom"
| "get_axiom AlessEqualRefl = lessEqualReflAxiom"
| "get_axiom Aassignd = assigndAxiom"
| "get_axiom Atestd = testdAxiom"
| "get_axiom Achoiced = choicedAxiom"
| "get_axiom Acomposed = composedAxiom"
| "get_axiom Arandomd = randomdAxiom"
fun get_axrule::"axRule \<Rightarrow> rule"
where
(*"get_axrule CT = CTaxrule"
|*) "get_axrule CQ = CQaxrule"
| "get_axrule CE = CEaxrule"
| "get_axrule G = Gaxrule"
| "get_axrule monb = monbrule"
lemma axrule_sound:"sound (get_axrule ar)"
proof (cases ar)
case CE
then show ?thesis using sound_CEaxrule by auto
next
case CQ
then show ?thesis using sound_CQaxrule by auto
next
case G
then show ?thesis using sound_Gaxrule by auto
next
case monb
then show ?thesis using sound_monbrule by auto
qed
lemma invX:"Rep_ident (Abs_ident ''$x'') = ''$x''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
lemma invY:"Rep_ident (Abs_ident ''$y'') = ''$y''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
lemma invZ:"Rep_ident (Abs_ident ''$z'') = ''$z''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
lemma axiom_safe:"fsafe (get_axiom a)"
by(cases a, auto simp add: axiom_defs Box_def Or_def Equiv_def Implies_def empty_def Equals_def
f1_def p1_def P_def f0_def expand_singleton Forall_def Greater_def id_simps DFunl_def Minus_def
TT_def Leq_def invX invY invZ ident_expose_def Ix_def Iy_def Iz_def SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
lemma axiom_valid:"valid (get_axiom a)"
proof (cases a)
case AloopIter
then show ?thesis by (simp add: loop_valid)
next
case AI
then show ?thesis by (simp add: I_valid)
next
case Atest
then show ?thesis by (simp add: test_valid)
next
case Abox
then show ?thesis by (simp add: box_valid)
next
case Achoice
then show ?thesis by (simp add: choice_valid)
next
case AK
then show ?thesis by (simp add: K_valid)
next
case AV
then show ?thesis by (simp add: V_valid)
next
case Aassign
then show ?thesis by (simp add: assign_valid)
next
case Adassign
then show ?thesis by (simp add: diff_assign_valid)
next
case AdConst
then show ?thesis by (simp add: diff_const_axiom_valid)
next
case AdPlus
then show ?thesis by (simp add: diff_plus_axiom_valid)
next
case AdMult
then show ?thesis by (simp add: diff_times_axiom_valid)
next
case ADW
then show ?thesis by (simp add: DW_valid)
next
case ADE
then show ?thesis by (simp add: DE_valid)
next
case ADC
then show ?thesis by (simp add: DC_valid)
next
case ADS
then show ?thesis by (simp add: DS_valid)
(*next
case ADIGeq
then show ?thesis by (simp add: DIGeq_valid)
next
case ADIGr
then show ?thesis by (simp add: DIGr_valid)*)
(*next
case ADG
then show ?thesis by (simp add: DG_valid)*)
next
case Advar
then show ?thesis by (simp add: diff_var_axiom_valid)
next
case AEquivReflexive
then show ?thesis by (auto simp add: EquivReflexiveAxiom_def valid_def)
next
case ADiffEffectSys
then show ?thesis by (simp add: DiffEffectSys_valid)
next
case AAllElim
then show ?thesis by (simp add: AllElimAxiom_valid)
next
case ADiffLinear
then show ?thesis by (simp add: DiffLinear_valid)
next
case ABoxSplit
then show ?thesis by(auto simp add: BoxSplitAxiom_def valid_def)
next
case AImpSelf
then show ?thesis by(auto simp add: ImpSelfAxiom_def TT_def valid_def)
next
case Acompose
then show ?thesis by(simp add: compose_valid)
next
case AconstFcong
then show ?thesis by (simp add: constFcong_valid)
next
case AdMinus
then show ?thesis by (simp add: dMinusAxiom_valid)
next
case AassignEq
then show ?thesis by (simp add: assignEq_valid)
next
case AallInst
then show ?thesis by (simp add: allInst_valid)
next
case AassignAny
then show ?thesis by (simp add: assignAny_valid)
next
case AequalCommute
then show ?thesis by (simp add: equalCommute_valid)
next
case ATrueImply
then show ?thesis by (simp add: TrueImply_valid)
next
case Adiamond
then show ?thesis by (simp add: diamond_valid)
next
case AdiamondModusPonens
then show ?thesis by (simp add: diamondModusPonens_valid)
next
case AequalRefl
then show ?thesis by (simp add: equalRefl_valid)
next
case AlessEqualRefl
then show ?thesis by (simp add: lessEqualRefl_valid)
next
case Aassignd
then show ?thesis by (simp add: assignd_valid)
next
case Atestd
then show ?thesis by (simp add: testd_valid)
next
case Achoiced
then show ?thesis by (simp add: choiced_valid)
next
case Acomposed
then show ?thesis by (simp add: composed_valid)
next
case Arandomd
then show ?thesis by (simp add: randomd_valid)
qed
fun seq_to_string :: "sequent \<Rightarrow> char list"
where "seq_to_string (A,S) = join '', '' (map fml_to_string A) @ '' |- '' @ join '', '' (map fml_to_string S)"
fun rule_to_string :: "rule \<Rightarrow> char list"
where "rule_to_string (SG, C) = (join '';; '' (map seq_to_string SG)) @ '' '' @ \<^cancel>\<open>[char_of_nat 10] @ \<close>seq_to_string C"
fun close :: "'a list \<Rightarrow> 'a \<Rightarrow>'a list"
where "close L x = filter (\<lambda>y. y \<noteq> x) L"
(* this way proof is harder but actually has right behavior *)
fun closeI ::"'a list \<Rightarrow> nat \<Rightarrow>'a list"
where "closeI (x # xs) 0 = xs"
| "closeI (x # xs) (Suc n) = x # (closeI xs n)"
| "closeI Nil _ = undefined"
fun replaceI :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list"
where "replaceI (x # xs) 0 y = (y # xs)"
| "replaceI (x # xs) (Suc n) y = x # (replaceI xs n y)"
| "replaceI Nil _ _ = undefined"
lemma close_sub:"sublist (close \<Gamma> \<phi>) \<Gamma>"
apply (auto simp add: sublist_def)
using member_filter by fastforce
lemma closeI_sub:"j < length \<Gamma> \<Longrightarrow> sublist (closeI \<Gamma> j) \<Gamma>"
proof -
assume j:"j < length \<Gamma>"
have imp:"j < length \<Gamma> \<Longrightarrow> sublist (closeI \<Gamma> j) \<Gamma>"
apply(rule index_list_induct[of "(\<lambda> \<Gamma> j. sublist (closeI \<Gamma> j) \<Gamma>)"])
subgoal for L by (auto simp add: sublist_def, cases L, auto simp add: member_rec)
using j by(auto simp add: sublist_def member_rec j)
then show ?thesis using j by auto
qed
lemma close_app_comm:"close (A @ B) x = close A x @ close B x"
by auto
lemma close_provable_sound:"sound (SG, C) \<Longrightarrow> sound (close SG \<phi>, \<phi>) \<Longrightarrow> sound (close SG \<phi>, C)"
proof (rule soundI_mem)
fix I::"interp"
assume S1:"sound (SG, C)"
assume S2:"sound (close SG \<phi>, \<phi>)"
assume good:"is_interp I"
assume SGCs:"(\<And>\<phi>'. List.member (close SG \<phi>) \<phi>' \<Longrightarrow> seq_sem I \<phi>' = UNIV)"
have S\<phi>:"seq_sem I \<phi> = UNIV"
using S2 apply simp
apply(drule soundD_mem)
using good apply auto
using SGCs UNIV_I by fastforce
have mem_close:"\<And>P. List.member SG P \<Longrightarrow> P \<noteq> \<phi> \<Longrightarrow> List.member (close SG \<phi>) P"
by(induction SG, auto simp add: member_rec)
have SGs:"\<And>P. List.member SG P \<Longrightarrow> seq_sem I P = UNIV"
subgoal for P
apply(cases "P = \<phi>")
subgoal using S\<phi> by auto
subgoal using mem_close[of P] SGCs by auto
done
done
show "seq_sem I C = UNIV"
using S1 apply simp
apply(drule soundD_mem)
using good apply auto
using SGs apply auto
using impl_sem by blast
qed
datatype rule_ret =
Rok "sequent list"
| Rerr "sequent list"
datatype step_ret =
Sok "rule"
| Serr "rule list"
fun LeftRule_result :: "lrule \<Rightarrow> nat \<Rightarrow> sequent \<Rightarrow> sequent list option"
where "LeftRule_result AndL j (A,S) = (case (nth A j) of And p q \<Rightarrow>
Some [((closeI A j) @ [p, q], S)]
| _ \<Rightarrow> None)"
| "LeftRule_result ImplyL j (A,S) = (case (nth A j) of Not (And (Not q) (Not (Not p))) \<Rightarrow>
Some [(closeI A j, S @ [p]),
(replaceI A j q, S)] | _ \<Rightarrow> None)"
(*| "LeftRule_result EquivForwardL j (A,S) = (case (nth A j) of Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) \<Rightarrow>
(if (p = p' & q = q') then Some [(closeI A j @ [q], S), (closeI A j, S @ [p])] else None) | _ \<Rightarrow> None)"
| "LeftRule_result EquivBackwardL j (A,S) = (case (nth A j) of Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) \<Rightarrow>
(if (p = p' & q = q') then Some [(closeI A j @ [p], S), (closeI A j , S @ [q])] else None) | _ \<Rightarrow> None)"*)
| "LeftRule_result HideL j (A,S) =
Some [(closeI A j, S)]"
| "LeftRule_result (CutLeft f) j (A,S) = Some [((replaceI A j f),S), ((closeI A j), S @[Implies (nth A j) f])]"
| "LeftRule_result EquivL j (A,S) = (case (nth A j) of Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) \<Rightarrow>
(if (p = p' & q = q') then Some [(replaceI A j (And p q), S), (replaceI A j (And (Not p) (Not q)) , S)] else None) | _ \<Rightarrow> None)"
| "LeftRule_result (BRenameL x y) j (A,S) = (if x = y then None else
(case (nth A j) of
Not(Diamond (Assign xvar \<theta>) (Not \<phi>)) \<Rightarrow>
(if
(x = xvar \<and>
(TRadmit \<theta> \<and> FRadmit([[Assign xvar \<theta>]]\<phi>) \<and> FRadmit \<phi> \<and> fsafe ([[Assign xvar \<theta>]]\<phi>) \<and>
{Inl y, Inr y, Inr x} \<inter> FVF ([[Assign xvar \<theta>]]\<phi>) = {}) \<and>
FRadmit ([[y := \<theta>]]FUrename xvar y \<phi>) \<and>
FRadmit (FUrename xvar y \<phi>) \<and>
fsafe ([[y := \<theta>]]FUrename xvar y \<phi>) \<and>
{Inl xvar, Inr xvar, Inr y} \<inter> FVF ([[y := \<theta>]]FUrename xvar y \<phi>) = {})
then
Some [(replaceI A j (FBrename x y (nth A j)),S)]
else None)
| Not(Exists xvar (Not \<phi>)) \<Rightarrow>
(if
x = xvar \<and>
(FRadmit(Forall xvar \<phi>) \<and>
FRadmit \<phi> \<and>
fsafe (Forall xvar \<phi>) \<and>
{Inl y, Inr y, Inr x} \<inter> FVF (Forall xvar \<phi>) = {}) \<and>
FRadmit (Forall y (FUrename xvar y \<phi>)) \<and>
FRadmit (FUrename xvar y \<phi>) \<and>
fsafe (Forall y (FUrename xvar y \<phi>)) \<and>
{Inl xvar, Inr xvar, Inr y} \<inter> FVF (Forall y (FUrename xvar y \<phi>)) = {}
then
Some [(replaceI A j (FBrename x y (nth A j)),S)]
else None)
| _ \<Rightarrow> None))"
| Lstep_Not:"LeftRule_result NotL j (A,S) = (case (nth A j) of (Not p) \<Rightarrow> Some [(closeI A j , S @ [p])] | _ \<Rightarrow> None)"
| Lstep_FalseR:"LeftRule_result FalseL j (A,S) = (if (nth A j) = FF then (Some []) else None)"
| Lstep_OrL:"LeftRule_result OrL j (A,S) =
(case (nth A j) of
Not (And (Not p) (Not q)) \<Rightarrow>
Some [(replaceI A j p, S),
(replaceI A j q, S)]
| _ \<Rightarrow> None
)"
(* Note: Some of the pattern-matching here is... interesting. The reason for this is that we can only
match on things in the base grammar, when we would quite like to check things in the derived grammar.
So all the pattern-matches have the definitions expanded, sometimes in a silly way. *)
fun RightRule_result :: "rrule \<Rightarrow> nat \<Rightarrow> sequent \<Rightarrow> sequent list option"
where
Rstep_Not:"RightRule_result NotR j (A,S) = (case (nth S j) of (Not p) \<Rightarrow> Some [(A @ [p], closeI S j)] | _ \<Rightarrow> None)"
| Rstep_And:"RightRule_result AndR j (A,S) = (case (nth S j) of (And p q) \<Rightarrow> Some [(A, replaceI S j p), (A, replaceI S j q)] | _ \<Rightarrow> None)"
| Rstep_Imply:"RightRule_result ImplyR j (A,S) = (case (nth S j) of Not (And (Not q) (Not (Not p))) \<Rightarrow>
Some [(A @ [p], (closeI S j) @ [q])] | _ \<Rightarrow> None)"
| Rstep_EquivR:"RightRule_result EquivR j (A,S) =
(case (nth S j) of Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) \<Rightarrow>
(if (p = p' \<and> q = q') then (Some [(A @ [p], (closeI S j) @ [q]), ( A @ [q], (closeI S j) @ [p])])
else (None)) | _ \<Rightarrow> None)"
(*| Rstep_CohideR:"RightRule_result CohideR j (A,S) = Some [(A, [nth S j])]"*)
| Rstep_CohideRR:"RightRule_result CohideRR j (A,S) = Some [([], [nth S j])]"
| Rstep_TrueR:"RightRule_result TrueR j (A,S) = (case (nth S j) of (Geq (Const x) (Const y)) \<Rightarrow>
(if (x = y & (sint (Rep_bword x) = 0)) then(Some []) else None) | _ \<Rightarrow> None)"
| Step_Skolem:"RightRule_result Skolem j (A,S) = (case (nth S j) of (Not (Exists x (Not p))) \<Rightarrow>
(if ((Inl x) \<notin> FVSeq (A,S)) \<and>
fsafe (foldr (&&) A TT) \<and>
fsafe (foldr (||) (closeI S j) FF)
then
Some [(A, replaceI S j p)]
else None)
| _ \<Rightarrow> None)"
| RStep_BR:"RightRule_result (BRenameR x y) j (A,S) = (if x = y then None else
(case (nth S j) of
Not(Diamond (Assign xvar \<theta>) (Not \<phi>)) \<Rightarrow>
(if
x = xvar \<and>
(TRadmit \<theta> \<and> FRadmit([[Assign xvar \<theta>]]\<phi>) \<and> FRadmit \<phi> \<and> fsafe ([[Assign xvar \<theta>]]\<phi>) \<and>
{Inl y, Inr y, Inr x} \<inter> FVF ([[Assign xvar \<theta>]]\<phi>) = {}) \<and>
FRadmit ([[y := \<theta>]]FUrename xvar y \<phi>) \<and>
FRadmit (FUrename xvar y \<phi>) \<and>
fsafe ([[y := \<theta>]]FUrename xvar y \<phi>) \<and>
{Inl xvar, Inr xvar, Inr y} \<inter> FVF ([[y := \<theta>]]FUrename xvar y \<phi>) = {}
then
Some [(A, replaceI S j (FBrename x y (nth S j)))]
else None)
| Not(Exists xvar (Not \<phi>)) \<Rightarrow>
(if
x = xvar \<and>
(FRadmit(Forall xvar \<phi>) \<and>
FRadmit \<phi> \<and>
fsafe (Forall xvar \<phi>) \<and>
{Inl y, Inr y, Inr x} \<inter> FVF (Forall xvar \<phi>) = {}) \<and>
FRadmit (Forall y (FUrename xvar y \<phi>)) \<and>
FRadmit (FUrename xvar y \<phi>) \<and>
fsafe (Forall y (FUrename xvar y \<phi>)) \<and>
{Inl xvar, Inr xvar, Inr y} \<inter> FVF (Forall y (FUrename xvar y \<phi>)) = {}
then
Some [(A, replaceI S j (FBrename x y (nth S j)))]
else None)
| _ \<Rightarrow> None))"
| RStep_ExchangeR:"RightRule_result (ExchangeR k) j (A,S) =
(if j \<noteq> k \<and> k < length S then
Some [(A, replaceI (replaceI S j (nth S k)) k (nth S j))]
else None)"
| Rstep_OrR:"RightRule_result (OrR) j (A,S) =
(case (nth S j) of
Not (And (Not p) (Not q)) \<Rightarrow>
Some [(A, ((closeI S j) @ [p, q]))]
| _ \<Rightarrow> None
)
"
(* TODO: Is this derivable *)
(* (if ((case (SG ! i) of ([],[Not(Diamond(Assign x t) (Not p))]) \<Rightarrow> True | _ \<Rightarrow> False)) then
Some (merge_seqs SG [SBrename x y (nth SG i)] i,C)
else None)*)
| Rstep_HideR:"RightRule_result HideR j (A,S) = Some [(A, closeI S j)]"
(** G |- c, D G |- c->p, D
* ------------------------- (Cut right)
* G |- p, D*)
| Rstep_CutRight:"RightRule_result (CutRight v) j (A,S) = Some [(A, replaceI S j v), (A,replaceI S j (Implies v (nth S j)))]"
(* G |- a<->b, D
* -------------
* G |- a->b, D*)
| Rstep_EquivifyR:"RightRule_result EquivifyR j (A,S) = (case (nth S j) of Not (And (Not q) (Not (Not p))) \<Rightarrow>
Some [(A, replaceI S j (Equiv p q))] | _ \<Rightarrow> None)"
(* G |- q<->p, D
* ------------- (<->cR)
* G |- p<->q, D*)
| Rstep_CommuteEquivR:"RightRule_result CommuteEquivR j (A,S) = (case nth S j of
Not(And (Not (And p q)) (Not (And (Not p') (Not q')))) \<Rightarrow>
(if (p = p' \<and> q = q') then (Some[(A, replaceI S j (Equiv q p))])
else None)| _ \<Rightarrow> None)"
lemma fml_seq_valid:"valid \<phi> \<Longrightarrow> seq_valid ([], [\<phi>])"
unfolding seq_valid_def valid_def by auto
lemma closeI_provable_sound:"\<And>i. sound (SG, C) \<Longrightarrow> sound (closeI SG i, (nth SG i)) \<Longrightarrow> i < length SG \<Longrightarrow> sound (closeI SG i, C)"
proof (rule soundI_mem)
fix i and I::"interp"
assume S1:"sound (SG, C)"
assume S2:"sound (closeI SG i, SG ! i)"
assume good:"is_interp I"
assume SGCs:"(\<And>\<phi>. List.member (closeI SG i) \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV)"
assume i:"i < length SG"
have S\<phi>:"seq_sem I (SG ! i) = UNIV"
using S2 apply simp
apply(drule soundD_mem)
using good apply auto
using SGCs UNIV_I by fastforce
have mem_close_ind:"(\<forall>P. List.member SG P \<longrightarrow> P \<noteq> (SG ! i) \<longrightarrow> List.member (closeI SG i) P)"
apply(rule index_list_induct[of "(\<lambda> SG i. (\<forall>P. List.member SG P \<longrightarrow> P \<noteq> (SG ! i) \<longrightarrow> List.member (closeI SG i) P))"])
subgoal for L by(induction L,auto simp add: member_rec)
by(auto simp add: member_rec i)
then have mem_close:"\<And>P. List.member SG P \<Longrightarrow> P \<noteq> (SG ! i) \<Longrightarrow> List.member (closeI SG i) P"
by auto
have SGs:"\<And>P. List.member SG P \<Longrightarrow> seq_sem I P = UNIV"
subgoal for P
apply(cases "P = (SG ! i)")
subgoal using S\<phi> by auto
subgoal using mem_close[of P] SGCs by auto
done
done
show "seq_sem I C = UNIV"
using S1 apply simp
apply(drule soundD_mem)
using good apply auto
using SGs apply auto
using impl_sem by blast
qed
lemma valid_to_sound:"seq_valid A \<Longrightarrow> sound (B, A)"
unfolding seq_valid_def sound_def by auto
lemma sound_to_valid:"sound ([], A) \<Longrightarrow> seq_valid A"
unfolding seq_valid_def sound_def by auto
lemma closeI_valid_sound:"\<And>i. i < length SG \<Longrightarrow> sound (SG, C) \<Longrightarrow> seq_valid (nth SG i) \<Longrightarrow> sound (closeI SG i, C)"
using valid_to_sound closeI_provable_sound by auto
fun merge_rules :: "rule \<Rightarrow> rule \<Rightarrow> nat \<Rightarrow> rule option"
where
"merge_rules (P1,C1) (Nil,C2) i =
(if (i < length P1 \<and> nth P1 i = C2) then
Some (closeI P1 i, C1)
else
(None))"
| "merge_rules (P1,C1) (S # SS, C2) i =
(if (i < length P1 \<and> nth P1 i = C2) then
Some ((replaceI P1 i S) @ SS, C1)
else None)"
lemma soundE_mem:"sound (SG,C) \<Longrightarrow> (\<And>I. is_interp I \<Longrightarrow> (\<And>\<phi>. List.member SG \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV) \<Longrightarrow> seq_sem I C = UNIV)"
proof -
assume snd:"sound (SG,C)"
have sound:"\<And>I. is_interp I \<Longrightarrow>
(\<And>i. i\<ge>0 \<Longrightarrow> i < length (fst (SG, C)) \<Longrightarrow> seq_sem I (fst (SG, C) ! i) = UNIV) \<Longrightarrow> seq_sem I C = UNIV"
using snd[unfolded sound_def] by(auto)
fix I::"interp"
assume good_interp:"is_interp I"
assume pres:"(\<And>\<phi>. List.member SG \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV)"
show "seq_sem I C = UNIV"
apply(rule sound)
apply(rule good_interp)
apply(simp)
subgoal for i
using pres[of "SG ! i"] nth_member[of i SG]
by auto
done
qed
lemma permute_sound:
assumes sound:"sound (SG1,C)"
assumes permute:"set SG1 = set SG2"
shows "sound (SG2,C)"
proof -
have in_mem:"\<And>i L. (List.member L i) = (i \<in> set L)"
subgoal for i L
apply(induction L)
by(auto simp add: List.member_rec)
done
have mem:"\<And>i. List.member SG1 i \<Longrightarrow> List.member SG2 i"
subgoal for i
using permute in_mem[of SG1 i] in_mem[of SG2 i] by auto done
show ?thesis
apply(rule soundI_mem)
using soundE_mem[OF sound] permute mem by(auto)
qed
lemma closeI_perm: "i < length L \<Longrightarrow> set ((List.nth L i) # closeI L i) = set L"
proof -
assume i:"i < length L"
have imp:"i < length L \<longrightarrow> set ((List.nth L i) # closeI L i) = set L"
apply(rule index_list_induct)
subgoal for L by(cases L,auto)
by(auto simp add: i)
then show ?thesis using i by(auto)
qed
lemma merge_front_sound:
assumes S1:"sound (C2 # SG1,C)"
assumes S2:"sound (SG2,C2)"
shows "sound (SG2 @ SG1,C)"
proof (rule soundI_mem)
fix I::"interp"
assume good_interp:"is_interp I"
assume pres:"(\<And>\<phi>. List.member (SG2 @ SG1) \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV)"
have presL:"(\<And>\<phi>. List.member SG2 \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV)"
subgoal for \<phi>
using pres mem_appL[of "SG2" \<phi> "SG1"] by auto done
have presR:"(\<And>\<phi>. List.member SG1 \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV)"
subgoal for \<phi>
using pres[of \<phi>] mem_appR[of SG1 \<phi> SG2] by auto done
have cSem:"seq_sem I C2 = UNIV"
using soundE_mem[OF S2 good_interp presL] by auto
have pres1:"(\<And>\<phi>. List.member (C2 # SG1) \<phi> \<Longrightarrow> seq_sem I \<phi> = UNIV)"
using cSem presR by(auto simp add: List.member_rec)
show "seq_sem I C = UNIV"
using soundE_mem[OF S1 good_interp pres1]
soundE_mem[OF S2 good_interp presL]
by(auto)
qed
lemma set_eq_left:
assumes eq:"set A1 = set A2"
shows "set (A1 @ L) = set (A2 @ L)"
by(induction L,auto simp add: eq)
lemma closeI_set_perm:"i < length SG1 \<Longrightarrow> set (S # closeI SG1 i) = set (replaceI SG1 i S)"
proof -
assume i:"i < length SG1"
have imp:"i < length SG1 \<Longrightarrow> set (S # closeI SG1 i) = set (replaceI SG1 i S)"
apply(rule index_list_induct[of "(\<lambda> SG1 i. set (S # closeI SG1 i) = set (replaceI SG1 i S))"])
subgoal for L using i by(cases L,auto simp add: i)
by(auto)
then show ?thesis using i by auto
qed
lemma merge_rules_some_match:
assumes merge:"merge_rules (SG1,C1) (SG2,C2) i = Some R"
shows"nth SG1 i = C2"
using merge apply(cases SG2,simp) apply(cases " i < length SG1 \<and> SG1 ! i = C2",auto) apply(cases " i < length SG1 \<and> SG1 ! i = C2",auto)
done
lemma merge_rules_sound:
assumes S1:"sound (SG1,C1)"
assumes S2:"sound (SG2,C2)"
assumes i:"i < length SG1"
assumes merge:"merge_rules (SG1,C1) (SG2,C2) i = Some R"
shows "sound R"
proof (cases SG2, auto)
case Nil then have Result:"SG2 = []" by auto
have at:"nth SG1 i = C2" using merge merge_rules_some_match by auto
from Result have valid:"seq_valid C2"
using sound_to_valid S2 by auto
then have valid:"seq_valid (nth SG1 i)" using at by auto
then show "sound R"
using closeI_valid_sound[OF i S1 valid] merge Result i at by auto
next
case (Cons S SS) then have Result:"SG2 = S # SS" by auto
have at:"nth SG1 i = C2" using merge merge_rules_some_match by auto
have sound1:"sound ([C2] @ closeI SG1 i, C1)"
apply(rule permute_sound[OF S1])
using closeI_perm[OF i] at by auto
have sound2:"sound (SG2 @ closeI SG1 i, C1)"
apply(rule merge_front_sound)
using sound1 S2 by auto
have sound3:"sound ((S # closeI SG1 i) @ SS, C1)"
apply(rule permute_sound[OF sound2])
using Result by auto
have sound:"sound (replaceI SG1 i S @ SS, C1)"
apply(rule permute_sound[OF sound3])
apply(rule set_eq_left)
apply(rule closeI_set_perm)
by(rule i)
then show "sound R" using merge at i Result by(auto)
qed
fun rule_result :: "rule \<Rightarrow> (nat * ruleApp) \<Rightarrow> rule option"
where
Step_LeftRule:"rule_result (SG,C) (i,LeftRule L j) =
(if j \<ge> length (fst (nth SG i)) then None else
(case (LeftRule_result L j (nth SG i)) of
Some a \<Rightarrow> merge_rules (SG,C) (a, nth SG i) i
| None \<Rightarrow> None))"
| Step_RightRule:"rule_result (SG,C) (i,RightRule R j) =
(if j \<ge> length (snd (nth SG i)) then None else
(case (RightRule_result R j (nth SG i)) of
Some a \<Rightarrow> merge_rules (SG,C) (a, nth SG i) i
| None \<Rightarrow> None\<^cancel>\<open>[(SG,C)]\<close>))"
| Step_Cut:"rule_result (SG,C) (i,Cut \<phi>) =
(if(fsafe \<phi>) then
(let (A,S)= nth SG i in (merge_rules (SG,C) ([(A @ [\<phi>], S), (A, S @ [\<phi>])], (A,S)) i))
else None)"
| Step_CloseId:"rule_result (SG,C) (i,CloseId j k) =
(if (j < length (fst (nth SG i))) \<and> (k < length (snd (nth SG i))) \<and> nth (fst (nth SG i)) j = nth (snd (nth SG i)) k then
Some (closeI SG i, C)
else None)"
| Step_UR:"rule_result (SG, C) (i, URename x y) =
(if(FRadmit (seq2fml (SG ! i)) \<and> FRadmit (seq2fml (SUrename x y (SG ! i))) \<and> fsafe (seq2fml (SUrename x y (SG ! i)))) then
merge_rules (SG,C) ([SUrename x y (nth SG i)],nth SG i) i
else None)"
| Step_Cohide2:"rule_result (SG, C) (i, Cohide2 j k) =
(if ((j \<ge> length (fst (nth SG i))) \<or> (k \<ge> length (snd (nth SG i)))) then None
else
(merge_rules (SG,C) ([([nth (fst(nth SG i)) j],[nth (snd(nth SG i)) k])], (nth SG i)) i))"
| Step_DIGeq:"rule_result (SG,C) (i, DIGeqSchema ODE \<theta>1 \<theta>2) =
( let proved =
([],[Implies
(Implies (DPredl vid1) (And (Geq \<theta>1 \<theta>2) ([[EvolveODE ODE (DPredl vid1)]](Geq (Differential \<theta>1) (Differential \<theta>2)))))
([[EvolveODE ODE (DPredl vid1)]](Geq \<theta>1 \<theta>2))])
in
let wanted = nth SG i in
if (proved = wanted \<and>
osafe ODE \<and>
dfree \<theta>1 \<and>
dfree \<theta>2 \<and>
FVT \<theta>1 \<subseteq> Inl ` ODE_dom ODE \<and>
FVT \<theta>2 \<subseteq> Inl ` ODE_dom ODE) then
Some (closeI SG i,C)
else None)"
| Step_DIGr:"rule_result (SG,C) (i, DIGrSchema ODE \<theta>1 \<theta>2) =
( let proved =
([],[Implies
(Implies (DPredl vid1) (And (Greater \<theta>1 \<theta>2) ([[EvolveODE ODE (DPredl vid1)]](Geq (Differential \<theta>1) (Differential \<theta>2)))))
([[EvolveODE ODE (DPredl vid1)]](Greater \<theta>1 \<theta>2))])
in
let wanted = nth SG i in
if (proved = wanted \<and>
osafe ODE \<and>
dfree \<theta>1 \<and>
dfree \<theta>2 \<and>
FVT \<theta>1 \<subseteq> Inl ` ODE_dom ODE \<and>
FVT \<theta>2 \<subseteq> Inl ` ODE_dom ODE) then
Some (closeI SG i,C)
else None)"
| Step_DIEq:"rule_result (SG,C) (i, DIEqSchema ODE \<theta>1 \<theta>2) =
( let proved =
([],[Implies
(Implies (DPredl vid1) (And (Equals \<theta>1 \<theta>2) ([[EvolveODE ODE (DPredl vid1)]](Equals (Differential \<theta>1) (Differential \<theta>2)))))
([[EvolveODE ODE (DPredl vid1)]](Equals \<theta>1 \<theta>2))])
in
let wanted = nth SG i in
if (proved = wanted \<and>
osafe ODE \<and>
dfree \<theta>1 \<and>
dfree \<theta>2 \<and>
FVT \<theta>1 \<subseteq> Inl ` ODE_dom ODE \<and>
FVT \<theta>2 \<subseteq> Inl ` ODE_dom ODE) then
Some (closeI SG i,C)
else None)
"
fun fnc :: "rule \<Rightarrow> sequent \<Rightarrow> ruleApp \<Rightarrow> rule option"
where "fnc r seq ra =
(case (rule_result (start_proof seq) (0,ra)) of
Some rule \<Rightarrow> merge_rules rule r 0
| None \<Rightarrow> None)"
fun pro :: "rule \<Rightarrow> rule \<Rightarrow> rule option"
where "pro r1 r2 = merge_rules r2 r1 0"
fun pt_result :: "pt \<Rightarrow> rule option"
where
"pt_result (FOLRConstant f) = Some ([], ([],[f]))"
| "pt_result (RuleApplication pt ra i) = (case (pt_result pt) of Some res \<Rightarrow> (if i \<ge> length (fst res) then None else rule_result res (i,ra)) | None \<Rightarrow> None)"
| "pt_result (AxiomaticRule ar) = Some(get_axrule ar)"
| "pt_result (PrUSubst pt sub) = (case (pt_result pt) of Some res \<Rightarrow>
(if ssafe sub \<and> Radmit sub res \<and> Rsafe res \<and> (FVS sub = {} \<or> (fst res = []) \<or> res = CQaxrule) then
Some (Rsubst res sub)
else None) | None \<Rightarrow> None)"
| "pt_result (Ax a) = Some([], ([],[get_axiom a]))"
| "pt_result (FNC pt seq ra) =
(case (pt_result pt) of
Some res \<Rightarrow> fnc res seq ra
| None \<Rightarrow> None)"
| "pt_result (Pro pt1 pt2) =
(case pt_result pt2 of
Some res2 \<Rightarrow>
(if (1 \<noteq> length (fst (res2))) then None else
(case pt_result pt1 of
Some res1 \<Rightarrow> pro res1 res2
| None \<Rightarrow> None))
| None \<Rightarrow> None)"
| "pt_result (Start f) = Some(start_proof f)"
| "pt_result (Sub pt1 pt2 i) =
(case pt_result pt1 of
Some res1 \<Rightarrow>
(if (i \<ge> length (fst (res1))) then None else
(case pt_result pt2 of
Some res2 \<Rightarrow> merge_rules res1 res2 i
| None \<Rightarrow> None))
| None \<Rightarrow> None)"
thm Or_def
thm Implies_def
inductive lrule_ok ::" sequent list \<Rightarrow> sequent \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> lrule \<Rightarrow> bool"
where
LeftRule_And:"(case (nth (fst (nth SG i)) j) of (p && q) \<Rightarrow> True | _ \<Rightarrow> False) \<Longrightarrow> lrule_ok SG C i j AndL"
| LeftRule_EquivForward:"(case (nth (fst (nth SG i)) j) of (!(!(PPPP && Q) && !(! PP && ! QQ))) \<Rightarrow> (PPPP = PP) \<and> (Q = QQ)| _ \<Rightarrow> False) \<Longrightarrow> lrule_ok SG C i j EquivForwardL"
| LeftRule_Imply:"(case (nth (fst (nth SG i)) j) of ( !(!Q && !(!PP))) \<Rightarrow> True | _ \<Rightarrow> False) \<Longrightarrow> lrule_ok SG C i j ImplyL"
| LeftRule_EquivBackward:"(case (nth (fst (nth SG i)) j) of (!(!(PPPP && Q) && !(! PP && ! QQ))) \<Rightarrow> (PPPP = PP) \<and> (Q = QQ) | _ \<Rightarrow> False) \<Longrightarrow> lrule_ok SG C i j EquivBackwardL"
| LeftRule_False:"nth (fst (nth SG i)) j = Geq \<^bold>0 (One) \<Longrightarrow> lrule_ok SG C i j FalseL"
named_theorems prover "Simplification rules for checking validity of proof certificates"
lemmas [prover] = axiom_defs Box_def Or_def Implies_def filter_append ssafe_def SDom_def FUadmit_def PFUadmit_def id_simps
inductive_simps
LeftRule_And[prover]: "lrule_ok SG C i j AndL"
and LeftRule_Imply[prover]: "lrule_ok SG C i j ImplyL"
and LeftRule_Forward[prover]: "lrule_ok SG C i j EquivForwardL"
and LeftRule_EquivBackward[prover]: "lrule_ok SG C i j EquivBackwardL"
inductive rrule_ok ::"sequent list \<Rightarrow> sequent \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> rrule \<Rightarrow> bool"
where
RightRule_And:"(case (nth (snd (nth SG i)) j) of (p && q) \<Rightarrow> True | _ \<Rightarrow> False) \<Longrightarrow> rrule_ok SG C i j AndR"
| RightRule_Imply:"(case (nth (snd (nth SG i)) j) of ( !(!Q && !(!PP))) \<Rightarrow> True | _ \<Rightarrow> False) \<Longrightarrow> rrule_ok SG C i j ImplyR"
| RightRule_Equiv:"(case (nth (snd (nth SG i)) j) of (!(!(PPPP && Q) && !(! PP && ! QQ))) \<Rightarrow> (PPPP = PP) \<and> (Q = QQ) | _ \<Rightarrow> False) \<Longrightarrow> rrule_ok SG C i j EquivR"
(* Note: Used to ban no-op cohides because close function breaks if sequent unchanged by rule, but we should just get the close function right instead *)
| RightRule_Cohide:"length (snd (nth SG i)) > j \<Longrightarrow> \<^cancel>\<open>(length (snd (nth SG i)) \<noteq> 1) \<Longrightarrow>\<close> rrule_ok SG C i j CohideR"
| RightRule_CohideRR:"length (snd (nth SG i)) > j \<Longrightarrow> \<^cancel>\<open> fst (nth SG i) \<noteq> [] \<Longrightarrow> length (snd (nth SG i)) \<noteq> 1 \<Longrightarrow>\<close> rrule_ok SG C i j CohideRR"
| RightRule_True:"nth (snd (nth SG i)) j = Geq \<^bold>0 \<^bold>0 \<Longrightarrow> rrule_ok SG C i j TrueR"
(* | RightRule_Cohide:"length (snd (nth SG i)) > j \<Longrightarrow> (\<And>\<Gamma> q. (nth SG i) \<noteq> (\<Gamma>, [q])) \<Longrightarrow> rrule_ok SG C i j CohideR"
*)
inductive_simps
RightRule_And_simps[prover]: "rrule_ok SG C i j AndR"
and RightRule_Imply_simps[prover]: "rrule_ok SG C i j ImplyR"
and RightRule_Equiv_simps[prover]: "rrule_ok SG C i j EquivR"
and RightRule_CohideR_simps[prover]: "rrule_ok SG C i j CohideR"
and RightRule_CohideRR_simps[prover]: "rrule_ok SG C i j CohideRR"
and RightRule_TrueR_simps[prover]: "rrule_ok SG C i j TrueR"
inductive sing_at::"(ident \<Rightarrow> trm) \<Rightarrow> trm \<Rightarrow> ident \<Rightarrow> bool"
where sing_at_zero: "is_vid1 i \<Longrightarrow> f i = \<theta> \<Longrightarrow> sing_at f \<theta> i "
| sing_not_zero: "\<not>(is_vid1 i) \<Longrightarrow> f i = \<^bold>0 \<Longrightarrow> sing_at f \<theta> i"
inductive is_singleton :: "(ident \<Rightarrow> trm) \<Rightarrow> trm \<Rightarrow> bool"
where Is_singleton: "(\<forall>i. sing_at (\<lambda>i. if is_vid1 i then \<theta> else \<^bold>0) \<theta> i) \<Longrightarrow> is_singleton (\<lambda>i. if is_vid1 i then \<theta> else \<^bold>0) \<theta> "
subsection \<open>Soundness\<close>
named_theorems member_intros "Prove that stuff is in lists"
lemma mem_sing[member_intros]:"\<And>x. List.member [x] x"
by(auto simp add: member_rec)
lemma mem_filter[member_intros]:"\<And>A P x. P x \<Longrightarrow> List.member A x \<Longrightarrow> List.member (filter P A) x"
subgoal for A
by(induction A, auto simp add: member_rec)
done
lemma sound_weaken_appL:"\<And>SG SGS C. sound (SGS, C) \<Longrightarrow> sound (SG @ SGS, C)"
subgoal for SG SGS C
apply(rule sound_weaken_gen)
apply(auto)
unfolding sublist_def apply(rule allI)
subgoal for x
using mem_appR[of SGS x SG] by auto
done
done
lemma close_nonmember_eq:"\<not>(List.member A a) \<Longrightarrow> close A a = A"
by (induction A, auto simp add: member_rec)
lemma close_noneq_nonempty:"List.member A x \<Longrightarrow> x \<noteq> a \<Longrightarrow> close A a \<noteq> []"
by(induction A, auto simp add: member_rec)
lemma close_app_neq:"List.member A x \<Longrightarrow> x \<noteq> a \<Longrightarrow> close (A @ B) a \<noteq> B"
using append_self_conv2[of "close A a" "close B a"] append_self_conv2[of "close A a" "B"] close_app_comm[of A B a] close_noneq_nonempty[of A x a]
apply(cases "close B a = B")
apply (auto)
by (metis (no_types, lifting) filter_True filter_append mem_Collect_eq set_filter)
lemma member_singD:"\<And>x P. P x \<Longrightarrow> (\<And>y. List.member [x] y \<Longrightarrow> P y)"
by (metis member_rec(1) member_rec(2))
lemma fst_neq:"A \<noteq> B \<Longrightarrow> (A,C) \<noteq> (B,D)"
by auto
lemma equiv_case_lem:"\<And>X. (case X of ! ((! (And PPPP Q)) && (! (And (! PP) (! QQ)))) \<Rightarrow>( PPPP = PP \<and> Q = QQ )
| ! (! (And PPPP Q) && (! (And (! PP) _))) \<Rightarrow> False
| ! (! (And PPPP Q) && (! (And _ formula2))) \<Rightarrow> False
| ! (! (And PPPP Q) && (! _)) \<Rightarrow> False
| ! (! (And PPPP Q) && _) \<Rightarrow> False
| ! (And (! _) formula2) \<Rightarrow> False
| ! (And _ formula2) \<Rightarrow> False
| ! _ \<Rightarrow> False
| _ \<Rightarrow> False) \<Longrightarrow> (\<exists> Q P. (X = (Q \<leftrightarrow> P)))"
subgoal for X
apply(cases "\<exists> PPPP PP Q QQ. X = (! (! (PPPP && Q) && ! (! PP && ! QQ)))")
subgoal apply auto subgoal for PP QQ by (simp add: Equiv_def Or_def) done
proof -
assume a0:"
case X of Not (Not (PPPP && Q) && Not (Not PP && Not QQ)) \<Rightarrow> PPPP = PP \<and> Q = QQ | ! (! (PPPP && Q) && ! (Not PP && _)) \<Rightarrow> False
| ! (Not (And PPPP Q) && Not (And _ xb)) \<Rightarrow> False
| ! (Not (And PPPP Q) && Not _) \<Rightarrow> False
| ! (Not (And PPPP Q) && _) \<Rightarrow> False
| ! (And (Not _) xb) \<Rightarrow> False
| ! (And _ xb) \<Rightarrow> False
| ! _ \<Rightarrow> False
| _ \<Rightarrow> False"
assume a1:"\<nexists>PPPP PP Q QQ. X = ! (! (PPPP && Q) && ! (! PP && ! QQ))"
show "\<exists>Q P. X = (Q \<leftrightarrow> P)"
apply(cases "\<exists> PPPP Q PP QQ. X = ! (! (PPPP && Q) && ! (! PP && QQ))")
subgoal using a0 a1 apply (auto simp add: Equiv_def Or_def) subgoal for PPPP Q PP QQ by(cases QQ, auto) done
proof -