isa-incredible.git
3 years agoUse Eisbach’s solves in apply scripts master AFP-Submission
Joachim Breitner [Fri, 20 May 2016 08:03:31 +0000 (10:03 +0200)]
Use Eisbach’s solves in apply scripts

3 years agoadd Stream_Ext to document
Denis Lohner [Fri, 20 May 2016 08:08:49 +0000 (10:08 +0200)]
add Stream_Ext to document

3 years agofix import of Stream
Denis Lohner [Fri, 20 May 2016 07:44:28 +0000 (09:44 +0200)]
fix import of Stream

3 years agoremove subsubsection Task 1.1 in Predicate_Tasks
Denis Lohner [Fri, 20 May 2016 07:42:50 +0000 (09:42 +0200)]
remove subsubsection Task 1.1 in Predicate_Tasks

3 years agorefactor duplicate fact sset_cycle
Denis Lohner [Fri, 20 May 2016 07:42:34 +0000 (09:42 +0200)]
refactor duplicate fact sset_cycle

3 years agoInclude Predicate Task in document
Joachim Breitner [Fri, 20 May 2016 07:17:59 +0000 (09:17 +0200)]
Include Predicate Task in document

3 years agoRepair proof (simpler now)
Joachim Breitner [Thu, 19 May 2016 21:44:51 +0000 (23:44 +0200)]
Repair proof (simpler now)

3 years agoFinish acyclicity
Joachim Breitner [Thu, 19 May 2016 21:36:30 +0000 (23:36 +0200)]
Finish acyclicity

3 years agoOne sorry left
Joachim Breitner [Thu, 19 May 2016 19:51:56 +0000 (21:51 +0200)]
One sorry left

3 years agoPrunedness
Joachim Breitner [Thu, 19 May 2016 19:49:40 +0000 (21:49 +0200)]
Prunedness

3 years agoSmall steps
Joachim Breitner [Thu, 19 May 2016 19:46:05 +0000 (21:46 +0200)]
Small steps

3 years agoMultiple interpretation commands make it easier
Joachim Breitner [Thu, 19 May 2016 19:38:29 +0000 (21:38 +0200)]
Multiple interpretation commands make it easier

3 years agoExample tasks using predicate (unfinished)
Joachim Breitner [Thu, 19 May 2016 16:50:25 +0000 (18:50 +0200)]
Example tasks using predicate (unfinished)

3 years agoIncredible_Propositional should not depend on Natural_Deduction
Joachim Breitner [Thu, 19 May 2016 15:04:50 +0000 (17:04 +0200)]
Incredible_Propositional should not depend on Natural_Deduction

3 years agoAdd Incredible_Predicate.thy
Joachim Breitner [Thu, 19 May 2016 15:02:05 +0000 (17:02 +0200)]
Add Incredible_Predicate.thy

3 years agoAdd Predicate Formula instantiation
Joachim Breitner [Thu, 19 May 2016 14:45:44 +0000 (16:45 +0200)]
Add Predicate Formula instantiation

3 years agocomment and refactor propositional
Denis Lohner [Thu, 19 May 2016 14:30:16 +0000 (16:30 +0200)]
comment and refactor propositional

3 years agowording and parantheses
Denis Lohner [Thu, 19 May 2016 13:33:13 +0000 (15:33 +0200)]
wording and parantheses

3 years agoUse HOL instead of HOLCF in session
Denis Lohner [Thu, 19 May 2016 12:51:07 +0000 (14:51 +0200)]
Use HOL instead of HOLCF in session

3 years agoadd Task 2.11
Denis Lohner [Thu, 19 May 2016 12:48:48 +0000 (14:48 +0200)]
add Task 2.11

3 years agoPropositional: rename Const -> Fun and C -> Const
Denis Lohner [Thu, 19 May 2016 12:48:28 +0000 (14:48 +0200)]
Propositional: rename Const -> Fun and C -> Const

3 years agoprettify sset_cycle
Denis Lohner [Thu, 19 May 2016 12:46:34 +0000 (14:46 +0200)]
prettify sset_cycle

3 years agorename facts to avoid 'Duplicate fact declaration' errors
Denis Lohner [Thu, 19 May 2016 12:45:56 +0000 (14:45 +0200)]
rename facts to avoid 'Duplicate fact declaration' errors

3 years agoNode -> RNode
Denis Lohner [Thu, 19 May 2016 12:34:20 +0000 (14:34 +0200)]
Node -> RNode

3 years agoproof of sset_cycle
Denis Lohner [Thu, 19 May 2016 10:38:01 +0000 (12:38 +0200)]
proof of sset_cycle

3 years agoFinish instantiation, and split theory into multiple
Joachim Breitner [Thu, 19 May 2016 10:02:12 +0000 (12:02 +0200)]
Finish instantiation, and split theory into multiple

3 years agoStart of interpretation for propositional logic
Denis Lohner [Thu, 19 May 2016 09:33:42 +0000 (11:33 +0200)]
Start of interpretation for propositional logic

3 years agoTitelei
Joachim Breitner [Thu, 19 May 2016 09:20:49 +0000 (11:20 +0200)]
Titelei

3 years agoPresentation polish
Joachim Breitner [Thu, 19 May 2016 09:10:09 +0000 (11:10 +0200)]
Presentation polish

3 years agoPut rose_trees in a separate file
Joachim Breitner [Thu, 19 May 2016 08:49:06 +0000 (10:49 +0200)]
Put rose_trees in a separate file

3 years agoFactor out a general rose tree data type
Joachim Breitner [Thu, 19 May 2016 08:41:01 +0000 (10:41 +0200)]
Factor out a general rose tree data type

3 years agoLess case_tac
Joachim Breitner [Thu, 19 May 2016 07:51:51 +0000 (09:51 +0200)]
Less case_tac

3 years agoAll hail inductive_cases
Joachim Breitner [Thu, 19 May 2016 07:46:53 +0000 (09:46 +0200)]
All hail inductive_cases

3 years agoMove some prefix-related lemmas
Joachim Breitner [Wed, 18 May 2016 17:17:53 +0000 (19:17 +0200)]
Move some prefix-related lemmas

3 years agoSplit out Inits theory
Joachim Breitner [Wed, 18 May 2016 17:15:34 +0000 (19:15 +0200)]
Split out Inits theory

3 years agoDocument setup
Joachim Breitner [Wed, 18 May 2016 17:13:23 +0000 (19:13 +0200)]
Document setup

3 years agoUn-Sorry
Joachim Breitner [Wed, 18 May 2016 15:00:29 +0000 (17:00 +0200)]
Un-Sorry

3 years agoreintroduce a sorry
Denis Lohner [Wed, 18 May 2016 14:57:48 +0000 (16:57 +0200)]
reintroduce a sorry

3 years agoremove parameter fresh_vars
Denis Lohner [Wed, 18 May 2016 08:08:42 +0000 (10:08 +0200)]
remove parameter fresh_vars

3 years agoLemma moved
Joachim Breitner [Wed, 18 May 2016 13:02:09 +0000 (15:02 +0200)]
Lemma moved

3 years agoAll sories gone!
Joachim Breitner [Wed, 18 May 2016 12:58:30 +0000 (14:58 +0200)]
All sories gone!

3 years agoIncredible_Completeness only needs plain_iwf
Joachim Breitner [Wed, 18 May 2016 12:33:21 +0000 (14:33 +0200)]
Incredible_Completeness only needs plain_iwf

3 years agoFix local_iwf_it
Joachim Breitner [Wed, 18 May 2016 12:28:02 +0000 (14:28 +0200)]
Fix local_iwf_it

3 years agoComplete sublocale Well_Scoped_Instantiation
Joachim Breitner [Wed, 18 May 2016 12:27:17 +0000 (14:27 +0200)]
Complete sublocale Well_Scoped_Instantiation

3 years agoGet rid of a few sorries
Joachim Breitner [Wed, 18 May 2016 08:52:13 +0000 (10:52 +0200)]
Get rid of a few sorries

3 years agorerename needs an explicit set
Joachim Breitner [Wed, 18 May 2016 08:27:57 +0000 (10:27 +0200)]
rerename needs an explicit set

3 years agotowards rerename_subst
Joachim Breitner [Wed, 18 May 2016 08:07:07 +0000 (10:07 +0200)]
towards rerename_subst

3 years agoImplement rerename
Joachim Breitner [Wed, 18 May 2016 07:58:54 +0000 (09:58 +0200)]
Implement rerename

3 years agoadd missing 'end'
Denis Lohner [Wed, 18 May 2016 07:47:47 +0000 (09:47 +0200)]
add missing 'end'

3 years agoKleine Schritte
Joachim Breitner [Tue, 17 May 2016 21:03:10 +0000 (23:03 +0200)]
Kleine Schritte

3 years agoInjectivity of labels is given
Joachim Breitner [Tue, 17 May 2016 20:24:06 +0000 (22:24 +0200)]
Injectivity of labels is given

3 years agoTowards variable globalization
Joachim Breitner [Tue, 17 May 2016 17:00:54 +0000 (19:00 +0200)]
Towards variable globalization

3 years agoSplit off Build_Incredible_Tree
Joachim Breitner [Tue, 17 May 2016 14:40:42 +0000 (16:40 +0200)]
Split off Build_Incredible_Tree

3 years agoUse list in trees, nat list as paths
Joachim Breitner [Tue, 17 May 2016 14:34:21 +0000 (16:34 +0200)]
Use list in trees, nat list as paths

3 years agoAdd subst_renameLCs
Joachim Breitner [Tue, 17 May 2016 08:17:50 +0000 (10:17 +0200)]
Add subst_renameLCs

3 years agoAbstractFormulas: Talk about local constants
Joachim Breitner [Tue, 17 May 2016 08:07:21 +0000 (10:07 +0200)]
AbstractFormulas: Talk about local constants

3 years agoCompleteness: Use annotations instead of fidx
Joachim Breitner [Fri, 13 May 2016 14:15:43 +0000 (16:15 +0200)]
Completeness: Use annotations instead of fidx

3 years agos/oops/qed/
Joachim Breitner [Thu, 12 May 2016 19:33:49 +0000 (21:33 +0200)]
s/oops/qed/

3 years agoIntroduce vidx
Joachim Breitner [Thu, 12 May 2016 16:25:37 +0000 (18:25 +0200)]
Introduce vidx

3 years agoMerge 'preform and 'form
Joachim Breitner [Thu, 12 May 2016 16:15:01 +0000 (18:15 +0200)]
Merge 'preform and 'form

3 years agointroduce polymorphic annotations
Denis Lohner [Thu, 12 May 2016 14:16:23 +0000 (16:16 +0200)]
introduce polymorphic annotations

3 years agofix assumption conclusions_closed
Denis Lohner [Thu, 12 May 2016 09:28:38 +0000 (11:28 +0200)]
fix assumption conclusions_closed

3 years agoTowards scoped variables
Joachim Breitner [Thu, 12 May 2016 09:12:05 +0000 (11:12 +0200)]
Towards scoped variables

3 years agoTighten well_scoped_inst
Joachim Breitner [Wed, 11 May 2016 14:21:01 +0000 (16:21 +0200)]
Tighten well_scoped_inst

3 years agoFactor out fidx_iAnnot (unproven)
Joachim Breitner [Wed, 11 May 2016 14:08:11 +0000 (16:08 +0200)]
Factor out fidx_iAnnot (unproven)

3 years agoTry to get tree stuff into a file of its own
Joachim Breitner [Wed, 11 May 2016 13:22:14 +0000 (15:22 +0200)]
Try to get tree stuff into a file of its own

3 years agoto_form_conc_forms
Joachim Breitner [Tue, 10 May 2016 15:15:26 +0000 (17:15 +0200)]
to_form_conc_forms

3 years agoShow that edge labels match up
Joachim Breitner [Fri, 26 Feb 2016 14:26:43 +0000 (15:26 +0100)]
Show that edge labels match up

up to the question of matching the indices.

3 years agoDefine hyp edges
Joachim Breitner [Thu, 25 Feb 2016 15:35:05 +0000 (16:35 +0100)]
Define hyp edges

3 years agoOn the existence of hypothesis along the way
Joachim Breitner [Tue, 23 Feb 2016 16:15:23 +0000 (17:15 +0100)]
On the existence of hypothesis along the way

3 years agoIntroduce HNode
Joachim Breitner [Tue, 23 Feb 2016 13:33:44 +0000 (14:33 +0100)]
Introduce HNode

3 years agoCleanup, prunedness
Joachim Breitner [Tue, 23 Feb 2016 13:04:52 +0000 (14:04 +0100)]
Cleanup, prunedness

3 years agoNight shift: categorize scope via prefix
Joachim Breitner [Tue, 23 Feb 2016 02:00:17 +0000 (03:00 +0100)]
Night shift: categorize scope via prefix

3 years agoMore on completeness, but it feels like the wrong way...
Joachim Breitner [Mon, 22 Feb 2016 17:09:19 +0000 (18:09 +0100)]
More on completeness, but it feels like the wrong way...

3 years agoCheckpoint completeness proof
Joachim Breitner [Mon, 22 Feb 2016 13:41:10 +0000 (14:41 +0100)]
Checkpoint completeness proof

3 years agoIsabelle2016 compat
Joachim Breitner [Mon, 22 Feb 2016 10:05:01 +0000 (11:05 +0100)]
Isabelle2016 compat

3 years agoAdd forgotten files
Joachim Breitner [Sun, 21 Feb 2016 17:56:14 +0000 (18:56 +0100)]
Add forgotten files

3 years agoA somewhat elaborated tree
Joachim Breitner [Sun, 21 Feb 2016 17:52:40 +0000 (18:52 +0100)]
A somewhat elaborated tree

3 years agoAdd Helper blocks, and Cuts
Joachim Breitner [Sun, 21 Feb 2016 16:29:15 +0000 (17:29 +0100)]
Add Helper blocks, and Cuts

3 years agostuff towards completeness
Joachim Breitner [Sun, 21 Feb 2016 15:26:55 +0000 (16:26 +0100)]
stuff towards completeness

3 years agoIntroduce an elaborated tree
Joachim Breitner [Fri, 12 Feb 2016 15:23:49 +0000 (16:23 +0100)]
Introduce an elaborated tree

3 years agoIntroduce the notion of a terminal path
Joachim Breitner [Fri, 12 Feb 2016 14:12:51 +0000 (15:12 +0100)]
Introduce the notion of a terminal path

3 years agoRelax requirement on fv (subst s v)
Joachim Breitner [Thu, 11 Feb 2016 10:16:05 +0000 (11:16 +0100)]
Relax requirement on fv (subst s v)

3 years agoCorrectness, now also for predicate logics
Joachim Breitner [Thu, 4 Feb 2016 16:14:00 +0000 (17:14 +0100)]
Correctness, now also for predicate logics

3 years agos/annotate/freshen/g
Joachim Breitner [Thu, 4 Feb 2016 11:35:41 +0000 (12:35 +0100)]
s/annotate/freshen/g

3 years agoNicer definition of eff
Joachim Breitner [Thu, 4 Feb 2016 10:18:25 +0000 (11:18 +0100)]
Nicer definition of eff

3 years agoStructured type for the antecedent
Joachim Breitner [Thu, 4 Feb 2016 09:36:57 +0000 (10:36 +0100)]
Structured type for the antecedent

3 years agoFirst attempt at specifying fresh variables
Joachim Breitner [Wed, 3 Feb 2016 16:01:17 +0000 (17:01 +0100)]
First attempt at specifying fresh variables

3 years agoFiniteness
Joachim Breitner [Wed, 3 Feb 2016 13:32:17 +0000 (14:32 +0100)]
Finiteness

3 years agoAdd gitignore
Joachim Breitner [Tue, 2 Feb 2016 15:54:16 +0000 (16:54 +0100)]
Add gitignore

3 years agoNotion of "solved"
Joachim Breitner [Tue, 2 Feb 2016 15:51:51 +0000 (16:51 +0100)]
Notion of "solved"

3 years agoSimplify
Joachim Breitner [Tue, 2 Feb 2016 14:52:23 +0000 (15:52 +0100)]
Simplify

3 years agoBeginning of an Isabelle Formalisation
Joachim Breitner [Tue, 2 Feb 2016 13:36:12 +0000 (14:36 +0100)]
Beginning of an Isabelle Formalisation