From bd2efacaf67ae84c41377e7af38dacc5aa64f405 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 14 Aug 2020 11:07:17 +0200 Subject: (FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules. (REF) Goal statement assumptions are now put into the new context data slots. (FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data. (REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context. MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`. (REF) Fixed incompatibilities in theories. --- spartan/lib/List.thy | 2 +- spartan/lib/Maybe.thy | 6 +++--- spartan/lib/Prelude.thy | 3 ++- 3 files changed, 6 insertions(+), 5 deletions(-) (limited to 'spartan/lib') diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index dd51582..83e5149 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -149,7 +149,7 @@ Definition map: proof (elim xs) show "[]: List B" by intro next fix x ys - assume "x: A" "ys: List B" + assuming "x: A" "ys: List B" show "f x # ys: List B" by typechk qed diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index 0a7ec21..da22a4e 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -25,10 +25,10 @@ Definition MaybeInd: "\a. a: A \ f a: C (some A a)" "m: Maybe A" shows "C m" - using assms[unfolded Maybe_def none_def some_def] + using assms[unfolded Maybe_def none_def some_def, type] apply (elim m) - apply (rule \_ \ _: C (inl _ _ _)\) - apply (elim, rule \_: C (inr _ _ _)\) + apply fact + apply (elim, fact) done Lemma Maybe_comp_none: diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy index 6adbce8..c0abf31 100644 --- a/spartan/lib/Prelude.thy +++ b/spartan/lib/Prelude.thy @@ -105,7 +105,8 @@ Definition ifelse [rotated 1]: "a: C true" "b: C false" shows "C x" - by (elim x) (elim, rule *)+ + using assms[unfolded Bool_def true_def false_def, type] + by (elim x) (elim, fact)+ Lemma if_true: assumes -- cgit v1.2.3